PutnamBench

What it measures

Formal theorem-proving on Putnam problems — models write a complete Lean/Isabelle/Coq proof, machine-checked by the proof assistant's kernel.

Primary metric

problems with a complete, kernel-verified formal proof — Lean subset (count / 672)

Judge model

not judged by a model

Human baseline

—not reportedNo usable human baseline, and the mismatch is starker than anywhere else on the wiki. The Putnam is famously brutal: the median score among the elite students who sit it is often 0 or 1 out of 120 (in 2024, ~40% of ~4,000 entrants scored 0–1; only 5 perfect scores in 85 years). But humans solve Putnam INFORMALLY, under a 6-hour limit, with no machine — while PutnamBench requires a COMPLETE FORMAL proof, with no time limit and a proof assistant. Humans and machines are not doing the same task, so a direct baseline comparison is more strained here than for any answer-based benchmark (cf. AIME's 'low even for excellent humans' point, taken further). Hence null, not a number.

Languages

English

Health

Scores are per-language and per-variant, and the totals grow as new Putnam years are formalized (a living benchmark — see Task details), so cite the denominator and 'as of' date. The dominant confound is NOT sampling noise but COMPUTE/SAMPLING BUDGET: results span pass@10 to pass@512-and-beyond, plus GPU-days-per-problem agentic runs, and these differ by tens of percentage points on the same benchmark. A special-purpose system at pass@512 and a general model at pass@1 solving similar counts are very different achievements. The leaderboard itself notes it is seeking a better way to indicate differing budgets.

Status evidence

The wiki's first formal-proving benchmark and, for reasonable budgets, still far from solved. Through most of 2024–2025 the best systems solved single digits of the Lean set (Goedel-Prover 7 at pass@512; GPT-4o ~1). General reasoning models at pass@1 remain low (GPT-5 ReAct ~28–42 of ~660, single digits %). Heavy-compute systems have since climbed steeply — ByteDance's Seed-Prover reportedly ~581/672 Lean at ~10 GPU-days per problem, and in Jan 2026 Logical Intelligence's Aleph CLAIMED 668/672 (99.4%, agentic pass@1) topping the board — but these use enormous or single-source, unreproduced budgets, and the Isabelle/Coq subsets and the harder 'no-answer' variant remain far less attacked. What would move this to nearing-saturation: independent reproduction of high solve rates across languages under disclosed, comparable budgets.

Saturated since

not saturated

Refresh cycle

static

Test set public

yes

A genuinely different contamination profile from every answer-based maths page. The formalizations are hand-crafted (not scraped text), and the formal PROOFS are not published as a solution set the way GSM8K/MATH worked solutions are — so the usual leakage vector is weaker. Crucially, the formal-proof requirement makes memorization far less useful: you cannot shortcut a kernel-checked Lean proof by recalling a number or a memorized informal argument. Working the other way: the Putnam problem STATEMENTS are public and decades of informal solutions circulate widely, which can leak proof strategies. Net: medium, effectively toward the low end — lower than any answer-based maths benchmark here, but not FrontierMath-low, because the statements are so public.

Models scored on this benchmark

The reverse lookup, which is this site’s addition: every model here with a score on this benchmark. Independent measurements and vendor-reported numbers are kept apart rather than interleaved, because they are different claims.

No model on this site has a score on this benchmark yet. That usually means the models that were measured on it are not in the registry, rather than that nobody has run it.

Trajectory

Where results are tracked

Leaderboards benchwiki lists for this benchmark. These are links out, not sources this site ingests — no score below comes from any of them.

• PutnamBench leaderboard (official / canonical live tracker)official