A landmark proof becomes software machines can check
- What it is
- A reported Lean formalization turns the known proof of Fermat’s Last Theorem into steps a computer can check.
- Who did it
- Anthropic’s Claude agents, with research led by Tianyi Peng
- What it could mean
- Fermat is already proved. Imagine giving that proof a ‘verify’ button. If this scales, AI-assisted mathematics could arrive with independently checkable logic—catching errors before other research builds on them.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
Formalizing Fermat's Last Theorem ↗See the proposed checks
In an isolated high-memory environment, clone the exact source commit; verify source hashes and provenance; run the default lake build; run verification/comparator/run.sh against the Mathlib-only challenge; run verification/nanoda/run.sh; inspect the four nanoda performance patches; and have a formal-methods reviewer map PROOF-PATH.md and the encoded theorem to the intended Frey–Serre–Ribet–Wiles/Taylor-Wiles argument.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
How a long proof becomes checkable
Fermat’s Last Theorem
aⁿ + bⁿ ≠ cⁿ for positive integers a, b, c and integer n > 2
Each tile stands for a mathematical statement; the connections show which earlier statements it depends on. The announcement describes a dependency graph used to organize a Lean formalization of Fermat’s Last Theorem. This illustration explains that structure; it is not the project’s actual proof graph.
Read the source · Formalizing Fermat’s Last Theorem · Prove2Me dependency graph ↗- What it claims
- Anthropic reports that Claude agents produced in eleven days the first complete end-to-end, computer-checked Lean proof of Fermat's Last Theorem. This is not a new solution to an open problem—Wiles and Taylor-Wiles proved the theorem in 1995—but a claim that their known mathematical route has been rebuilt as a fully machine-checkable formal artifact at unprecedented scale and speed.
- Why this could matter
- A landmark proof becomes software machines can check Fermat's Last Theorem was solved in 1995. The new achievement is different: turning that enormous human proof into code independent computers can replay. If this scales, AI-generated mathematics can arrive with a checkable receipt—helping researchers find errors and spend time understanding the truth.
- If it holds up
- A reproducible end-to-end Lean proof would show that AI can help turn landmark mathematics into independently checkable software, making formal verification a practical companion to human peer review as mathematical output accelerates.
- If it does not
- Fermat's theorem remains proved, but this artifact would not yet demonstrate a reliable new route for machine-checking large AI-assisted proofs; the verification workflow would need repair.
- Impact horizon
- Methods · Formal verification · AI mathematics · Research infrastructure
- Version
- Anthropic research announcement, published 2026-09-04; public proof repository pinned at unsigned commit aa2d8b34692b16c70f699536de0d8e75b9a3e9ef, authored 2026-09-03
- Why we tracked it
- Anthropic's complete Lean 4 formalization claim is pinned to a public source commit with three concrete replay routes; it remains source-locked and independently unvalidated by State of Proof, and no docket has been created.
- Highest-risk dependency
- The evidence is author-supplied and the repository's formalization.yaml labels review status self-assessed with no listed reviewers. Full replay is resource-heavy—the published route reports hundreds of gigabytes of working storage and up to roughly 300 GB of memory—and machine checking establishes formal inference, not by itself the semantic faithfulness of every named intermediate result or generated explanation.
- Available artifacts
- The pinned Apache-2.0 repository contains roughly 13 million lines of Lean, 29,511 theorem/proof modules, FinalCheck.lean, a human-readable PROOF-PATH.md, metadata declaring zero sorry terms and exactly Lean's three standard axioms, a Lean Comparator challenge, and an independent nanoda-kernel replay route. Lean 4.33.1 and Mathlib commit db584cd6d46c92f209a44c0f1c829460d327499d are pinned. The artifact builds on and attributes work from the Imperial College London FLT project, flt-regular, and Mathlib.
- Current boundary
- Intake record only; examination not started.