Anthropic's Claude Formally Proved Fermat's Last Theorem in 11 Days

Fermat's Last Theorem waited more than three centuries for a proof, and another three decades for anyone to seriously attempt machine verification. Anthropic has now shipped the first complete one, generated largely autonomously by Claude in 11 days. The resulting artifact is 13 million lines of Lean 4, over five times the size of Mathlib, the community library it builds on.

Unlike recent AI-driven work on the Riemann hypothesis, which produced novel mathematics, what's novel here is the verification. This is a claim about what AI agents can now do to the reliability layer of mathematics as a discipline.

What formalization actually means

A formalized proof rewrites informal human mathematics into a language a computer can mechanically check, step by step. Lean needs to see every step, no matter how trivial, whereas a proof written for human readers will skip many obvious ones. Human proofs also build on centuries of published work, while formalization starts from the tiny fraction of math that's been formalized already.

That gap is why formalizing Fermat's Last Theorem was considered a years-long undertaking. Just the blueprint the mathematical community has been using to describe the initial phase of the project runs to 86 pages. Kevin Buzzard at Imperial College London kicked off a multi-year community effort in 2024 to do it by hand.

How Claude pulled it off in 11 days

Claude produced computer-verifiable proofs of 30,300 theorems along the way, using 29,500 in the final proof. The approach was a swarm of agents rather than one long context: dozens of Claude agents collaborated to define concepts, prove intermediate theorems, and use those results to tackle progressively harder statements.

Early attempts failed in a recognizable LLM pattern. Agents had some initial success but quickly lost track of the project's state and stopped collaborating effectively. The fix was infrastructure rather than a smarter model. The team switched to Prove2Me, a platform built by Anthropic researcher Tianyi Peng and collaborators at Columbia, which coordinated agents through three mechanisms:

• A directed acyclic graph (DAG) of theorem statements that agents used to decide what to attempt next, mitigating memory degradation and enabling parallel work.
• Separated theorem statements and proofs into different files to speed up Lean compilation and minimize resource consumption.
• A natural-language description of each theorem statement, letting agents find lemmas semantically rather than by exact name.

Human mathematical input was minimal: occasional high-level instructions from Tianyi, such as "Jacobian as a scheme sounds high priority" and "push [the] Mazur [theorem] to be done soon." With Prove2Me and a Claude Code-based multi-agent harness, the team completed the proof in just under two weeks, consuming about six billion output tokens from a general-purpose internal research model roughly comparable to Claude Fable 5.1.

Why the output can be trusted

Lean's kernel refuses to accept anything that does not reduce to its own axioms, so auditing 13 million lines means running the checker, not reading the source. The finished proof uses just Lean's three standard axioms, and a comparator confirmed the theorem statement matches Mathlib's own statement of FLT.

The GitHub repo goes further, running the proof through nanoda, a second independent Lean kernel written in Rust, which accepted an export of the entire environment. The build contains no sorry, no added axioms, no native_decide escape hatches, and the top-level theorem is exactly what you would write informally:

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n)
    (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
    a ^ n + b ^ n ≠ c ^ n

Reproducing it is expensive but possible. A from-scratch build takes roughly five and a half hours across 96 cores with a 153 GB memory peak; the comparator kernel replay adds about 15 hours on a single core. The proof follows a simplified version of Wiles's argument by Darmon, Diamond and Taylor, going through Frey curves, Ribet's theorem, and the Taylor-Wiles patching argument.

Strengths and limits of the artifact

Claude can hold a research-scale plan across dozens of agents when given an external scaffold, grind through the tedious algebraic geometry and number theory that human formalizers dread, and produce Lean that a second kernel accepts. The proof also covers wide swaths of previously unformalized math, including pieces of algebra, harmonic analysis, geometry, and number theory.

The output is verbose and machine-flavored. Sources were written to be checked rather than read: names are machine-generated, and labels such as P2M or hexadecimal suffixes are pipeline artifacts rather than mathematical identifiers. About 7% of the non-boilerplate lines came from failed attempts that were never cleaned up, and Anthropic acknowledges the proof is likely far longer than necessary. There is also a trust gap the kernel cannot close: no tool can verify that each of the 29,500 intermediate lemma names actually corresponds to the mathematical statement it claims to be. That remains a job for human readers, aided by the accompanying PROOF-PATH.md.

What changes for math and AI

Reviewing the artifact, Kevin Buzzard argued this pushes autoformalization from a research curiosity into something practically deployable. The near-term implications are concrete:

1. Formalization can now plausibly run alongside informal write-ups, giving reviewers a machine-checked skeleton to trust while they focus on ideas.
2. AI-generated mathematics, which is arriving faster than referees can evaluate it, gets a scalable check. Buzzard specifically calls out rigorously checking LLM-generated math, which he describes as currently an extremely costly human-led process.
3. The existing mathematical corpus becomes easier to audit for errors that have quietly propagated, a category that includes Wiles's original gap, the Kepler conjecture review, and results accepted for years before being found wrong.

Anthropic researchers also ran a smaller experiment using three personal Claude Max plans to formalize applications of the Hardy-Littlewood Circle Method. Collaborating entirely through Prove2Me, the agents completed a formalization of Vinogradov's Three Primes Theorem in three days, suggesting that the infrastructure, not just the frontier model, is what unlocked the larger result.