The Real Breakthrough Isn’t Re-Proving Fermat—It’s Making Math Auditable

Anthropic is working to formalize Fermat’s Last Theorem in Lean 4. That may sound like AI has cracked a legendary problem all over again. The more interesting story is that mathematics is starting to build its own version of automated testing.

Nobody Is Re-Proving Fermat

Fermat’s Last Theorem says that no positive integers (a), (b), and (c) satisfy

[ a^n+b^n=c^n ]

when the integer (n) is greater than 2.

Pierre de Fermat wrote the claim around 1637. Andrew Wiles announced a proof in 1993, but reviewers found a gap. Wiles and Richard Taylor repaired it, and the completed work was published in 1995.

Anthropic’s project is not searching for a different proof. It is translating an accepted human proof into a form that Lean can check step by step.

That distinction matters. Saying “Anthropic’s AI proved Fermat’s Last Theorem” would be misleading. The actual task is to turn a human argument into machine-verifiable mathematics.

A Paper Is Not Executable Code

Mathematical papers leave a lot unsaid. Experts routinely skip familiar calculations, omit standard definitions, and compress entire chains of reasoning into phrases such as “clearly” or “by the same argument.”

Lean allows no such shortcuts.

Every definition must be explicit. Every theorem application must meet its exact conditions. If one assumption is missing, the proof stops compiling.

Wiles’s proof makes this especially difficult. It does not attack Fermat’s equation directly. It travels through a vast landscape of modern number theory, including elliptic curves, modular forms, and Galois representations.

Formalizing the final theorem without that supporting theory would be like shipping an app without its dependencies. The headline result may be the visible product, but years of infrastructure sit underneath it. As the formal proof grows, the surrounding mathematical library must grow with it.

The AI Writes; Lean Checks

An AI trying to solve a new mathematical problem explores possible arguments. It may propose a new lemma, combine familiar results in an unusual way, or search through approaches that eventually fail. That work depends on creativity and judgment.

Formalization is a different job. An AI can translate prose into draft Lean code, locate supporting lemmas, repair type errors, and identify assumptions that the original paper left implicit.

But the language model does not get the final vote.

Lean’s small trusted kernel checks whether each proof term follows the system’s rules. A model can produce code that looks elegant and remains completely wrong. If the kernel rejects it, it is not a proof.

The closest software analogy is a pull request backed by an unusually unforgiving CI pipeline. The AI can write the patch. Lean decides whether it passes.

Formalization Exposes the Hidden Structure

Machine checking is useful for more than catching mistakes. It reveals the dependency graph buried inside a proof: which definitions matter, which assumptions are essential, and which results depend on which earlier lemmas.

That structure makes mathematics easier to reuse. Once a definition or theorem has been formally verified, researchers can treat it as a trusted component in later work. The model starts to resemble open-source software, where reliable libraries support increasingly ambitious systems.

There is an important limit, though. A proof that Lean accepts is not automatically a proof that humans will understand.

Verification and explanation are different products. Lean can establish that every logical step is valid. It cannot guarantee that the argument offers intuition, teaches the underlying ideas, or tells a compelling mathematical story.

Mathematics Is Getting a New Production Stack

The significance of this project is larger than Fermat’s Last Theorem. It points toward a workflow in which humans develop the ideas, AI handles much of the formalization, and a proof assistant verifies the result.

Software engineering changed when testing, version control, and automated checks became standard practice. Mathematics may now be approaching a similar shift.

The biggest question is not whether AI will beat humans to the next famous proof. It is how much of the mathematics we already trust can become auditable knowledge.