Claude formalized Fermat's Last Theorem in 11 days. The proof was old — the verification is new

On September 4, Anthropic announced that Claude had produced the first complete computer-checked proof of Fermat's Last Theorem, writing it in the Lean proof assistant over 11 days of largely autonomous work. The news leaked about an hour earlier: by Buzzard's account, a coffee shop in Islington broke it on Instagram, and the Imperial College mathematician leading the community's own formalization effort initially dismissed the email that reached him at a Welsh festival as a crank's. The result is real — Buzzard compiled the roughly 13-million-line codebase and ran its verification tooling himself. What it means is a quieter question.

A 358-year gap between a margin note and a machine

Fermat's Last Theorem began around 1637 as a claim scrawled in the margin of a copy of Diophantus's Arithmetica: no three positive integers satisfy aⁿ + bⁿ = cⁿ for n > 2, accompanied by Fermat's note that he had "a truly marvelous proof" the margin was too narrow to contain. Mathematicians now believe that proof never existed. The theorem survived three and a half centuries — a 1908 prize of 100,000 German gold marks drew 621 incorrect submissions in its first year alone — until Andrew Wiles announced a proof in June 1993, a gap surfaced during review, and Wiles and Richard Taylor closed it a year later. The final proof ran to 129 pages and was published in May 1995.

"Formalizing" FLT is a different task: translating that human proof, line by line, into a language a computer can check. Wiedijk's famous list of 100 formalization challenges has stood for two decades with FLT as its final item, and the community push Buzzard kicked off in 2024 was expected to run for years — its blueprint alone spans 86 pages. That is the backdrop against which Anthropic's claim of an 11-day, largely autonomous completion should be read: the theorem has been proved since 1995, so what happened last week is verification of a settled result, not the discovery of a new one.

What 11 days of largely autonomous work produced

The campaign began as a research test. Tianyi Peng, an Anthropic researcher whose Columbia group builds AI formalization tools, set out to see whether Claude could make progress on FLT. Early runs failed: agents lost track of the project's state and stopped collaborating, and Anthropic says those failed attempts still contributed roughly 7% of the non-boilerplate lines in the final proof. The breakthrough came with a switch to Prove2Me, an open platform Peng and collaborators designed that keeps a directed acyclic graph of theorem statements, separates statements from proofs in different files, and indexes each statement with a natural-language description so agents can find and reuse work.

Dozens of Claude agents then worked through the graph on a Claude Code-based multi-agent harness. Human input was occasional and high-level — "Jacobian as a scheme sounds high priority," "push [the] Mazur [theorem] to be done soon." Claude's own notes capture the finish:

"THE FLT root reads Proved on the site. Historic moment (modulo re-check)." "!!! The FLT ROOT 62eb32c0 reads PROVED." — From Claude's campaign notes, shared by Anthropic

The scale, per Anthropic's post:

• About 13 million lines of Lean, more than 5x the size of Mathlib (Buzzard measured 13.4 million when he compiled the repository)
• 30,300 theorems proved along the way; 29,500 used in the final proof
• Roughly six billion output tokens from an internal research model "roughly comparable" to Claude Fable 5.1, an unreleased model rather than a shipping product
• The proof rests on Lean's three standard axioms, and a comparator confirmed the theorem's statement matches Mathlib's own statement of FLT
• The route is the Darmon-Diamond-Taylor exposition of the Wiles-Taylor-Wiles argument, covering exponents p ≥ 17; the gap is covered by the community's earlier formalization for regular primes, since the smallest irregular prime is 37

The repository, committed September 3 by a user named "claude," credits the Imperial College London FLT project, flt-regular and Mathlib for 106 files, and is candid about the artifact's purpose: "written to be checked rather than read," with machine-generated names and comments stripped.

The independent check that matters

Vendor claims about proofs deserve the same skepticism as vendor claims about benchmarks, which is why the response on Buzzard's blog matters more than the announcement. Buzzard compiled the codebase on 96 cores — Anthropic also lent him a machine with 500 GB of RAM — ran the comparator and reports that "it checks out." The proof takes nearly 20 times as long to compile as Mathlib. His verdict, as quoted by Anthropic:

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

This is the story's closest thing to an independent signal: not an Anthropic employee, but the leader of the rival formalization effort, confirming statement, axioms and build. The repository adds a second check: nanoda, an independently implemented Lean kernel, accepts the same environment.

"Essentially nothing," and why that is the point

Buzzard is equally blunt about the mathematical content. The work, he writes, "tells us essentially nothing: I am on record as saying that I am 99.9% sure that the proof of FLT is OK." Anthropic makes the same distinction itself, noting that unlike its recent Riemann-hypothesis work — which produced novel mathematics — "what's novel here is the verification." Formalizing a theorem proved in 1995 is a test of translation, not of discovery.

Several caveats keep the milestone honest. The model behind it is internal and unreleased; "roughly comparable to Claude Fable 5.1" is a hedged vendor description of the flagship we covered at launch, and no outside party can reproduce the 11-day run at any price. The artifact is not human-readable mathematics, and Buzzard expects Anthropic's job to end with the formalization — his own project's promise of a dynamic document for humans remains community work. The economics are unproven either way — a comment-thread debate on his blog put the cost of six billion output tokens at roughly $300,000 at API prices, with a counter that ~70% gross margins imply a real cost near $100,000. Buzzard noted the arithmetic of his own situation: "Anthropic took only 11 days but I do wonder if they spent more money" than the £1M funding his five-year project. On Reddit's r/singularity, the thread "Anthropic has formalised FLT!!" drew roughly 550 points and 190 comments.

A week when the machines did the math

The formalization lands in the middle of an unusually crowded stretch for machine-checked mathematics. Epoch AI's new FrontierMath Erdős benchmark saw its first AI solutions this week, the same batch of results we cover alongside Astra's run, and OpenAI's GPT-5.6 drew attention for improving a prime-gap bound — a result that survived scrutiny mainly because an expert wrote out a heuristic exposition of it. What separates last week's announcement from those is the referee: a 30,300-theorem argument checked by a kernel that accepts no hand-waving, resting on three axioms. The recurring question — how to trust AI mathematics no human can read — has, for the first time at this scale, a mechanical answer.

What would settle the bigger claims

Part of the skepticism budget is already spent: the independent check happened and it passed — Buzzard compiled the build, ran the comparator, confirmed the statement matches Mathlib's, and a second kernel agrees. What remains unsettled is the general claim hiding inside this specific success — that autoformalization at this scale is ready to referee AI-generated mathematics. Testing that requires the release of the model that did the work, so the economics of an 11-day, six-billion-token campaign can be measured rather than debated; it requires formalizations that integrate upstream into Mathlib rather than standing alone as 13 million lines no one reads; and above all it requires a genuinely novel theorem — not a 1995 proof — machine-checked end to end, where the computer is not confirming what mathematicians already believe but arbitrating what they cannot yet read. Until then, the correct headline is the one the mathematical community has been writing for decades: the proof of Fermat's Last Theorem was right, and now a machine agrees.