AxiomProver produces machine-checked Lean proofs for all 12 Putnam 2025 problems
Axiom Math's autonomous Lean 4 prover solved 8 of 12 problems of the 6 Dec 2025 Putnam competition within exam time and the remaining 4 in the following days, all as machine-checked Lean proofs published on GitHub.
Key facts
- Putnam 2025 held 6 Dec 2025; 8/12 solved within the exam window, 12/12 after extra time
- Proofs are formal Lean 4 and publicly released
- Axiom says no human scored 12/12, but the 12/12 includes solutions found after the deadline
- Not an official entry; self-reported timing
Science result
- Field
- mathematics / competition mathematics / formal proof
- Problem
- William Lowell Putnam Competition 2025 (12 problems)
- Result
- Formally verified Lean 4 solutions to all 12 problems, 8 of them within the exam time.
- AI system
- AxiomProver
- Human role
- Autonomous proof search; humans formalised problem statements (per company)
- Verification
- Formal proof in Lean (public repository)
- Status
- confirmed
- Why surprising
- The hardest undergraduate competition, fully solved with machine-checkable proofs rather than natural-language answers.
What happened
Axiom Math ran its prover on the 2025 Putnam problems, producing formal Lean 4 proofs that any Lean installation can check.
Why it matters
Formal verification removes grading disputes like those around informal IMO proofs, and showed formal provers catching up with informal LLMs on hard competition maths.
Changelog
- 2026-09-29: created
Related events
- AI systems reach gold-medal level at the International Mathematical Olympiad ★★★★★
- AI systems score a perfect 42/42 at IMO 2026, officially graded ★★★★★
- Math Inc's Gauss agent completes the Strong Prime Number Theorem formalisation in Lean in three weeks ★★★★
- DeepSeekMath-V2: open-weights self-verifying prover reaches IMO 2025 gold level and 118/120 on Putnam 2024 ★★★★
Sources (2)
- codeGitHub: AxiomMath/putnam2025 (Lean proofs)
- officialAxiom Math: From seeing why to checking everything
id: 2025-12-06-axiomprover-putnam-2025 · updated 2026-09-29 · open in the interactive timeline