Anthropic Publishes Formal Lean Proof of Fermat’s Last Theorem

Anthropic’s Lean proof of Fermat’s Last Theorem is a newly public formal representation of an already known mathematical result, not a new solution to the problem. Anthropic announced a complete machine-verified proof in the Lean 4 system on September 4, 2026. The first human proof of the theorem was published by Andrew Wiles and Richard Taylor in 1995.

Fermat’s Last Theorem states that the equation xⁿ + yⁿ = zⁿ has no nonzero solutions for natural numbers x, y, z and an integer n greater than 2. Its significance in this case lies not in a new insight in number theory, but in the scale and method of machine formalization of a modern proof.

Anthropic’s Lean proof was created using a multi-agent process

According to Anthropic, the Claude system worked on the project predominantly autonomously for 11 days. It created approximately 13 million lines of Lean code and used a multi-agent process on the Prove2Me platform. The company also states that the system occasionally received human instructions and worked with existing human formalization projects.

This is an important limitation when interpreting the result. The degree of autonomy cannot be precisely measured independently from the published materials alone. The result therefore cannot be equated with the independent discovery of a mathematical proof by artificial intelligence. It is a transcription and linking of a known argument into a language that a proof assistant can verify.

Anthropic made the source code available in a GitHub repository. The project documentation states that it was successfully checked by the Lean kernel, the comparator tool, and a second independent kernel called nanoda. These procedures are intended to verify that the formal object conforms to the rules of the logic and type system used by Lean.

Mathematician Kevin Buzzard also confirmed the check

Mathematician Kevin Buzzard, who leads the Xena project focused on teaching and popularizing the formalization of mathematics, said that he compiled the repository and verified the proof using the comparator tool. According to his statement, the formal proof passed the check.

Such verification is important mainly because the public repository allows other researchers to reproduce the result. The formal check confirms the logical validity of the claim within Lean, subject to trust in the checking tools used. By itself, however, it does not mean that every name, intermediate step, or human explanation in the code automatically captures the intended mathematical interpretation.

Anthropic describes its result as the largest Lean proof. The label “longest mathematical proof of all time,” however, cannot be reliably confirmed because there is no publicly documented universal ranking of mathematical proofs by length. It is safer to describe it as a very extensive formal proof and, according to Anthropic, the largest project of its kind in Lean.

The difference between discovery and formalization

Formal proofs convert mathematical arguments into a precise form that software can check. For extensive modern proofs, this transcription requires considerable time and specialized work: definitions, assumptions, auxiliary claims, and every logical step must be captured explicitly, even though they are often summarized in ordinary academic writing.

That is why the published Anthropic Lean proof is a milestone in autoformalization. The public artifact shows that a multi-agent AI system was able, in a short time, to create and have machine-verified an extensive formalization of a known proof. It does not, by itself, say anything about whether the system found a new result in number theory.

Further assessment will focus on independent reproductions of the complete build and checking scripts. Experts will also be able to examine the scope of the existing components used, the quality of the connection to Wiles’s original proof, and the project’s practical reproducibility with lower hardware requirements.

Verified and updated: 09/05/2026 15:25