How Lean Formalized Fermat’s Last Theorem

Picture a mathematician in 1637 writing a tantalizing sentence in the margin of a book: no positive integers can solve aⁿ + bⁿ = cⁿ when the exponent n is greater than 2. The statement is short enough to fit beside a paragraph. The proof took more than three centuries.

On September 4, 2026, a new milestone shifted attention from discovering the proof to checking it. An Anthropic project reported a complete, end-to-end formalization of Fermat’s Last Theorem in Lean, a programming language and proof assistant. The mathematics still comes from the tradition surrounding Andrew Wiles’s proof; the new achievement is translating that mathematics into code a computer can verify. (anthropic.com)

A tiny statement with a huge proof

A positive integer is a whole number greater than zero. The exponent tells us how many times a number is multiplied by itself. Fermat’s Last Theorem says that for positive integers a, b, and c, there is no solution to

aⁿ + bⁿ = cⁿ

whenever n ≥ 3. The boundary matters. When n = 2, the familiar equation 3² + 4² = 5² provides a solution. The theorem begins exactly where those Pythagorean triples stop being possible.

The surprising part is how far the proof moves from elementary arithmetic. A high-level outline starts with a hypothetical solution and constructs a special elliptic curve, an equation whose points have a rich algebraic structure. Work by Gerhard Frey and Ken Ribet connects that curve to modularity, meaning a deep relationship with a highly structured analytic object called a modular form. Wiles’s modularity results then force the same curve to have two incompatible properties. The contradiction eliminates the original solution. (github.com)

The published human proof from the 1990s was already difficult to read and verify. Formalizing it requires every definition, hidden assumption, and intermediate result to be made explicit, including the machinery of elliptic curves, modular forms, Galois representations, and deformation theory.

What “formalized” adds

A normal mathematical proof is written for a human reader. It may say “the remaining cases follow by a standard argument” or use a familiar theorem without restating all of its conditions. A formal proof is different. It is a precisely typed object that must be accepted by a small piece of software called a kernel.

Lean’s kernel is a trusted type checker. In programming, a type describes what kind of value something is allowed to be. Lean extends that idea to logic: a proposition is a statement, and a proof is a term that inhabits the proposition’s type. A proof-writing helper called a tactic may search for the right steps, but the final proof term still has to pass through the kernel. (lean-lang.org)

Here is a compact description of the theorem’s shape:

#check
 ∀ (n: ℕ), 3 ≤ n →
 ∀ (a b c: ℕ),
 0 < a → 0 < b → 0 < c →
 a ^ n + b ^ n ≠ c ^ n

This code does not prove Fermat’s Last Theorem. The #check command asks Lean to verify that the statement itself is well-formed. ℕ means the natural numbers, arrows represent assumptions leading to a conclusion, and ≠ means that an equality would produce a contradiction. The completed project supplies the enormous proof that inhabits this proposition. (github.com)

How can a computer check a proof it does not understand in the human sense? It does not need to appreciate why a theorem is beautiful. It checks whether each symbol has the right type, whether each referenced theorem really exists, and whether every deduction follows the rules of Lean’s logic.

Why the translation is difficult

Human mathematics leans on a large shared background. A reader may know what an elliptic curve means, recognize a standard construction, and fill in three omitted algebraic steps without noticing. Lean cannot rely on that kind of intuition. The objects must be defined, their properties proved, and their relationships connected through declarations that another theorem can reuse.

Mathlib, Lean’s community-maintained library of formal mathematics, provides much of that foundation. The Fermat project still had to build or adapt many pieces of modern number theory. The result resembles a very large software build: hundreds of modules expose definitions and theorems, and later modules depend on earlier ones. A missing hypothesis is not a minor editorial flaw; it can change the statement being proved.

The AI breakthrough was coordination

The reported formalization took Claude about 11 days and produced roughly 13 million lines of Lean. Along the way, the system proved around 30,300 intermediate theorems, with about 29,500 used in the final chain. The difficult engineering problem was not asking one model to remember an entire proof. It was keeping many separate proof-writing efforts organized. (anthropic.com)

That is where Prove2Me entered the picture. The platform represents the project as a directed acyclic graph, or DAG: a network of theorem statements whose arrows show dependencies and never form a loop. Separate AI workers could select unfinished nodes, attempt proofs, and reuse results already checked by Lean. Prove2Me also kept theorem statements apart from their proofs and attached natural-language descriptions, much like a software project separates an interface from its implementation.

The public artifact adds another important detail. It pins the build to Lean 4.33.1 and Mathlib 4.33.0, checks that the final theorem uses only Lean’s standard foundational axioms, and rejects shortcuts such as sorry placeholders or extra axioms. An independent Rust implementation of the kernel also accepted an export of the environment. These checks do not make the proof short, but they make the verification process inspectable and repeatable.

A checked proof is not a replacement for understanding

Machine-checked and human-understood are different achievements. Lean can confirm that a formal proof follows from its definitions and foundations. It cannot automatically tell a reader whether a machine-generated theorem name captures the idea a mathematician intended, or whether an intermediate definition is illuminating rather than merely correct. The repository itself separates kernel-level verification from the reader’s responsibility to understand what each statement means.

That distinction is healthy. Formalization does not replace mathematical exposition; it adds a second layer of confidence. The human proof explains why the argument works. The Lean proof checks that the thousands of individual links actually connect.

From margin to machine

Fermat’s Last Theorem has now traveled from a handwritten margin, through Wiles’s modern proof, into a dependency graph containing millions of lines of formally checked code. The striking lesson is not that computers can perform arithmetic. It is that modern mathematics can be turned into a reusable, testable artifact without losing its logical force.

For future research, a paper may increasingly have two companions: an explanation meant for people and a formal proof meant for a kernel. One tells us why the result matters. The other makes every hidden step wait at the door for inspection.