HyperCactus0/LeanTransitionCorpus

LeanTransitionCorpus 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… See the full description on the dataset page: https://huggingface.co/datasets/HyperCactus0/LeanTransitionCorpus.