Anthropic said on 4 September that Claude produced the first end-to-end, computer-checked formalization of Fermat’s Last Theorem, writing about 13 million lines of Lean code in 11 days and proving tens of thousands of intermediate results along the way. TechTimes covered the claim on 5 September. The underlying mathematics is still Andrew Wiles’s 1995 argument. What changed is verification: a machine can now check the logic step by step instead of leaving the load entirely to human referees.<\/p>\n
Fermat’s claim, scribbled around 1637, says no positive integers a, b, and c satisfy a\u207f + b\u207f = c\u207f for any integer n greater than 2. Wiles’s published proof ran to 129 pages and still needed a year of repair with Richard Taylor after a gap turned up in review. Formalizing that kind of argument in a proof assistant was expected to take years. Kevin Buzzard’s Imperial College London project had already published an 86-page blueprint and recruited mathematicians worldwide.<\/p>\n
Anthropic researcher Tianyi Peng’s first multi-agent run stalled when agents lost the project state. The breakthrough came with Prove2Me, a collaborative platform that keeps a shared graph of theorem dependencies so many agents can work without overwriting each other. Lean then checked the finished proof against its standard axioms, and a comparator confirmed the statement matches Mathlib’s own Fermat theorem. Buzzard called the result an extraordinary autoformalization step toward checking modern mathematics at scale.<\/p>\n
The work leans hard on community infrastructure: Mathlib, the Lean FRO, and files adapted from the Imperial FLT project. A summer 2026 Lean kernel bug that briefly let a bad Collatz “disproof” pass is a reminder that machine checking is powerful, not magic. Still, if AI can ship a formalized proof beside a human write-up, refereeing the next wave of machine-assisted math gets a little less impossible.<\/p>\n
Sources:<\/p>\n