Formalizing Fermat's Last Theorem: How Lean 4 Verifies Math's Hardest Proof

Prologue: A Three-and-a-Half-Century Mathematical Legend

Fermat's Last Theorem is one of the most famous problems in mathematical history. In 1637, French mathematician Pierre de Fermat scribbled in a book margin that tantalizing note that would haunt generations of mathematicians: for integer n > 2, the equation x^n + y^n = z^n has no positive integer solutions. He added that he had discovered a marvelous proof, but the margin was too narrow to contain it.

What makes this theorem special is its extreme simplicity of statement—any middle school student who has learned the Pythagorean theorem can grasp its meaning. It essentially says that while the Pythagorean equation x²+y²=z² has integer solutions (like the classic 3,4,5 or 5,12,13), these solutions completely vanish when the exponent rises to 3 or higher. This "easy to understand, hard to prove" characteristic made it the problem that attracted more amateur enthusiasts and professional mathematicians than any other in mathematical history. For over three centuries, successive generations of brilliant mathematicians—Euler, Dirichlet, Kummer—proved specific cases for particular exponents, but a general proof remained elusive.

This "margin too narrow" legend puzzled the mathematical world for 358 years. Finally, in 1994, British mathematician Andrew Wiles completed a full proof using modern algebraic geometry, modular forms, and elliptic curve theory. Wiles's proof didn't directly attack the Fermat equation itself but took a profound and circuitous route. What he actually proved was the modularity theorem for semistable elliptic curves (a special case of the Taniyama-Shimura-Weil conjecture). Previously, Kenneth Ribet had proven the epsilon conjecture (later called Ribet's theorem) in 1986, showing that if the Taniyama-Shimura conjecture held, Fermat's Last Theorem would automatically follow. The logical chain works like this: assume a counterexample to Fermat's equation exists; from it you can construct a Frey curve with such bizarre properties that it cannot be modular—but if the modularity theorem says all semistable elliptic curves are modular, you have a contradiction, thus no counterexample exists.

Now, a new challenge is unfolding—encoding and verifying this grand proof completely using the formal proof assistant Lean 4.

What Is the Lean 4 Formalization Project

The "Fermat's Last Theorem in Lean 4" project, which recently sparked discussion on Hacker News, is spearheaded by mathematician Kevin Buzzard. Kevin Buzzard is a number theory professor at Imperial College London and one of the most influential evangelists of the formal mathematics movement. He began exploring Lean around 2017 and has since tirelessly promoted formal tools among professional mathematicians. He has publicly challenged the mathematical community's belief that "peer review is sufficient," pointing out that modern mathematical papers have such long citation chains and deep interdependencies that no single reviewer could fully verify a complex result's correctness. His earlier projects—like the Liquid Tensor Experiment, which successfully formalized a key theorem from Peter Scholze's condensed mathematics—have already demonstrated the feasibility of this approach and accumulated valuable experience for formalizing Fermat's Last Theorem.

The goal of this project is to translate Wiles's proof (along with subsequent refinements by Taylor, Wiles, and others) line by line into a formal language that Lean 4 can verify in a computer-checkable manner.

Why Formalization Is Needed

Wiles's proof was accepted by peer review back in 1994, so why invest enormous effort in formalization? The answer touches on a deep anxiety in modern mathematics.

A formal proof means writing every reasoning step of a mathematical proof in a strict formal logic language so that a computer program (called a proof checker or proof assistant) can mechanically verify its correctness. Unlike human readers who may rely on intuition and skip "obvious" steps, formal proofs allow no ambiguity—every step must have explicit logical justification. Lean 4 is precisely such a next-generation theorem prover and programming language, developed by Leonardo de Moura's team at Microsoft Research. It's based on a variant of the Calculus of Inductive Constructions, using dependent type theory as its logical foundation. Compared to its predecessor Lean 3, Lean 4 has qualitative leaps in performance, metaprogramming capabilities, and user experience, and possesses complete general-purpose programming ability, making it not just a proving tool but also a practical programming language.

Wiles's original proof spans over a hundred pages and relies on massive prerequisite theory and results from other mathematicians. Experts worldwide who can fully understand and review this proof can be counted on one hand. In fact, Wiles's initially submitted proof contained a gap that took over a year of effort (collaborating with Richard Taylor) to finally complete.

The significance of formalization is this: once the proof is completely verified by Lean 4, it means the machine has checked every logical reasoning step, eliminating any possibility of human oversight. This provides an unprecedented level of certainty for mathematical truth.

The Scale and Difficulty of the Challenge

Climbing Mathematics' Mount Everest

The difficulty of formalizing Fermat's Last Theorem far exceeds most completed formalization projects. The Lean community has already formalized famous results like the four color theorem and the Kepler conjecture (completed in the Flyspeck project using HOL Light), but the complexity of modern mathematical machinery invoked by Fermat's Last Theorem proof is unparalleled.

Reviewing these completed milestones helps understand the scale of the challenge. The formalization of the four color theorem (2005, Georges Gonthier using Coq) was an early milestone in mathematical formalization, proving that any planar map needs only four colors to ensure adjacent regions have different colors. The formalization of the Kepler conjecture (Flyspeck project, 2014, Thomas Hales's team using HOL Light and Isabelle) verified the densest sphere packing conclusion, a project that consumed approximately 20 person-years. More recent milestones include the formalization of the perfect graph theorem and the aforementioned Liquid Tensor Experiment. Notably, these projects' scale and complexity have been progressively escalating—from the four color theorem to the Kepler conjecture to the Liquid Tensor Experiment, the level of mathematical abstraction involved has risen higher and higher, and Fermat's Last Theorem represents the most ambitious formalization goal to date.

The prerequisite theories that need to be built for the proof include: elliptic curve theory, modular forms, Galois representations, the Taniyama-Shimura-Weil conjecture (modularity theorem), and more. It's necessary to elaborate on these concepts. Elliptic curves are not ellipses but algebraic structures defined by cubic curve equations of the form y²=x³+ax+b. They possess a natural group structure—two points on the curve can be "added" through geometric methods to obtain a third point—making them extremely rich objects of study in number theory, with broad applications in cryptography (such as the ECDSA signature algorithm used in Bitcoin). Modular forms are a class of functions in complex analysis with extremely high symmetry, defined on the upper half complex plane and satisfying specific transformation properties. The Taniyama-Shimura-Weil conjecture (now called the modularity theorem, fully proven by Breuil, Conrad, Diamond, and Taylor in 2001) asserts that every elliptic curve over the rational numbers corresponds to a modular form, establishing a profound connection between two seemingly unrelated mathematical fields, considered an important instance of the Langlands program.

This means the formalization team must not only prove the theorem itself but must first build the entire edifice of modern algebraic geometry and number theory in Lean's mathematical library Mathlib.

Blueprint-Driven Collaboration

Buzzard adopted a methodology called "blueprint" to organize this massive engineering effort. The blueprint method was initially supported by tooling developed by Patrick Massot. Specifically, mathematicians first write traditional-style mathematical proofs in LaTeX while embedding special markup that decomposes the proof into a series of atomic statements (lemmas, definitions, propositions) with clear dependency relationships. The toolchain automatically generates an interactive dependency graph where each node is color-coded: blue indicates formalization completed in Lean, green indicates LaTeX proof written but not yet formalized, and gray indicates not yet started.

The entire proof is broken down into a directed dependency graph, with each node being a lemma or definition, marking which are complete, which are in progress, and which still depend on unestablished prerequisites.

This visualization enables contributors worldwide to work in parallel, each claiming independently completable subtasks. The revolutionary nature of this method lies in decomposing a seemingly impossible massive task into hundreds or thousands of small problems that can be tackled independently, greatly lowering the barrier to participation—even a graduate student might only need to master a certain local domain to contribute to the project. This also reflects a prominent characteristic of modern formal mathematics—it increasingly resembles an open-source software engineering project rather than the individual heroism of lone geniuses.

The Rise of Lean and the Mathlib Ecosystem

Mathematicians' New Toolkit

Lean 4, as both a functional programming language and theorem prover, has seen its influence in the mathematics community surge in recent years. Its core advantages lie in its powerful dependent type system and active community support. Mathlib, as Lean's unified mathematics library, has already collected a massive amount of mathematical theorems from undergraduate to graduate level, becoming one of the largest formalized mathematical knowledge bases to date.

The advancement of the Fermat's Last Theorem project will fundamentally feed back into the entire Mathlib ecosystem. To prove this ultimate goal, the team is forced to complete numerous intermediate layers of modern mathematical theory, and these achievements will permanently remain in Mathlib, available for reuse by all future formalization work.

Formal Mathematics in the AI Era

Formal mathematics is intersecting profoundly with artificial intelligence. In recent years, DeepMind's AlphaProof and various theorem-proving assistance tools based on large language models have begun attempting to automatically generate Lean proofs.

The field of AI-assisted theorem proving has made rapid progress in recent years. DeepMind's AlphaProof demonstrated powerful competition mathematics problem-solving capabilities at the 2024 International Mathematical Olympiad (IMO), combining AlphaZero-style reinforcement learning with Lean formal verification. Meta's research team developed HyperTree Proof Search, automatically proving numerous previously unformalized theorems in Lean and Metamath. Additionally, tools based on large language models like GPT-4 (such as LeanDojo, Copilot for Lean) are exploring the use of natural language prompts to generate formal proof tactics. However, current AI still struggles with proofs requiring deep mathematical intuition and creative construction—they excel at filling in "obvious but tedious" intermediate steps, not proposing key proof ideas.

A project of Fermat's Last Theorem's scale provides an extremely valuable training ground and litmus test for AI-assisted proving. The project contains numerous tedious intermediate steps, precisely the ideal application scenario for AI assistance.

One can foresee that human mathematicians drafting blueprints, AI assisting in filling tedious proof details, and Lean's kernel ultimately verifying—this human-machine collaboration model may well be the prototype of future mathematical research.

Conclusion: The Pursuit of Certainty

Although the discussion heat on Hacker News was relatively modest (41 upvotes, 10 comments), this project's symbolic significance far exceeds its surface attention. It represents the mathematical community's relentless pursuit of absolute certainty and marks the historical process of formal proof moving from fringe tool to mainstream.

When Fermat wrote that famous phrase in the margin, he could hardly imagine that 358 years later, humanity would use something called a "programming language" to thoroughly and irrefutably seal the puzzle he left behind. When Lean 4 finally displays that green verification-passed indicator, perhaps that will be when this mathematical legend truly reaches its conclusion.

Key Takeaways