PutnamBench

Overview

PutnamBench is the first benchmark on this wiki that does not grade an answer — it grades a proof. Every prior maths entry, all the way up the ladder (GSM8K → MATH → AIME → FrontierMath), checks a final number or expression: is the boxed answer right? PutnamBench, built by Tsoukalas et al. (UT Austin) and released in July 2024, asks for something categorically harder and cleaner to verify: a complete formal proof, written in a proof assistant — Lean 4, Isabelle, or Coq — whose correctness is confirmed deterministically by the proof assistant’s kernel. Not string match, not an equivalence checker, not an LLM judge: a machine mechanically verifies that the proof is valid, step by step, from the axioms.

That single design choice makes PutnamBench a formal theorem-proving benchmark — a genuinely new sub-area for this wiki, distinct from the answer-checking maths pages, and the opening of a benchmark family that includes miniF2F (high-school level) and ProofNet (undergraduate textbook level). Its problems are manually-constructed formalizations of the William Lowell Putnam Competition — the premier North American undergraduate math competition, famous for being brutally hard even for elite students. As of 2026-07-22 the (living, versioned) benchmark holds 1,724 formalizations across the three languages (672 Lean 4, 640 Isabelle, 412 Coq), spanning Putnam years 1962–2025, with the original English problem statements included by permission of the MAA.

The correctness guarantee is the point. A kernel-checked Lean proof is not gameable the way an answer is: you cannot luck into it, memorize a number, or talk a judge into accepting it. So when a PutnamBench proof verifies, the model genuinely proved the theorem. That also makes the benchmark’s story unusually honest about budget: for most of 2024–2025, the best systems solved only single digits of the 600+ Lean problems, and general reasoning models did poorly — the archetypal far-from-solved frontier. That has begun to change with enormous compute and agentic systems (see status and Known issues), including a striking, very recent, single-source claim (Aleph, 99.4% of the Lean set) that would reshape the picture if it reproduces. Whether formal proving is “nearly solved” or “barely started” depends entirely on which language, which variant, and — above all — which compute budget you mean.

Task details

Each item is a Putnam problem formalized as a theorem statement in a proof assistant; the model must produce a proof that the assistant accepts. The benchmark has structure worth stating precisely:

Three languages: Lean 4 (672 formalizations), Isabelle (640), Coq (412) — 1,724 total. The same underlying Putnam problems are formalized in each, but the subsets and tooling differ, so per-language scores are not comparable (Isabelle’s Sledgehammer / SMT automation historically closed more goals than early Lean approaches, for instance). The Lean set is the primary leaderboard configuration, which is why this page’s dataset.size is 672.
Two variants: (a) prove the theorem with the numerical answer already written into the statement, and (b) the harder “no-answer” variant, where the system must also determine the answer before proving it. The leaderboard tracks these separately — and as of this writing the no-answer board is empty: no method has been benchmarked on it.
Living / versioned. The paper reported ~640 theorems / ~1,697 formalizations (Putnam 1962–2023); the set has since grown to the current totals (through 2025). Always cite the denominator and an “as of” date — a first-class concern here.
Input: a formal theorem statement (plus, in variant b, the task of finding the answer).
Output: a formal proof, machine-checked. Verified or not — no partial credit.

The canonical repo is trishullab/PutnamBench (leaderboard + results.json); it asks contributors to coordinate before submitting proofs for subsets — a mild contribution protocol, not an access gate.

Example

A PutnamBench item is a formalized Putnam problem — for instance, a statement (in Lean 4) that a certain sum equals a given closed form, or that some configuration is impossible. The model’s job is not to state the answer but to derive it formally:

theorem putnam_example (n : ℕ) (hn : 0 < n) : ... := by
  -- the model must produce tactics that close every goal;
  -- Lean's kernel checks the result. If it type-checks, the theorem is proved.

The difference from MATH or AIME is total: there, a model writes “the answer is 42” and a checker compares 42 to the key. Here, a model must construct the entire logical argument, and a proof assistant — not a string comparison — certifies it. That is why PutnamBench cannot be gamed by memorizing answers, and why it is the strongest correctness guarantee in the wiki (see Scoring methodology).

Scoring methodology

Grading is machine-checked formal verification: the proof assistant’s kernel deterministically confirms the proof is valid. This is a stronger correctness guarantee than anything earlier in the wiki. Answer-matching (GSM8K, MATH) credits a right number reached by wrong or memorized reasoning; equivalence-checking (MATH) and LLM-judge grading (SimpleQA, HLE) are imperfect and, for judges, drift and can be argued with. A kernel-verified Lean proof is none of these: it is correct or it does not compile.

Schema note (flagged). This grading mechanism has no exact match in the scoring enum. It is emphatically not exact-match (nothing is string-compared). The closest existing value is unit-tests — because both are deterministic machine verification of correctness by a checker (there a test harness, here a proof kernel), the same category and equally ungameable-by-matching — so this page uses unit-tests. But formal proving deserves its own formal-verification value; the “second benchmark imminent” bar this wiki set for scoring extensions is already met, since miniF2F and ProofNet (both formal, both real) will re-raise it. The value should be added when the second formal-proving page lands, not for one page.

The budget trap — the headline caveat. Because a proof either verifies or not, systems throw sampling and compute at the search, and the budgets vary wildly: pass@10, pass@512, “pass@thousands,” or GPU-days per problem. A “solved N problems” figure is close to meaningless without the budget. This is the formal-proving analogue of AIME’s sampling-convention trap, but more extreme — the leaderboard itself notes it is looking for a better way to indicate differing budgets. run_config.pass_at is left null here precisely because there is no single convention; always report the budget.

Tools are constitutive. tools: true here does not mean the optional calculator/browser of the answer-based benchmarks — it means the proof assistant itself, without which a checked proof is impossible. “Tools off” is incoherent for formal proving. Read the sidebar’s tools: true accordingly: it is a statement about the medium, not an optional aid.

What it doesn’t measure

PutnamBench measures formal theorem-proving on undergraduate competition mathematics — a narrow, deep slice. It is not general reasoning, and not the answer-computation the rest of the maths ladder tests. Even within proving, it is bounded: Putnam-level problems, formalized with a checkable proof, in three specific proof assistants. It says nothing about research-level open problems (that is closer to FrontierMath’s answer-based frontier, and to open-problem proving generally), nor about informal mathematical reasoning as humans practice it. And because the compute budgets vary so much, a headline solve count reflects a system-plus-budget, not a model’s standalone ability. It is English-statement-based (with formal targets), and the no-answer variant — arguably the more honest test of mathematical ability — is essentially unmeasured so far.

Known issues & criticisms

Budget non-comparability (first-order). As in Scoring methodology: pass@10 vs pass@512 vs GPU-days-per-problem swing results by tens of points. Any comparison across systems that does not match budgets is close to meaningless — the single biggest source of misleading PutnamBench claims.
The recent heavy-compute / single-source frontier. The picture changed fast in late 2025–early 2026. ByteDance’s Seed-Prover reportedly solved ~581/672 Lean problems at roughly 10 GPU-days per problem (independent, on the leaderboard). Then in January 2026 Logical Intelligence reported its Aleph system solved 668/672 (99.4%) of the Lean set — agentic, one attempt per problem but at ~$68 average ($1,400 cap) compute — topping the leaderboard ahead of ByteDance and Apple, and providing verified counterexamples fixing 15 (~2%) malformed formalizations, which the PutnamBench team confirmed. What is established: the counterexample fixes were checked by the PutnamBench team, and verified proofs are Lean-kernel-checked in principle. What is not yet established: independent reproduction, comparison under matched budgets, and whether it generalizes beyond the Lean subset. It is a single-source (company-blog), very recent result a generation ahead of every other entry — a claimed frontier result that would change the picture if it holds and is widely reproduced, which is why the status here remains active rather than saturated.
Per-language incomparability. Lean/Isabelle/Coq have different subset sizes and automation strengths; a score in one language does not transfer to another.
Public statements. Putnam problems and informal solutions are extremely public (see Contamination) — a partial leakage vector even though formal proofs are not published.
No-answer variant unmeasured. The harder, more meaningful variant has no benchmarked methods yet.

Contamination notes

Risk: medium, and structurally unlike every answer-based maths page — effectively toward the low end. Two features suppress the usual leakage. First, the formalizations are hand-crafted, not scraped, and the formal proofs are not released as a solution set the way GSM8K/MATH worked solutions are, so there is far less “answer key” to memorize. Second, and more fundamentally, the formal-proof requirement makes memorization nearly useless: you cannot shortcut a kernel-checked Lean proof by recalling a number or even a memorized informal argument — the proof must actually verify. This is a real, qualitative difference from the answer-based benchmarks, where a leaked number is a free point. Pushing risk up: the Putnam problem statements are public, and decades of informal solutions circulate widely, which can leak proof strategies (especially for the answer-in-statement variant). Net assessment: lower than any answer-based maths benchmark here, but not as low as FrontierMath’s private held-out set, because the statements are so public. The paper includes its own dataset-contamination discussion.

How to run it

Use the official repo, and — non-negotiably — report your budget:

git clone https://github.com/trishullab/PutnamBench
# Lean 4 (672) / Isabelle (640) / Coq (412) formalizations + results.json
# Prove theorems with your system; the proof assistant's kernel verifies them.
# Leaderboard + submission info: https://trishullab.github.io/PutnamBench/leaderboard.html

When citing a PutnamBench result, always state: the language (Lean/Isabelle/Coq), the variant (answer-in-statement vs no-answer), the denominator and as-of date (the set grows), and — above all — the compute/sampling budget (pass@k, GPU-time, or agentic cost). A bare “solved 92% of PutnamBench” omits all five and is not interpretable.

History & lineage

2024-07 — PutnamBench released (Tsoukalas et al., UT Austin; arXiv:2407.11214; NeurIPS 2024 D&B, ICML 2024 AI4Math Best Paper). Best systems solve single digits of the Lean set; GPT-4o solves ~1. It opens formal theorem-proving as a frontier benchmark.
2025 — Specialized neural provers improve but stay low at reported budgets (e.g. Goedel-Prover 7/644 at pass@512). General reasoning models (o-series, DeepSeek-R1) do poorly; a general model reaching tens of problems at pass@1 (GPT-5) is itself notable.
late 2025 — Heavy-compute systems climb steeply: ByteDance’s Seed-Prover reportedly ~581/672 Lean at ~10 GPU-days per problem — the first sign the Lean set is tractable with enough compute.
2026-01 — Logical Intelligence reports Aleph at 668/672 (99.4%) on the Lean set, topping the leaderboard and fixing 15 malformed formalizations (verified by the PutnamBench team) — a striking, single-source, unreproduced result.

PutnamBench has no successor (successor is null): it sits alongside miniF2F (high-school) and ProofNet (undergraduate) as the first cluster of a formal-proving benchmark family in this wiki. Those are peers spanning difficulty levels, not derivatives — the wiki currently surfaces them via lineage.variants for cross-linking, which is an imperfect fit (they are siblings, not variants) and is itself evidence that a proper grouping mechanism for sub-areas is overdue.

Performance over time