miniF2F
In plain wordsA test of 488 math problems, mostly from competitions, written in a form a computer can check, used to measure how well AI systems produce proofs that are verified automatically.
A benchmarkbenchmark, n.: A fixed, shared test — a set of questions or tasks with an agreed way of scoring — used to compare AI systems with one another and to track progress over time. for formal theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement. made of 488 hand-formalized problem statements, split evenly into validation and test sets. The problems come from US competitions (the American Mathematics Competitions, AMC, and the American Invitational Mathematics Examination, AIME), the International Mathematical Olympiad (IMO), the MATH dataset and school and university courses, and they were formalized for LeanLean, prop. n.: A programming language and proof checker in which mathematicians write proofs that the computer verifies line by line. It has become the main language in which AI systems produce checkable proofs. and Metamath in full and for Isabelle and HOL Light in part, so that provers built on different systems could be compared. A problem counts as solved only when the system outputs a proof that the checker accepts, and results are usually reported as pass@k, the share of problems solved within k attempts. Reported Lean test-set results rose from about 30 percent at release to above 90 percent in 2025, effectively saturating the benchmark and shifting attention to harder suites such as PutnamBenchPutnamBench, prop. n.: A test built from hundreds of problems from the Putnam, North America's top university math contest, written in a form a computer can check, used to measure how well AI systems prove harder mathematics.. Audits found errors in some original formalizations, including unprovable or trivially easy statements, and several groups now use corrected versions.
Our prover solves most of miniF2F-test at pass@32, but nearly all the gains are on the easier algebra items.
Origin
Released in 2021 by Kunhao Zheng, Jesse Michael Han and Stanislas Polu, working with OpenAI, as a shared cross-system benchmark for neural theorem proving, and published at ICLR 2022. 'F2F' stands for formal-to-formal: both the problem and the proof are formal. Community ports moved it to Lean 4 after the Mathlib migration.
Usage note
Because the formal statements of numerical questions already contain the answer, solving one shows that a system can prove an answer correct, not that it can find the answer.
Related
- LeanLean, prop. n.: A programming language and proof checker in which mathematicians write proofs that the computer verifies line by line. It has become the main language in which AI systems produce checkable proofs.
- MathlibMathlib, prop. n.: A huge shared library of mathematics written in the Lean language, in which every definition and proof has been checked by computer. Mathematicians keep extending it, and AI proof systems are trained on it.
- PutnamBenchPutnamBench, prop. n.: A test built from hundreds of problems from the Putnam, North America's top university math contest, written in a form a computer can check, used to measure how well AI systems prove harder mathematics.
- automated theorem provingautomated theorem proving, n.: Getting computers to prove mathematical or logical statements by themselves, by searching for a chain of valid steps that leads from basic assumptions to the statement.
- benchmarkbenchmark, n.: A fixed, shared test — a set of questions or tasks with an agreed way of scoring — used to compare AI systems with one another and to track progress over time.
- AlphaProofAlphaProof, prop. n.: A Google DeepMind system that learned to write computer-checked mathematical proofs by trial and error. In 2024 it helped an AI reach silver-medal level at the International Mathematical Olympiad for the first time.
- International Mathematical OlympiadInternational Mathematical Olympiad, prop. n.: The world's top math competition for high-school students. Because its problems demand creative written proofs, not just answers, earning a gold medal there became a famous test of AI reasoning, first passed in 2025.
- benchmark saturationbenchmark saturation, n.: When the best AI systems score so close to the maximum on a test that it can no longer tell them apart or show further progress.
Sources
- Zheng, K., Han, J. M. & Polu, S. (2022). MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics. ICLR 2022. arXiv:2109.00110.
Mentioned in
International Mathematical OlympiadInternational Mathematical Olympiad, prop. n.: The world's top math competition for high-school students. Because its problems demand creative written proofs, not just answers, earning a gold medal there became a famous test of AI reasoning, first passed in 2025., MathlibMathlib, prop. n.: A huge shared library of mathematics written in the Lean language, in which every definition and proof has been checked by computer. Mathematicians keep extending it, and AI proof systems are trained on it., PutnamBenchPutnamBench, prop. n.: A test built from hundreds of problems from the Putnam, North America's top university math contest, written in a form a computer can check, used to measure how well AI systems prove harder mathematics.