Anthropic's Claude autonomously completed the first computer-verified formal proof of Fermat's Last Theorem using Lean. Running for 11 days, the AI generated 13 million lines of code and 30,300 theorems through multi-agent collaboration. The system formalized Andrew Wiles' 1995 proof, which was then verified by Lean using only three axioms. This milestone demonstrates AI's capacity for large-scale mathematical formalization, potentially reducing manual verification costs and establishing a new standard for combining human oversight with automated proof generation.