lean
Datasets
All datasets matching “lean”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.Lean-Workbook
Lean Workbook
This dataset is about contest-level math problems formalized in Lean 4.
Our dataset contains 57231 problems in the split of Lean Workbook and 82893 problems in the split of Lean Workbook Plus. We provide the natural language statement, answer, formal statement, and formal proof (if available) for each problem. These data can support autoformalization model training and searching for proofs.
We open-source our code and our data.
Our test environment is based on Lean… See the full description on the dataset page: https://huggingface.co/datasets/internlm/Lean-Workbook.lean-eval-source
Lean Eval Humanize Source
A reproducible snapshot of 226 self-contained Lean Eval workspaces attempted with
the Humanize workflow. Each workspace contains the trusted problem files, the best
available Humanize submission snapshot, and any submission helper modules.
The snapshot contains 152 comparator-accepted submissions and 74 unaccepted or
unverified attempts. An included attempt is not an assertion that its proof is
valid.
[!WARNING]
Every workspace ships a Solution.lean… See the full description on the dataset page: https://huggingface.co/datasets/humanfia-lab/lean-eval-source.GUEThis is a copy of the Genome Understanding Evaluation (GUE) that was presented in
DNABERT-2: Efficient Foundation Model and Benchmark For Multi-Species Genome
Zhihan Zhou and Yanrong Ji and Weijian Li and Pratik Dutta and Ramana Davuluri and Han Liu
and is available to download directly from
https://github.com/MAGICS-LAB/DNABERT_2
If you use this dataset, please cite
@misc{zhou2023dnabert2,
title={DNABERT-2: Efficient Foundation Model and Benchmark For Multi-Species Genome}… See the full description on the dataset page: https://huggingface.co/datasets/leannmlindsey/GUE.NuminaMath-LEAN
Dataset Card for NuminaMath-LEAN
Dataset Summary
NuminaMath-LEAN is a large-scale dataset of 100K mathematical competition problems formalized in Lean 4. It is derived from a challenging subset of the NuminaMath 1.5 dataset, focusing on problems from prestigious competitions like the IMO and USAMO. It represents the largest collection of human-annotated formal statements and proofs designed for training and evaluating automated theorem provers. This is also the dataset… See the full description on the dataset page: https://huggingface.co/datasets/AI-MO/NuminaMath-LEAN.Lean-workbook-proofsThis is the 29.7 solutions of Lean-workbook found by Goedel-Prover-SFT.
Citation
@misc{lin2025goedelproverfrontiermodelopensource,
title={Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving},
author={Yong Lin and Shange Tang and Bohan Lyu and Jiayun Wu and Hongzhou Lin and Kaiyu Yang and Jia Li and Mengzhou Xia and Danqi Chen and Sanjeev Arora and Chi Jin},
year={2025},
eprint={2502.07640},
archivePrefix={arXiv}… See the full description on the dataset page: https://huggingface.co/datasets/Goedel-LM/Lean-workbook-proofs.