Anthropic reports first complete computer-checked proof of Fermat's Last Theorem

Anthropic has published what it describes as the first complete computer-checked proof of Fermat's Last Theorem. According to the company, Claude worked largely autonomously over 11 days to write the proof in the Lean programming language, a proof assistant that verifies each logical step mechanically. The theorem, which states that no positive integers a, b and c satisfy the equation a to the n plus b to the n equals c to the n for any n greater than 2, was first claimed by Pierre de Fermat around 1637. Sir Andrew Wiles produced the first accepted proof in 1995. It ran to 129 pages and took months of painstaking human review to verify. A decade later, Dutch computer scientist Jan Bergstra proposed formalizing Wiles's proof so that computers could check it, and in 2024 Kevin Buzzard at Imperial College London launched a multi-year community effort to complete that formalization in Lean. Anthropic says the work began when Tianyi Peng, an Anthropic researcher whose group at Columbia University builds tools for AI formalization, set out to test whether Claude could make progress on the project. The post describes how the formalization was done and discusses what it might mean for research mathematics. If the result holds up to community scrutiny, it marks a significant milestone for AI-assisted formal verification.