LeanTransitionCorpus is a dataset for training and studying automated theorem proving systems in Lean. Its unit of data is one tactic transition: the proof state before a tactic, the tactic that was executed, and the resulting state. This makes it suitable for tactic prediction, proof-state representation learning, premise selection, retrieval, verification, and trajectory-level training. Many Lean datasets expose a theorem, tactic, and pretty-printed goal strings. This corpus retains those human-readable views, but also preserves richer information Lean Expr trees, local context, metavariables, universe metavariables, source ranges, and premise/context information. The extra…