mlsanityData to 7 Oct 2026

PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition

arXiv 2407.11214 ↗First posted 15 Jul 2024cs.AI cs.CL cs.LGcited by 153

Not on the map. Why?

Cited by 64 in LLM reasoning, but placed by its own abstract, which didn’t fit.

Abstract (arXiv)

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.

Key facts. Cited by 153 papers in the map (data through 7 Oct 2026). Builds on 15 of its 57 references that are in the map. First posted on arXiv 15 Jul 2024.

Builds on

15 of 57 references.

References · 15

  1. 2021Training Verifiers to Solve Math Word Problemscited by 9,743
  2. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  3. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  4. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  5. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  6. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  7. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  8. 2019The Lean mathematical librarycited by 127
  9. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  10. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  11. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 78
  12. 2023Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Provingcited by 37
3 more
  1. 2019Generating Correctness Proofs with Neural Networkscited by 36
  2. 2024Graph2Tac: Online Representation Learning of Formal Math Conceptscited by 15
  3. 2021Online Machine Learning Techniques for Coq: A Comparisoncited by 7

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 5; 2025: 67; 2026: 81.

153 papers.

Sort:

By area:

  1. 2025MathArena: Evaluating LLMs on Uncontaminated Math Competitionscited by 275
  2. 2024FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AIcited by 227
  3. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
  4. 2025Chain-of-Thought Reasoning In The Wild Is Not Always Faithfulcited by 166
  5. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  6. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  7. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 96
  8. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  9. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 77
  10. 2025Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiadcited by 72
  11. 2025Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Modelscited by 65
  12. 2025MegaScience: Pushing the Frontiers of Post-Training Datasets for Science Reasoningcited by 56
38 more
  1. 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
  2. 2025FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Modelscited by 45
  3. 2024ErrorRadar: Benchmarking Complex Mathematical Reasoning of Multimodal Large Language Models Via Error Detectioncited by 37
  4. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experiencecited by 36
  5. 2024LeanAgent: Lifelong Learning for Formal Theorem Provingcited by 34
  6. 2025Theoretical Physics Benchmark (TPBench) -- a Dataset and Study of AI Reasoning Capabilities in Theoretical Physicscited by 33
  7. 2025CombiBench: Benchmarking LLM Capability for Combinatorial Mathematicscited by 28
  8. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 28
  9. 2025The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofscited by 27
  10. 2025Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physicscited by 27
  11. 2025Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learningcited by 26
  12. 2025ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Datacited by 23
  13. 2025FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levelscited by 23
  14. 2024Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchicallycited by 22
  15. 2025Solving Inequality Proofs with Large Language Modelscited by 21
  16. 2025ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimizationcited by 18
  17. 2025A benchmark for vericoding: formally verified program synthesiscited by 16
  18. 2025StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusioncited by 15
  19. 2025MatSciBench: Benchmarking the Reasoning Ability of Large Language Models in Materials Sciencecited by 15
  20. 2025Mathesis: Towards Formal Theorem Proving from Natural Languagescited by 14
  21. 2025Reliable Fine-Grained Evaluation of Natural Language Math Proofscited by 14
  22. 2025MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?cited by 13
  23. 2025miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forwardcited by 13
  24. 2026A Minimal Agent for Automated Theorem Provingcited by 13
  25. 2026AI co-mathematician: Accelerating mathematicians with agentic AIcited by 13
  26. 2025Humanizing Machines: Rethinking LLM Anthropomorphism Through a Multi-Level Framework of Designcited by 11
  27. 2025IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generationcited by 11
  28. 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworkscited by 11
  29. 2025Decomposing Elements of Problem Solving: What "Math" Does RL Teach?cited by 10
  30. 2025Generalized Tree Edit Distance (GTED): A Faithful Evaluation Metric for Statement Autoformalizationcited by 9
  31. 2025Putnam-AXIOM: A Functional and Static Benchmark for Measuring Higher Level Mathematical Reasoning in LLMscited by 9
  32. 2025Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalitiescited by 8
  33. 2025An Investigation of Robustness of LLMs in Mathematical Reasoning: Benchmarking with Mathematically-Equivalent Transformation of Advanced Mathematical Problemscited by 8
  34. 2025DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theoremscited by 8
  35. 2026Riemann-Bench: A Benchmark for Moonshot Mathematicscited by 8
  36. 2025Autoformalizer with Tool Feedbackcited by 7
  37. 2025Lean Finder: Semantic Search for Mathlib That Understands User Intentscited by 7
  38. 2026LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematicscited by 7

50 most cited of 153 All 153 (JSON)