Claude's 11-day proof of Fermat's Last Theorem passes computer verification
Formalizing Fermat's Last Theorem
Anthropic's Claude has achieved the first complete computer-checked proof of Fermat's Last Theorem, working largely autonomously over 11 days to write the proof in the Lean programming language. The effort produced 13 million lines of Lean code and proved 29,500 intermediate theorems. The proof follows a simplified version of Wiles's proof and was verified using the Lean proof assistant, with human input limited to occasional high-level instructions. This milestone demonstrates the potential for AI to formalize complex mathematics, reducing the burden of verifying new results.
If the automatic formalization of FLT is possible now, then we have taken a big step towards automatic formalization of the modern mathematical literature.