Primary evidence
- PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical CompetitionS1 · Primary research · Paper · 2024-07-15
- PutnamBench formal benchmark repositoryS1 · Primary research · Repository
PutnamBench raises formal theorem-proving evaluation to Putnam-level mathematics
Initial neural and symbolic provers solved only a handful of benchmark problems, making the collection a high-difficulty target for formal reasoning.
What happened?
PutnamBench released 1,692 hand-constructed formalizations of 640 Putnam theorems in Lean 4 and Isabelle, with a substantial Coq subset.
Why it matters
It shifted formal theorem-prover evaluation from high-school Olympiad problems toward broad advanced undergraduate mathematics.
Significance rationale: PutnamBench created a difficult multi-system benchmark from the premier North American undergraduate mathematics competition and exposed a large capability gap.
Historical context
Earlier developments
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- Computation only
- Formal assurance
- Artifact available
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- Automated theorem provers are evaluated on the formalized Putnam problems.
- Human contribution
- Researchers hand-formalized competition problems across multiple proof assistants and built the benchmark.
- Verification
- Paper released · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-11
Technical details
- Systems
- putnambench, lean, isabelle, coq
- Organizations
- university-of-texas-at-austin
- Problems
- putnam-competition
- Methods
- benchmarking, formalization
Sources & artifacts
- PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical CompetitionS1 · Primary research · Paper · accessed 2026-09-10
- PutnamBench formal benchmark repositoryS1 · Primary research · Repository · accessed 2026-09-11
- PutnamBench Lean, Isabelle and Coq formalizationsArtifact · Dataset
Verification history
- 2024-07-15 · Paper released · E2 · Research record
The Chronicle records this event from the cited primary or official source; the status does not imply independent Chronicle verification.
- 2026-09-11 · Paper released · E3 · Inspectable artifact
This corpus refresh added a directly inspectable public artifact maintained by the authors or releasing organization. E3 records artifact-level inspectability and does not imply independent verification of the underlying scientific or mathematical claim.
Corrections
No corrections recorded.