PutnamBench
Can an automated prover produce a machine-checked formal proof, not just a numeric answer, for a Putnam Competition problem?
UT Austin (Tsoukalas, Chaudhuri et al.)Released 15 July 2024Live
PutnamBench tests something narrower and harder than getting a maths problem’s answer right: it asks a formal theorem prover to produce a complete, machine-checked proof of a problem from the William Lowell Putnam Mathematical Competition, the premier undergraduate maths contest in North America. Built by George Tsoukalas, Swarat Chaudhuri and colleagues at UT Austin and published in mid-2024, the benchmark hand-translates competition problems into equivalent theorem statements in three proof assistants at once — Lean 4, Isabelle and Coq — so a system’s proof, once accepted, is verified by the same rigorous checker mathematicians use, not by comparing a final number to an answer key. At launch, the paper reported that existing neural provers “can only solve a handful” of its problems.
That gap closed fast as labs turned reinforcement learning on formal proving. DeepSeek’s DeepSeek-Prover-V2-671B solved 49 of 658 Lean problems in April 2025; months later, ByteDance’s Seed-Prover system passed 50% using heavier inference, and Goedel-Prover-V2 took the open-weight lead by solving 86 problems with a model a twentieth of DeepSeek’s size. By December 2025, Seed-Prover 1.5 reported solving 88% of the benchmark and 11 of the 12 problems on the live 2025 Putnam competition within nine hours — a jump from single digits to near-completeness in under eighteen months.
The pace of that climb has made PutnamBench a proving ground for a wider claim: that formal, machine-checked reasoning, once a narrow academic niche, is now tractable at scale for large language models paired with search. Because a PutnamBench proof cannot be faked past its checker, the benchmark has become a harder-to-game companion to informal maths tests, and labs increasingly report results on graduate- and research-level successors — Seed-Prover’s own paper introduced two such follow-ons, Fate-H and Fate-X — as PutnamBench itself approaches saturation.
The set
Hand-written formalizations of problems from the William Lowell Putnam Mathematical Competition, given in parallel across Lean 4, Isabelle and Coq (1,724 formalizations of 640-plus theorems as of 2026, spanning 1962-2025); a submission counts only if the theorem prover closes the formal proof obligation, so guessing the final numeric answer without deriving it is not credited.
Example
PutnamBench's own docstring for Putnam 1962 A1: "Given five points in a plane, no three of which lie on a straight line, show that some four of these points form the vertices of a convex quadrilateral." Formalized in Lean 4 as: theorem putnam_1962_a1 (S : Set (ℝ × ℝ)) (hS : S.ncard = 5) (hnoncol : ∀ s ⊆ S, s.ncard = 3 → ¬Collinear ℝ s) : ∃ T ⊆ S, T.ncard = 4 ∧ ¬∃ t ∈ T, t ∈ convexHull ℝ (T \ {t})raw.githubusercontent.com
Where it stands
State-of-the-art rose from single digits in 2024 to a majority of problems by late 2025 as labs applied large-scale reinforcement learning to formal proving; the leaderboard tracks Lean, Isabelle and Coq separately.
How the top score changed hands
- July 2024Contemporary provers at launcha handful of problemsThe paper reported that existing neural theorem-proving approaches "can only solve a handful of the PutnamBench problems."
- April 2025DeepSeek-Prover-V2-671B49 of 658Reported alongside an 88.9% pass ratio on miniF2F-test; DeepSeek's paper describes the model closing the gap between formal and informal mathematical reasoning.
- July 2025Seed-Prover 1.0 (ByteDance)over 50%Achieved with heavier inference; the same paper reported the system essentially saturating miniF2F and proving 78.1% of formalized past IMO problems.
- August 2025Goedel-Prover-V2-32B86 of 658 (pass@184)Best result among open-weight models, nearly double DeepSeek-Prover-V2's open-weight record, using a 32B model at a twentieth of DeepSeek's parameter count.
- December 2025Seed-Prover 1.5 (ByteDance)88%
Current best: Seed-Prover 1.5 (ByteDance) — 88% Also solved 11 of 12 problems from the live Putnam 2025 competition within nine hours; reported in the same paper alongside 80% on the harder Fate-H set and 33% on PhD-level Fate-X.