What it measures
640+ William Lowell Putnam Mathematical Competition problems (1962–2023) formalized in Lean 4, Isabelle, and Coq.
Reading the measurement
Partial credit can distinguish a useful approach from an empty attempt, but it is not the same as a completed task. Read the rubric, full-success count and score distribution together. For mathematical work, preserve the difference between expert review and acceptance by a formal proof checker.
Published evaluation
Counts are divided by the published problem denominator and displayed as percentages. Formal systems remain separate.
Where this fits in an evaluation suite
Final-answer accuracy, proof credit, and expert-reviewed research progress are distinct signals. A proof-aware evaluation should retain partial work and audit strong claims.
Start with a capability hypothesis, then choose a second test with a different failure mode. Keep the checkpoint, reasoning effort, agent tools, sampling policy, and scoring procedure fixed when measuring a training intervention. Record failures and missing outputs in the denominator.
A reproducible comparison
Counts are divided by the published problem denominator and displayed as percentages. Formal systems remain separate.
Publish the exact run configuration, item coverage, score units, and available uncertainty. If a source supplies only an aggregate or a single run, preserve that limit. A new model name or a rounded score alone does not establish a capability improvement.
PRIMARY EVIDENCE & FURTHER READING
- PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition — published result table ↗
All 8 authors
George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, Swarat Chaudhuri
Reviewed 2026-10-26. Explanation and interpretation by RLTasks. Benchmark ownership remains with its original authors.