Theorem Proving · AI-MO
minif2f_test
A corrected Lean 4 test set for the miniF2F formal mathematics benchmark.
What minif2f_test is
minif2f_test is a test set benchmark for formal theorem proving and mathematical reasoning in Lean 4, published by AI-MO. It evaluates the capabilities of automated and neural theorem provers on competition-style mathematical problems.
The dataset is derived from the Lean 4 adaptation of the miniF2F benchmark provided by DeepSeek-Prover-V1.5. In earlier versions, several formal statements contained errors that made them impossible to prove or logically inconsistent with their informal specifications.
To resolve this, the maintainers corrected multiple formalisations so that their formal hypotheses properly reflect their informal problem statements. The resulting test set was used to evaluate theorem provers such as Kimina-Prover.
How it was made
The dataset consists of formal theorem statements formulated in the Lean 4 interactive theorem prover, stored as text in Parquet format. It draws from mathematical competitions, including the AMC 12, AIME, and IMO, as well as problems from the MATH dataset.
Curation focused on identifying unprovable formalisations and aligning them with their original informal problem requirements. For example, missing constraints such as requiring an integer to be strictly positive (n > 0) rather than a general natural number (which includes zero) were explicitly added to ensure logical validity.
Key facts
- Modality
- Text
- Format
- Parquet
- Size
- Fewer than 1,000 examples
- Formal language
- Lean 4
- Category
- Theorem Proving
What you can use it for
- Automated theorem proving evaluation
- Benchmarking automated theorem provers and neural proof generation models, such as Kimina-Prover, on formal mathematical reasoning tasks.
- Mathematical reasoning evaluation
- Testing the formal problem-solving capabilities of systems across olympiad-level algebra, number theory, and analysis problems.
- Lean 4 benchmark verification
- Validating the soundness of formal problem specifications against their informal mathematical problem descriptions.
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/minif2f_test at the moment you asked. Nothing is cached or stored — every row above came from that request.
How the columns are distributed
Over 244 rows of default/train
formal_statement
string_text- min
- 203
- median
- 381
- mean
- 415.28
- max
- 1,042
informal_prefix
string_text- min
- 46
- median
- 140.50
- mean
- 182.36
- max
- 762
name
string_text- min
- 11
- median
- 17
- mean
- 19.36
- max
- 55
Strengths and limits
Good at
- Fixes flawed formal statements that were previously unprovable due to discrepancies with informal problem specifications.
- Standardised for evaluation in the Lean 4 theorem prover environment.
- Covers verified, competition-level mathematics problems from benchmarks including AMC, AIME, and IMO.
Watch out for
- Contains fewer than 1,000 test examples.
- Restricted to formal theorem statements tailored to Lean 4 syntax and libraries.
Questions
Can I look inside minif2f_test 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 minif2f_test under?
Its authors declare apache-2.0. Read the terms on the original page before reusing the data.
What is the origin of this dataset?
It is an improved version of the Lean 4 miniF2F test set previously provided by DeepSeek-Prover-V1.5, based on the original miniF2F formal mathematics benchmark.
What changes were introduced in this version?
Several erroneous formal statements were corrected to ensure they are mathematically provable, such as adding missing positivity conditions to natural number variables.
What types of problems are included?
The test set includes formalised competition mathematics problems, including items from AMC 12, AIME, the International Mathematical Olympiad (IMO), and algebra and number theory problems from the MATH dataset.
Which proof assistant is targeted?
The formal theorem statements in this repository are written for the Lean 4 interactive theorem prover.
How to cite it
Zheng, Kunhao, Jesse Michael Han, and Stanislas Polu. "MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics." arXiv preprint arXiv:2109.00110 (2021).
Written from minif2f_test'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.