Formalizing Fermat's Last Theorem (Anthropic, 2026-09-04)

Anthropic's account of Claude producing the first end-to-end machine-checked proof of Fermat's Last Theorem in Lean, "largely autonomously," over 11 days in August 2026. The proof is public: github.com/anthropics/fermats-last-theorem, Apache-2.0, created 2026-09-04, 725 stars and a ~227 MB checkout when this page was written.

The claim is about verification, not discovery — Anthropic says so in its own words, contrasting the work with AI-driven results on the Riemann hypothesis "which produced novel mathematics": "what's novel here is the verification." The mathematics is Wiles's 1995 proof, by way of the simplified Darmon–Diamond–Taylor exposition. See autoformalization for why that distinction carries most of the weight here.

Tier: T3 — a first-party announcement about the performance of the company's own model, and every number in it is Anthropic's. The unusual part, and the reason the grade matters less than it normally would, is the same one lean-certificate identified in ten-proofs: the artifact type-checks or it doesn't, on a stranger's machine. Here there is also an external reviewer — kevin-buzzard, who leads the community FLT formalization this work adapts pieces from, read the proof and is quoted at length.

The numbers


Wall-clock	11 days; the FLT root read PROVED at 02:00:57Z on 2026-08-18
Lean produced	13 million lines — over 5× the size of Mathlib
Theorems	30,300 proved, 29,500 used in the final proof
Tokens	~6 billion output tokens
Model	"a general-purpose internal research model roughly comparable to Claude Fable 5.1"
Human mathematical input	occasional high-level steers from Tianyi Peng: "Jacobian as a scheme sounds high priority," "push [the] Mazur [theorem] to be done soon"
Axioms	Lean's three standard ones, with a comparator confirming the statement matches Mathlib's own FLT statement

Two contextual figures from the same post: the community blueprint for the initial phase alone runs to 86 pages, and Buzzard's Imperial College project, started in 2024, was expected to take years.

Clarified 2026-09-06, from the community project's own repository (flt-imperial-project). The two formalizations follow different proofs, and this page previously left that ambiguous. Anthropic formalized Wiles's 1995 argument via the Darmon–Diamond–Taylor exposition; the Imperial project is explicitly not formalizing Wiles/Taylor–Wiles but a newer route through Khare–Wintenberger and Kisin, designed by Richard Taylor after discussions with Buzzard. Both turn on the same core (a deformation ring is isomorphic to a Hecke algebra), by different roads. Anthropic adapting pieces of the community work is consistent with that; "finishing their project" is not what happened. Two further corrections from the primary: the Imperial repository was created 2023-11-19 (the grant year 2024 is when Buzzard's funded time began), and the project's stated 2029 goal is a reduction of FLT to claims known by the late 1980s — not a complete proof from the axioms.

The failure that came first

Anthropic reports the naive multi-agent approach failing outright: agents "quickly lost track of the project's state and stopped collaborating effectively," and those attempts contributed about 7% of the non-boilerplate lines in the final proof. What made it work was prove2me — a DAG of theorem statements agents consult to choose their next target, statements split from proofs into separate files, and a natural-language description attached to each statement so agents can find and reuse what already exists.

The win came from external structure holding the project state, not from longer-running or better-prompted agents.

What Buzzard said

"This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics. … we learn that AI autoformalization artefacts are now robust enough to be built upon."

And on where it leads: "Such autoformalization techniques will lead to new tools, rooting out errors in the current mathematical corpus and lightening the load of referees. The techniques will also enable us to rigorously check LLM-generated mathematics, which is currently typically an extremely costly human-led process."

Note the hedge Buzzard keeps in his own sentence — "which Anthropic researchers say only took 11 days." The proof is checkable; the 11 days are not.

Claims that go past the artifact

Formalizing helps the model prove new things. Anthropic says recent Claude-authored results were formalized in parallel with their proofs, and that Claude "appears to use these partial proofs to independently check its hypotheses much like it writes numerical simulations." No measurement offered.
The cost floor may be low. Three personal Claude Max plans, collaborating through prove2me, formalized Vinogradov's three-primes theorem in three days. If that generalizes, the 6-billion-token figure is a ceiling for a hard case rather than the price of entry.
The proof is "likely much longer than it needs to be" — Anthropic's own caveat, and the reason 13 million lines is not a measure of the mathematics.

Cross-spoke context

The multi-agent orchestration half — memory degradation, a shared DAG as external state, a Claude Code-based harness running dozens of agents — sits next to ../agentic-tooling-wiki's harness thread. Routed here because the subject is formal methods (cluster E); the harness detail is recorded on prove2me rather than split out.

autoformalization · prove2me · lean-theorem-prover · lean-certificate · ten-proofs · kevin-buzzard · tianyi-peng · anthropic · formal-verification · abduction