---
id: "2025-12-06-axiomprover-putnam-2025"
url: "https://postcutoff.com/e/2025-12-06-axiomprover-putnam-2025/"
as_of: "2026-11-13T13:49:00+01:00"
date: "2025-12-06"
date_precision: day
category: science
importance: 3
confidence: medium
status: [Result confirmed]
verification: Lean-verified
sources: 2
editor: human editor
human_review: null
version: "2026-10-04"
---

As of: 2026-11-13 13:49 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2025-12-06-axiomprover-putnam-2025/

# 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

## 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.

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): in its training data
- Claude Opus 5.5 (training cutoff June 2026): in its training data
- Gemini 4 Hydrogen (training cutoff March 2026): in its training data
- Grok 4.7 (training cutoff May 2026): in its training data

## Sources

1. [GitHub: AxiomMath/putnam2025 (Lean proofs)](https://github.com/AxiomMath/putnam2025) (github.com, code)
2. [Axiom Math: From seeing why to checking everything](https://axiommath.ai/research/from-seeing-why-to-checking-everything/) (axiommath.ai, official)

## Changes

- 2026-09-29 (filed): Created

## Related

- 2026-07-23: [AI systems score a perfect 42/42 at IMO 2026, officially graded](https://postcutoff.com/e/2026-07-23-imo-2026-ai-perfect-scores/index.md)
- 2025-07-21: [AI systems reach gold-medal level at the International Mathematical Olympiad](https://postcutoff.com/e/2025-07-21-imo-gold-ai/index.md)