Source-linked AI summary
PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, Swarat Chaudhuri
TL;DR
Neural theorem proving lacks a broad, difficult, multilingual benchmark that tests competition mathematics without reducing solution-finding challenges. PutnamBench provides hand-constructed formalizations of Putnam problems across major proof assistants and evaluates existing approaches, which solve only a handful of problems. The benchmark therefore presents a difficult open challenge for automated mathematical reasoning.
Problem
Existing competition benchmarks have limitations in difficulty, mathematical breadth, language coverage, or framework currency, motivating a new benchmark for neural theorem proving.
Method
PutnamBench hand-constructs 1692 formalizations of 640 Putnam problems across Lean 4, Isabelle, and a substantial subset of Coq, while factoring out solutions where needed.
Results
Existing neural and symbolic theorem-proving approaches solve only a handful of PutnamBench problems.
Takeaways & Limitations
PutnamBench establishes a challenging open benchmark spanning broad undergraduate mathematics and multiple formal proof frameworks.
Takeaways & Limitations
The few problems solved by current methods are among the easiest Putnam problems, and significant advances in automated mathematical reasoning are required for broader progress.
Abstract
from arXiv · showhide
We present PutnamBench, a new multi-language benchmark for evaluating the ability of neural theorem-provers to solve competition mathematics problems. PutnamBench consists of 1692 hand-constructed formalizations of 640 theorems sourced from the William Lowell Putnam Mathematical Competition, the premier undergraduate-level mathematics competition in North America. All the problems have formalizations in Lean 4 and Isabelle; a substantial subset also has Coq formalizations. PutnamBench requires significant problem-solving ability and proficiency in a broad range of topics taught in undergraduate mathematics courses. We use PutnamBench to evaluate several established neural and symbolic theorem-provers. These approaches can only solve a handful of the PutnamBench problems, establishing the benchmark as a difficult open challenge for research on neural theorem-proving. PutnamBench is available at https://github.com/trishullab/PutnamBench.
1 Introduction
PUTNAMBENCH addresses limitations in existing neural theorem-proving benchmarks with a hand-curated, multilingual collection of difficult Putnam problems. Its broad undergraduate mathematical coverage and low success rates make it a challenging open evaluation benchmark.
- Existing benchmarks have limitations: MINIF2F includes many problems immediately solvable by SMT, while FIMO targets only the no-longer-maintained Lean 3.
- PUTNAMBENCH contains 1692 formalizations of 640 Putnam competition problems, with Lean 4 and Isabelle coverage for all problems and substantial Coq coverage.
- Putnam problems cover undergraduate topics such as analysis and abstract algebra that do not appear in the IMO, while success in the two competitions is correlated.
- PUTNAMBENCH is the first mathematics-competition benchmark to include problems in Lean 4, Coq, and Isabelle.
- Several neural and symbolic approaches solve only a handful of PUTNAMBENCH problems, establishing it as a hard open challenge for neural theorem proving.
2 Background
The background introduces machine-verifiable formal proof frameworks and situates PUTNAMBENCH among competition-based and formal theorem-proving benchmarks. The benchmark compares broad language support and difficult undergraduate-level competition problems while preserving factored solutions.
- Formal proof frameworks let users state mathematical theorems and write machine-verifiable proofs whose remaining proof state is tracked during proof construction.
- Figure 1 illustrates a Lean 4 formalization of Putnam 1988 B1 and its proof workflow using intro, use, linarith, and ring.
- The Putnam Competition consists of two three-hour sessions of six problems, covering varied undergraduate topics and requiring natural-language correctness proofs.
- PUTNAMBENCH provides Lean 4, Isabelle, and Coq support on difficult competition problems using undergraduate-level mathematics.
3 PUTNAMBENCH
PUTNAMBENCH is a manually produced, multi-language benchmark of Putnam problems designed to preserve solution-finding difficulty while supporting broad undergraduate mathematics and multiple proof assistants. Its formalization choices, language coverage, and evaluation setup target limitations in prior benchmarks, although library support constrains coverage of some domains.
- Benchmark scope: PUTNAMBENCH contains 1692 formalizations of 640 Putnam problems, including 640 formalizations in Lean 4 and Isabelle and 412 in Coq.The benchmark also incorporates informal statements and numerical solutions where applicable.
- Diversity and breadth: The benchmark covers undergraduate mathematics more broadly than competition benchmarks focused generally on high-school mathematics, while reflecting Putnam’s cross-field problem variety.The authors note that limited mathematical-library support restricts coverage of geometry and probability.
- Multiple languages: PUTNAMBENCH includes formalizations in Lean 4, Isabelle, and Coq, making it the first undergraduate-level competition benchmark for each language and the first human mathematics-competition benchmark for Coq.The formalizations use concepts from repositories including Mathlib, the HOL standard library, and Coquelicot.
- Release and contamination: PUTNAMBENCH supports Lean 4 on initial release, addressing a gap in prior benchmarks, while direct formal-proof contamination is unlikely although indirect transfer from informal proofs can occur.The benchmark is released under open-source licenses and includes informal statements with permission from the Mathematical Association of America.
- Factored solutions: Roughly 60% of Putnam problems require finding a closed-form solution and proving it correct, so PUTNAMBENCH separates candidate solutions from correctness proofs rather than writing solutions directly into theorem statements.Task 1 asks models to identify and prove a solution, whereas Task 2 supplies the solution and asks only for its proof; the authors argue this better reflects the informal difficulty.
- Construction: The benchmark was hand-crafted across several months, with each formalization verified by a second person at least once, and formalizations may not transfer directly across languages because their foundations differ.The authors report an average time-to-formalize of roughly 25 minutes per problem in one language.
4 Experimental Evaluation
PUTNAMBENCH evaluations across Lean 4, Isabelle, and Coq show that current neural and symbolic theorem-proving systems solve only a handful of problems. Performance is concentrated in Isabelle, while language compatibility, search limits, and problem difficulty constrain broader success.
- Experimental setup: All tested methodologies perform poorly, solving at most a handful of PUTNAMBENCH problems across the evaluated languages.The evaluation runs language-specific experiments with GPT-4, search-based systems, and symbolic automation using the pass@n metric.
- Lean 4: A single GPT-4 pass@10 evaluation solves one of 640 Lean 4 formalizations.The successful proof is for Putnam 1988 B1 and is found on the first of ten attempts.
- Lean 4: ReProver solves no Lean 4 problems with or without retrieval, while COPRA solves one problem, Putnam 1988 B1.COPRA finds a ten-line proof on its tenth GPT-4 query, whereas ReProver fails under standard LeanDojo search parameters.
- Isabelle: DSP produces four Isabelle proofs, including two that Sledgehammer alone cannot generate, while GPT-4 alone proves one Isabelle problem.DSP solves Putnam 2001 A1, 1971 B1, 1995 A1, and 1986 B1; Sledgehammer solves the three magma problems but no other formalization.
- Coq: Tactician and CoqHammer each produce no successful Coq proofs under their reported timeouts.The results indicate that the evaluated symbolic and learned Coq systems do not yet scale to these challenging olympiad-style problems.
- General analysis: Across all experiments, only 6 PUTNAMBENCH problems are successfully proven, and these are described as among the easiest Putnam problems.The authors conclude that significant advances in automated mathematical reasoning are required for substantial progress.
5 Related Work
Related benchmarks cover formal competition mathematics, informal mathematical reasoning, and automated theorem-proving methods. PUTNAMBENCH extends this landscape through undergraduate-level competition problems and support for Lean 4, Isabelle, and Coq.
- Formal benchmarks: MINIF2F, FIMO, Compfiles, and ProofNet provide formal mathematics benchmarks drawn mainly from competition problems or undergraduate curricula.MINIF2F spans several proof languages, FIMO contains Lean 3 IMO shortlist formalizations, and Compfiles and ProofNet include Lean formalizations of competition or undergraduate mathematics.
- Informal benchmarks: MATH and GSM8K benchmark informal natural-language mathematical reasoning using high-school and grade-school problem collections.These datasets provide natural-language problems rather than machine-checked theorem statements.
- Theorem-proving methods: Most recent formal theorem-proving systems combine neural proof-step prediction with a search mechanism that locates a valid proof.Earlier systems such as GPT-f synthesize proofs from data derived from formal mathematical libraries.
- Theorem-proving methods: Isabelle research leverages Sledgehammer for external automated reasoning and DSP for language-model-generated proof sketches.These systems combine Isabelle’s declarative proof framework with symbolic automation or neural generation.
- Theorem-proving methods: Coq supports both software verification and general mathematics, with Tactician providing online learning methods for proof search.The cited Tactician configuration uses an approximate nearest-neighbors approach based on locality-sensitive hashing.
6 Conclusion
PUTNAMBENCH is a multilingual benchmark spanning broad undergraduate mathematics, and experiments show that current theorem-proving approaches solve only a handful of its problems.
- PUTNAMBENCH covers undergraduate topics including algebra, analysis, and number theory across Lean 4, Isabelle, and Coq.
- All current theorem-proving approaches fail to solve more than a handful of PUTNAMBENCH problems.
- The paper attributes these failures to difficulty synthesizing and orchestrating new lemmas and leveraging mathematical knowledge repositories.
Checklist
The checklist reports that the paper supports its claims, discloses experimental and asset details, and discusses formalization limitations without theoretical results or human-subject research.
- The paper states that its main claims are supported in Sections 3 and 4.
- The authors report discussing challenges in formalizing geometry and probability because mathematical-library support varies across languages.
- The paper reports no theoretical results, human-subject research, crowdsourcing, or associated participant compensation.
- The experiments use open-sourced methods, disclose reproducibility information, and provide the dataset URL.
- The authors report no training, because the experiments rely on existing methods and calls to GPT-4.
A Appendix
The appendix presents formalizations of diverse Putnam problems in Lean 4, Isabelle, and Coq, illustrating repository dependencies, factored solutions, proof failures, and successful automated proofs.
- The appendix includes Coq formalizations relying on MathComp and Coquelicot, with Coq using Admitted as the equivalent of Lean’s sorry.
- Several Lean formalizations factor Boolean or numerical answers out of theorem statements when problems ask for decisions or witnesses.
- The examples show that formalization requires specifying underspecified types and may depend on libraries such as mathlib4, GeoCoq, or MathComp.
- GPT-4-generated proofs can fail through Lean-version syntax errors, incorrect algebraic assumptions, or wrong witness choices during search.
- The appendix notes that DSP’s LLM-synthesized informal proofs may introduce indirect dataset contamination, while generated sketches can also be more complex and erroneous than direct automation.
- Sledgehammer solves examples involving binary operations on sets, while DSP can require sketching beyond a single Sledgehammer invocation.