Anthropic uses Claude to formalize Fermat's Last Theorem in 11 days

Anthropic has successfully utilized its Claude AI model to produce a fully computer-checked formalization of Fermat's Last Theorem. The project, which mathematicians estimated would take years, was completed in just 11 days of largely unsupervised work. The resulting proof consists of 13 million lines of Lean code, significantly exceeding the size of the existing Mathlib library. Claude’s agents proved over 30,000 theorems to reach this milestone, with minimal human guidance. The breakthrough was supported by the Prove2Me software tool, which helped the AI navigate complex research workflows. While the 11-day timeline highlights the efficiency of modern AI, it also underscores the labor-intensive nature of formalizing complex mathematical proofs. This achievement follows Anthropic's recent work on the Riemann zeta function and reflects a broader trend of AI labs tackling classic mathematical problems to demonstrate the reasoning capabilities of their latest models.