Anthropic said Claude produced the first complete, computer-checked proof of Fermat’s Last Theorem on September 4, 2026. The model worked largely on its own for 11 days in the Lean proof assistant. It wrote 13 million lines of Lean, proved about 30,300 intermediate theorems, and used 29,500 of them in the final argument. Lean checked the finished file against the theorem’s statement in Mathlib, using only Lean’s three standard axioms.

This is not a new proof of the 1637 claim that no positive integers a, b, and c satisfy a^n + b^n = c^n for any n greater than 2. Andrew Wiles published the first accepted human proof in 1995. Anthropic is explicit that the novelty is verification. Claude followed a simplified version of Wiles’s argument from Darmon, Diamond, and Taylor. The company contrasts the work with recent AI attempts on the Riemann hypothesis, which tried to produce new mathematics.

Tianyi Peng, an Anthropic researcher whose Columbia University group builds autoformalization tools, started the run as a test. Early agent swarms lost the project state and stopped cooperating. Those failed passes still contributed about 7 percent of the non-boilerplate lines. The effort worked after the team switched to Prove2Me, an open collaborative platform Peng designed at Columbia. Prove2Me kept a directed graph of theorem statements, split statements from proofs so Lean compiled faster, and stored a natural-language description of each result so agents could search and reuse work.

The successful harness used a Claude Code multi-agent setup and about six billion output tokens from an internal research model Anthropic said is roughly comparable to Claude Fable 5.1. Human math input, the post says, was limited to occasional notes from Peng, such as pushing Mazur’s theorem or treating a Jacobian as a scheme. The community blueprint for the first phase of a human Lean formalization, kicked off in 2024 by Kevin Buzzard at Imperial College London, already ran to 86 pages. Claude’s Lean file is more than five times the size of Mathlib.

“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.” Kevin Buzzard, Imperial College London, in Anthropic’s research post

Decoded Take

The headline writes itself, and that is the trap. Claude did not out-Wiles Wiles. It compiled a known path into a machine-checked artifact at a scale no human formalization group has shipped. That still matters. Referee time is the hidden tax on new math, and a Lean file that matches Mathlib’s FLT statement is a different kind of receipt than a 129-page PDF. The operational tell is Prove2Me: the run failed until agents had a shared graph and a search index. Watch whether the Lean community treats the 13 million lines as a library they can import, whether Buzzard’s group can replay the check on public hardware, and whether the next target is a result that does not already have a famous proof sitting on the shelf.