Claude formalizes Fermat’s Last Theorem in Lean — first complete computer-checked proof

On 4 Sep 2026 Anthropic published Formalizing Fermat’s Last Theorem: Claude agents, steered lightly by researcher Tianyi Peng and running on Prove2Me, wrote the first complete computer-checked FLT proof in Lean in about 11 days. The artifact spans roughly 13 million lines and ~29,500 intermediate theorems (~30,300 proved along the way), uses only Lean’s three standard axioms, and a comparator confirmed the statement matches Mathlib’s FLT. The campaign follows a Darmon–Diamond–Taylor exposition of Wiles’s proof; early multi-agent attempts failed until Prove2Me’s DAG of theorem statements kept agents aligned. Kevin Buzzard reviewed the result and framed it as a step toward autoformalizing the modern mathematical literature. Anthropic contrasts this verification milestone with recent AI work that claims novel math (e.g. Riemann-related results).