Anthropic published the first complete computer-checked proof of Fermat's Last Theorem. Claude worked largely on its own for 11 days to write it in Lean, a proof-checking language. Dozens of Claude agents split the work and proved intermediate results in parallel. Human input was limited to occasional high-level priorities from researcher Tianyi Peng. Early attempts failed because agents lost track of the project state. The effort succeeded after switching to Prove2Me, an open platform from Columbia University. Kevin Buzzard of Imperial College London reviewed the proof and called it an extraordinary achievement. Lean confirmed the proof uses only its three standard axioms. Anthropic also formalized a smaller theorem in three days using consumer Claude Max plans. The full proof is on GitHub.

• 11 days to complete
• 13 million lines of Lean
• 29,500 intermediate theorems
• ~6 billion output tokens