Anthropic: Fermat’s Last Theorem formalized in Lean

The decisive moment in this Fermat project is unspectacular: in Lean, a proof either compiles or it does not. Anthropic’s GitHub repository now contains what the company describes as a fully computer-checked version of Fermat’s Last Theorem. Mathematician Kevin Buzzard has since compiled the code himself and run the associated comparator.

Mathematically, the theorem is not new. Andrew Wiles proved in 1995, over 129 pages, that the equation xⁿ + yⁿ = zⁿ has no integer solutions for integer exponents n > 2. What is new is the formalization: the proof is translated into code so that a computer can check every single step, rather than relying on intermediate steps that have been skipped because they are obvious to humans.

Lean serves as both a programming language and a verification system. Mathematical statements and their derivations are checked against a fixed set of logical rules; if even one gap remains, the proof will not compile. Trust must then rest primarily on Lean’s small core and its axioms. The available Mathlib library does, however, limit the scope to the areas of mathematics that have already been formalized.

According to Anthropic, dozens of Claude agents worked for eleven days on a simplified version of Wiles’ proof following Darmon, Diamond and Taylor. The result was 13 million lines of Lean code and around 29,500 intermediate theorems. According to the company, the first teams failed to maintain an overview of the project; the work only made progress with Prove2Me, a platform developed by Tianyi Peng’s group at Columbia University that manages the next proof steps in a directed acyclic graph. According to Anthropic, the effort amounted to around six billion output tokens; that translates into estimated costs of between $100,000 and $300,000.

This is already changing something concrete about the formalization of mathematical literature: third parties can compile the disclosed code and check the logical chain. That creates a technically reproducible form of verification, but it does not replace an independent assessment, which is still largely pending. Buzzard considers the formalization a major step toward the automated formalization of modern mathematics; at the same time, it follows the early literature and offers no new mathematical statement about Fermat’s Last Theorem.