Anthropic recently announced that its AI model successfully completed the first end-to-end, computer-checked Lean formal proof of Fermat's Last Theorem (FLT) after running autonomously for 11 days. This work did not involve the AI rediscovering a mathematical proof of the theorem, but rather converting existing mathematical proofs into forms that can be step-by-step verified by the Lean proof assistant. Lean is a proof assistant used to write and verify formal mathematical proofs, capable of checking the logical steps in a proof through a computer.

In this process, Claude generated approximately 13 million lines of Lean code and proved about 30,300 theorems, with about 29,500 intermediate theorems eventually incorporated into the complete proof of Fermat's Last Theorem. The entire proof was checked by Lean, using only three standard axioms from Lean. The goal of this work was to formalize the proof of Fermat's Last Theorem completed by British mathematician Andrew Wiles in 1995. Fermat's Last Theorem states that when the integer exponent $n$ is greater than 2, there are no positive integers $a$, $b$, and $c$ that satisfy $a^n + b^n = c^n$. Wiles' original proof was 129 pages long and underwent several months of manual verification before publication.

The difficulty of mathematical formalization lies in the fact that human mathematical proofs often omit many derivation steps considered obvious, while Lean requires explicit verification of every logical step. Additionally, mathematicians have long cited a large number of mathematical results that have not yet been formalized, so converting a complete proof into a computer-verifiable form usually requires significant time. Anthropic had previously estimated that formalizing Fermat's Last Theorem might take several years.

image.png

This project was initiated by Anthropic researcher Tianyi Peng. Claude did not complete all the work by a single agent, but rather through multi-agent collaboration to handle concept definitions, prove intermediate theorems, and derive more complex propositions. The project used the Prove2Me platform developed by Peng and his colleagues at Columbia University, which records theorems to be proven and their dependencies using a directed acyclic graph and supports multiple Claude agents working in parallel. The final proof followed a simplified version of Wiles' proof by Darmon, Diamond, and Taylor. Human researchers mainly provided a small number of high-level instructions, such as determining the priority of certain mathematical objects or theorems, while the specific proof process was primarily completed by Claude.

The entire project consumed approximately 6 billion output tokens, using a general internal research model roughly equivalent to Claude Fable5.1. The final generated proof is more than five times the size of Mathlib, the main mathematical proof library. Anthropic specifically emphasized that the focus of this achievement is not that AI independently proposed a new proof of Fermat's Last Theorem, as the theorem was already proven by Wiles in 1995. The innovation of this work lies in using AI to automatically formalize proofs on a large scale, and then having Lean perform computer verification of the final result.

Anthropic believes that if similar automated formalization technology can be extended to more modern mathematical achievements, it could significantly reduce the manual cost of verifying new proofs in mathematical research. As the amount of mathematical results generated by AI increases, it may become a common practice to provide both human-readable and formalized versions of mathematical proofs. The complete Lean proof from this project has been made publicly available on GitHub. At the same time, mathematician Kevin Buzzard reviewed the proof and believes that this automated formalization result shows important progress in AI-assisted formalization of large mathematical achievements.