Theorem Proving · AI-MO
NuminaMath-LEAN
Formal Lean 4 dataset of 100K mathematical competition problems for training and testing automated theorem provers.
What NuminaMath-LEAN is
Developed by AI-MO, the dataset is derived from challenging subsets of the NuminaMath 1.5 dataset, featuring problems from high-level competitions such as the International Mathematical Olympiad (IMO) and the United States of America Mathematical Olympiad (USAMO). It also powers the Kimina-Prover 72B automated reasoning model.
The dataset addresses the scarcity of formal mathematical statements and step-by-step proofs needed to train and evaluate automated theorem provers and neural reasoning models. By translating natural-language contest problems into machine-verifiable code, it enables researchers to systematically benchmark formal verification systems against difficult mathematical tasks.
How it was made
To build the dataset, curators filtered NuminaMath 1.5 to retain competition-grade problems, removing non-competition data such as standard school curricula, as well as geometry and combinatorics problems due to the difficulty of formalising them. The collection was supplemented with an olympiad-level reference split containing problems transcribed and curated from official competition documents, including the IMO, IMO Shortlist, and USAMO.
Problems contain formal statements written in Lean 4 style similar to miniF2F, authored either by human annotators or by an autoformalizer model. Ground truth formal proofs are provided for human-formalised problems and categorised as complete proofs, partial proofs containing 'sorry' place-holders, or statements only. Additionally, the dataset tracks model-generated formal proofs produced during reinforcement learning along with training metadata, such as proof attempts, correct solutions, and model win rates. All formalisations are compiled and verified against mathlib version 4.15.0.
Key facts
- Format
- Parquet
- Formal language
- Lean 4
- Lean library dependency
- mathlib v4.15.0
- Primary domain
- Competition mathematics
What you can use it for
- Training automated theorem provers
- Train formal reasoning systems and large language models using formal Lean 4 statements and human-verified proofs.
- Reinforcement learning for formal reasoning
- Guide reinforcement learning policies using the included problem difficulty metrics, attempt counts, and model win rates.
- Benchmarking theorem-proving systems
- Evaluate automated reasoning models against formalised high-level competition problems derived from IMO and USAMO.
Explore the data
The schema, real rows, full-text search and a SQL filter — read in your browser, nothing downloaded.
Explore
Read the real rows without downloading anything
Reading rows…
LiveRead from AI-MO/NuminaMath-LEAN at the moment you asked. Nothing is cached or stored — every row above came from that request.
How the columns are distributed
Over 104,155 rows of default/train
answer
string_text- min
- 0
- median
- 7
- mean
- 9.97
- max
- 231
6.4% empty
author
string_label- autoformalizer81%
- human19%
exam
string_label- unknown97%
- HMMT1%
- IMO1%
formal_ground_truth
string_text- min
- 0
- median
- 0
- mean
- 412.03
- max
- 69,614
formal_proof
string_text- min
- 0
- median
- 686
- mean
- 1016.80
- max
- 14,324
63.0% empty
formal_statement
string_text- min
- 60
- median
- 382
- mean
- 424.03
- max
- 29,051
ground_truth_type
string_label- complete9%
- statement8%
- with_sorry2%
80.7% empty
problem
string_text- min
- 14
- median
- 190
- mean
- 226.35
- max
- 9,959
problem_type
string_label- Algebra38%
- Number Theory27%
- Inequalities14%
question_type
string_label- math-word-problem55%
- proof31%
- MCQ8%
0.00% empty
source
string_label- olympiads49%
- unknown14%
- aops_forum12%
uuid
string_text- min
- 36
- median
- 36
- mean
- 36
- max
- 36
Strengths and limits
Good at
- Provides a large-scale collection of 100K competition-grade mathematical statements in Lean 4.
- Verified for compatibility with Lean 4 and mathlib version 4.15.0.
- Includes reinforcement learning training data, including attempt counts and success rates from automated proving runs.
- Contains human-annotated formal proofs for benchmark comparisons alongside autoformalised entries.
Watch out for
- Excludes geometry and combinatorics problems due to the complexity of formalising them.
- Contains instances of inaccurate statement formalisations resulting from autoformalizer limitations.
- Lacks complete metadata for certain entries, including missing question types on many human-annotated problems.
- Contains occasional incorrectly extracted reference answers from the original source texts.
Questions
Can I look inside NuminaMath-LEAN without downloading it?
Yes. This page reads its schema, real rows and per-column statistics in the browser, with full-text search and a SQL filter. Nothing is downloaded to your machine.
What licence is NuminaMath-LEAN under?
Its authors declare apache-2.0. Read the terms on the original page before reusing the data.
Which version of Lean is used for the formalisations?
All problems and proofs are written in Lean 4 and verified against mathlib version 4.15.0.
Are all formal statements accompanied by complete proofs?
No. Formal ground truth proofs are only provided for entries formalised by human annotators. These proofs may be complete, partially proven with 'sorry' place-holders, or consist solely of the formalized statement.
Why are there no geometry or combinatorics problems in the dataset?
Geometry and combinatorics categories from NuminaMath 1.5 were intentionally filtered out during curation because of their difficulty to formalise.
What information does the reinforcement learning metadata include?
The rl_data field records how many times a problem was presented to the model during training, the number of successful proofs generated, and the resulting win rate.
How to cite it
Wang, Haiming and Unsal, Mert and Lin, Xiaohan and Baksys, Mantas and Liu, Junqi and Santos, Marco Dos and Sung, Flood and Vinyes, Marina and Ying, Zhenzhe and Zhu, Zekai and Lu, Jianqiao and Saxcé, Hugues de and Bailey, Bolton and Song, Chendong and Xiao, Chenjun and Zhang, Dehao and Zhang, Ebony and Pu, Frederick and Zhu, Han and Liu, Jiawei and Bayer, Jonas and Michel, Julien and Yu, Longhui and Dreyfus-Schmidt, Léo and Tunstall, Lewis and Pagani, Luigi and Machado, Moreira and Bourigault, Pauline and Wang, Ran and Polu, Stanislas and Barroyer, Thibaut and Li, Wen-Ding and Niu, Yazhe and Fleureau, Yann and Hu, Yangyang and Yu, Zhouliang and Wang, Zihan and Yang, Zhilin and Liu, Zhengying and Li, Jia (2025). Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning. arXiv:2504.11354.
Written from NuminaMath-LEAN's own dataset card. Statements citing a figure that does not appear there are removed before publication. Licence and running details come from our registry.