Anthropic's Claude formalizes Fermat's Last Theorem proof in 11 days

Anthropic has announced that its AI model, Claude, has successfully formalized the proof of Fermat's Last Theorem in just 11 days. This achievement involves converting Andrew Wiles' 1995 mathematical proof into a computer-verifiable format using the Lean programming language.

The formalization process resulted in approximately 13 million lines of Lean code and the generation of roughly 29,500 intermediate theorems. This is significantly larger than the Mathlib library and represents the largest file of its kind ever created. While mathematicians previously estimated that formalizing Wiles' 129-page proof would take several years, Anthropic's researchers completed the task in less than two weeks using a multi-agent collaboration approach.

The project utilized the Prove2Me platform to manage the complex dependencies of the proof. Rather than discovering a new proof, the AI focused on translating existing human logic into a syntax that eliminates human error and allows for automated verification. Anthropic noted that this technology could eventually reduce the manual labor required to verify new mathematical research.