Claude agents built a computer-checked proof of Fermat's Last Theorem in 11 days, Anthropic says

Andrew Wiles’s 1995 proof of Fermat’s Last Theorem is a landmark of modern maths. On 4 September 2026 Anthropic announced the first complete formalisation of it in Lean 4: a version a computer can check step by step, down to the basic axioms. Experts had expected this to take human teams years. Dozens of Claude agents built it in 11 days, finishing on 18 August, using an internal research model and a multi-agent Claude Code setup. Anthropic researcher Tianyi Peng gave occasional high-level direction.

The result is about 13 million lines of Lean, more than five times the size of Mathlib, Lean’s main maths library. According to the repository, it builds using only Lean’s three standard axioms. A separate tool confirmed that the final statement matches Mathlib’s statement of the theorem. nanoda, an independent checker, checked 1,052,234 declarations with no errors.

Kevin Buzzard, whose human-led Imperial College project supplied 106 of the files it builds on, reviewed the work. He called it a big step toward automatically formalising the modern maths literature.

What it means

Turning a long, famous proof into one a computer can check, a job that would have taken people years, took AI agents 11 days. That makes it more realistic to check much of published maths this way, as Buzzard suggests. It does not show that AI could find a proof like Wiles’s on its own.

Caveats

• No new mathematics: it checks a known proof and does not replace a human-readable write-up, Anthropic says.
• The proof is far longer than necessary, theorem names are machine-generated, and no tool can check that intermediate names mean what they suggest (README).
• The 11-day figure is Anthropic’s own account; about 7% of non-boilerplate lines came from earlier, abandoned attempts.
• Buzzard’s human-led Imperial College project is a separate effort that is still going.