Anthropic said Sept. 4, 2026, that Claude agents produced what the company calls the first complete, end-to-end computer-checked proof of Fermat’s Last Theorem — formalized in Lean and published as a public repository built on Mathlib.
The claim is about verification, not new mathematics. Fermat’s statement (no positive integers a, b, c satisfy aⁿ + bⁿ = cⁿ for n greater than 2) was proved by Andrew Wiles in the 1990s with Richard Taylor after a gap in the first announcement. Anthropic said Claude’s formalization follows a simplified Wiles route as presented by Darmon, Diamond and Taylor, run as a proof by contradiction along the Frey–Serre–Ribet–Wiles line.
According to Anthropic, the run took about 11 days with dozens of Claude agents, wrote roughly 13 million lines of Lean, and produced computer-verifiable proofs of about 30,300 theorems, using about 29,500 in the finished proof. The company said Lean checked the finished proof using only Lean’s three standard axioms, that a comparator matched Mathlib’s FLT statement, and that builds fail if the proof relies on sorry, added axioms, or native_decide.
Anthropic said the agents used Prove2Me and a Claude Code–based harness, consuming about six billion output tokens from an internal research model roughly comparable to Claude Fable 5.1.
Human mathematical authorship was minimal by Anthropic’s account: occasional high-level priority notes from researcher Tianyi Peng, whose Columbia group builds AI formalization tools — no Lean and no mathematics beyond the one-line goal theorem, the company said.
The artifact adapts material from Kevin Buzzard’s Imperial College London Lean FLT project (started 2024) and related community libraries; Anthropic said 106 files contain credited material from those efforts and that it shared the proof with Buzzard. In a statement Anthropic published, Buzzard called the work an “extraordinary autoformalization achievement” that “proves Fermat’s Last Theorem with no assumptions other than the axioms of mathematics” and said such artefacts “are now robust enough to be built upon.” New Scientist largely restated Anthropic’s account when reporting those comments.
Caveats matter for trust and refereeing. Anthropic and its README note the proof is not meant for upstreaming as readable mathematics, that named classical results are proved only in restricted strength, and that no tool can check that each intermediate theorem means what its name suggests. The story is AI-for-science infrastructure and referee burden: a years-scale Lean formalization compressed into a multi-agent run with a public kernel-checked certificate — not a claim that FLT was unsolved until 2026, and distinct from Anthropic’s product launches.
What remains unclear is how much of the artefact the broader Lean and number-theory communities will treat as a foundation versus a one-off, hard-to-read autoformalization dump — even if the kernel checks pass.