Anthropic formalizes Fermat's Last Theorem in Lean

Anthropic said on September 4, 2026 that Claude agents produced the first complete computer-checked proof of Fermat's Last Theorem in 11 days, writing about 13 million lines of Lean and proving about 29,500 intermediate theorems. The run used the Prove2Me collaboration platform and an internal research model, and Lean checked the result against the theorem's Mathlib statement using only Lean's three standard axioms. Imperial College mathematician Kevin Buzzard, who has led a multi-year human formalization effort, called the result a step toward autoformalizing the modern mathematical literature.