Claude Writes 13-Million-Line Proof of Fermat’s Last Theorem

Fermat’s Last Theorem, posed by Pierre de Fermat in 1637, says no positive integers satisfy aⁿ + bⁿ = cⁿ when n is greater than two. Andrew Wiles, working with Richard Taylor, delivered the first accepted proof in 1995. Anthropic’s result does not solve the theorem anew; it translates the established mathematical argument into Lean, a proof-assistant language that lets computers check every logical step and could reduce the time and uncertainty involved in reviewing highly complex mathematics.

Anthropic said on Sept. 4, 2026, that Claude worked largely autonomously through Prove2Me, a platform developed by Tianyi Peng and collaborators at Columbia University, to complete the formalization in 11 days. The system generated 13 million lines of Lean and proved 30,300 computer-verifiable theorems, 29,500 of which appear in the final proof. Kevin Buzzard, who leads Imperial College London’s long-running formalization project, reviewed the work and said it establishes the theorem using only the axioms of mathematics; Lean independently checked the finished artifact.