REVIEW 15 cited by
PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
Not yet reviewed by Pith; the record is open.
This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.
SPECIMEN: schema-true, not a live event
T0 review · schema-true
One-sentence machine reading of the paper's core claim.
pith:XXXXXXXX · record.json · timestamp
read the original abstract
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.
Forward citations
Cited by 15 Pith papers
-
CausalForge: A Formally Grounded, Self-Improving Agentic Framework for Automated Research in Causal Inference
CausalForge is a Lean-grounded, self-improving agentic framework that proposes, proves, and statement-audits causal inference theorems; its runs produced nine accepted results including a new ATE minimax upper bound.
-
Proof2Hybrid: Automatic Mathematical Benchmark Synthesis for Proof-Centric Problems
A fully automated pipeline produces proof-centric math benchmarks, demonstrated on algebraic geometry with 456 items, where leading LLMs score near 60 percent.
-
Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution
A verifier-grounded self-evolving Lean proof agent with a champion-driven, self-hardening benchmark reached 45.1% held-out miniF2F solve rate versus 32.0% for a fixed-benchmark baseline.
-
The Topological Dual of a Dataset: A Logic-to-Topology Encoding for AlphaGeometry-Style Data
The topological dual of a dataset is introduced as a transformation that encodes logical structures into topological ones to expose invariants in neural latent spaces for AlphaGeometry-style reasoning.
-
LeanTree: Accelerating White-Box Proof Search with Factorized States in Lean 4
White-box proof search with factorized Lean 4 goals reaches 18.4% on MiniF2F with Llemma-7B, outperforming black-box generation at 9.6%.
-
Mathesis: Towards Formal Theorem Proving from Natural Languages
An RL-trained autoformalizer plus a Lean prover solves 18% of Chinese Gaokao proof problems end-to-end from natural language, and 64.3% of MiniF2F at pass@32.
-
MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?
MATP-BENCH pairs 1,056 multimodal math problems with formal theorem statements in Lean 4, Coq, and Isabelle; the strongest tested model solves only 5.68% of Lean 4 end-to-end proving tasks at pass@10.
-
Decomposing Elements of Problem Solving: What "Math" Does RL Teach?
Reinforcement learning (GRPO) on math LLMs primarily increases execution robustness on already-solvable problems, not planning or coverage of new problems.
-
Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving
An open-source theorem-proving model reaches state-of-the-art scores on miniF2F (57.6% Pass@32) and PutnamBench by training on 800K formal proofs synthesized through autoformalization and expert iteration.
-
Question Begets Question: Self-Evolving Curriculum for Reinforcement Fine-Tuning on Competition Mathematics
A self-evolving curriculum that retrains a language model on variants of problems it can mostly get right lifts AIME pass@1 from 5.6% to 16.5%, beating static augmentation under the same data budget.
-
LeanFlow: A Case Study in Workflow-Driven Lean Autoformalization
Workflow control and a cached Lean verifier improve completion and token efficiency in document-to-project autoformalization.
-
FMC: Formalization of Natural Language Mathematical Competition Problems
An LLM-based error-feedback pipeline produces FMC, a dataset of 3,922 Olympiad problems aligned with 9,787 Lean statements, claimed to be a challenging ATP benchmark.
-
Leanabell-Prover-V2: Verifier-integrated Reasoning for Formal Theorem Proving via Reinforcement Learning
Verifier-integrated reinforcement learning with multi-turn reflection improves 7B-scale Lean 4 theorem proving by 2 to 3 points on MiniF2F at pass@128.
-
LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving
LeanConjecturer automatically generates thousands of Lean 4 theorem statements from Mathlib files and uses them for reinforcement learning, with modest measured gains on held-out problems.
-
Formally Solving Answer-Construction Problems in Lean
ECP, an enumerate-conjecture-prove framework with Lean verification, improves answer-construction accuracy on ConstructiveBench and a PutnamBench subset, but its benchmark has a 17% major-error rate and its abstract r...
Discussion (0). Continue with ORCID to comment.