PutnamBench
In plain wordsA 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.
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. whose problems come from the William Lowell Putnam Mathematical Competition, the most prestigious mathematics contest for university students in the United States and Canada. The 2024 release covered 640 Putnam problems from 1962 to 2023 with roughly 1,700 hand-written formal statements: every problem in 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. 4 and Isabelle, and a large share also in Coq (now RocqRocq, prop. n.: A long-established computer system, known until 2025 as Coq, in which people write mathematical proofs and verified software that the computer checks step by step.); problems from later competitions have since been added. The problems span analysis, linear and abstract algebra, number theory, combinatorics, probability and geometry, and many require undergraduate theory, drawn in Lean from 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., rather than the mostly high-school material of miniF2FminiF2F, prop. n.: A 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 problem counts as solved only when the proof checker accepts the output. At release the best systems proved only a handful of problems; during 2025, provers combining large reasoning models with proof-checker feedback, search and decomposition into lemmas raised the share to a majority, making PutnamBench a main yardstick for formal provers once miniF2F saturated.
The new prover clears most of miniF2F, so we report PutnamBench, where it solves about a third.
Origin
Introduced in July 2024 by George Tsoukalas and colleagues in Swarat Chaudhuri's group at the University of Texas at Austin, and presented in the NeurIPS 2024 Datasets and Benchmarks track. The maintainers keep a public leaderboard and correct statements found to be misformalized.
Usage note
Scores refer to particular versions and proof languages of the benchmark and are often obtained with very different compute budgets, so leaderboard numbers are not always directly comparable.
Related
- miniF2FminiF2F, prop. n.: A 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.
- 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.
- 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.
- 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
- Tsoukalas, G. et al. (2024). PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition. NeurIPS 2024 Datasets and Benchmarks Track. arXiv:2407.11214. arxiv.org/abs/2407.11214
Mentioned in
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., miniF2FminiF2F, prop. n.: A 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.