Anthropic says Claude has produced the first complete, computer-checked formal proof of Fermat’s Last Theorem.

Working largely autonomously for 11 days, Claude translated a proof based on Andrew Wiles’s work into 13 million lines of Lean and used 29,500 intermediate theorems in the final result. Rather than discovering a new mathematical proof, the project converted the existing reasoning into a form whose every step can be verified by a computer.