Research map / Large language models / Agents, code and math
PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Introduces PutnamBench, a hand-built multi-language (Lean 4, Isabelle, Coq) benchmark of 1692 formalizations of 640 Putnam competition theorems, and evaluates GPT-4, COPRA, ReProver, DSP, Sledgehammer, Tactician and CoqHammer, which solve only a handful.
Problem
Existing neural theorem-proving benchmarks (MiniF2F, FIMO, ProofNet) are limited in difficulty breadth, cover only a subset of proof assistants, and risk contamination; there is no undergraduate-level competition benchmark spanning Lean 4, Isabelle, and Coq.
Approach
Hand-formalize Putnam competition problems in Lean 4, Isabelle, and Coq, factoring numerical solutions out of theorem statements so that solution finding and proof are both tested, and evaluate off-the-shelf neural and symbolic provers on it.
Key results
- Across all languages, only 6 problems in PutnamBench are solved in total by the evaluated methods.
- In Isabelle, DSP solves 4/640 and Sledgehammer solves 3/640 problems.
- In Lean 4, GPT-4 (pass@10), COPRA, and ReProver solve at most 1/640; in Coq, GPT-4 and COPRA solve 1/412.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| add retrieval to ReProver (ablation) | ReProver on Lean 4 · PutnamBench Lean 4 | success rate: 0/640 -> 0/640 | No clear effect |
| use DSP instead of Sledgehammer alone | Isabelle theorem proving · PutnamBench Isabelle | success rate: 3/640 -> 4/640 | Helped |
| use Sledgehammer instead of GPT-4 alone | Isabelle theorem proving · PutnamBench Isabelle | success rate: 1/640 -> 3/640 | Helped |
Surprising findings
- GPT-4 frequently outputs Lean 3 syntax even when instructed to produce Lean 4.
- Sledgehammer alone solves problems that GPT-4 cannot, and symbolic automation outperforms the LLM in Isabelle.
Limitations
- Few geometry and probability problems can be formalized due to limited library support.
- Evaluated methods are off-the-shelf and not tailored to multi-language proving; GPT-4 evaluations limited by query cost.
- Possible indirect contamination via informal proofs in LLM pretraining data.
Experimental setup
Datasets: Putnam competition problems
Benchmarks: PutnamBench
Metrics: pass@n success rate
Baselines: GPT-4 COPRA ReProver DSP Sledgehammer Tactician CoqHammer
Builds on: MiniF2F FIMO ProofNet LeanDojo Draft-Sketch-Prove
Closest papers by meaning
- LEGO-Prover: Neural Theorem Proving with Growing Libraries (ICLR 2024 · similarity 0.90)
- miniCTX: Neural Theorem Proving with (Long-)Contexts (ICLR 2025 · similarity 0.88)
- Putnam-AXIOM: A Functional & Static Benchmark for Measuring Higher Level Mathematical Reasoning in LLMs (ICML 2025 · similarity 0.88)
- ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · similarity 0.87)
- Alchemy: Amplifying Theorem-Proving Capability Through Symbolic Mutation (ICLR 2025 · similarity 0.87)
- Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning (ICLR 2025 · similarity 0.87)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.