What does it mean to formalize mathematics? Fermat, Lean, and the gap between human rigor and machine-checkable proof

Anthropic’s announcement sounds strange the first time you hear it: Claude produced a complete computer-checked proof of Fermat’s Last Theorem in Lean.

That immediately raises a reasonable question:

What does it mean to “formalize” a theorem? Isn’t mathematics already formal?

The short answer is: modern mathematics is rigorous, but most mathematics written for humans is not expressed as a complete formal proof for a machine.

That distinction looks small, but it changes a great deal.

A published proof can be perfectly valid for expert mathematicians while still containing hundreds or thousands of steps that a knowledgeable reader reconstructs mentally without needing to see them written down.

A proof assistant such as Lean does not work that way.

It does not infer the author’s intent. It does not accept “obviously.” It does not fill in an omitted lemma because that was probably what the author meant.

The argument must be represented precisely enough that a small verifier—the kernel—can check each step according to explicit logical rules.

That is the shift from rigorous mathematics for humans to formalized mathematics for mechanical verification.

Three levels worth separating

It helps to distinguish three levels.

1. Mathematical intuition

This is where someone suspects a claim is true and has a conceptual reason for believing it.

For example:

“It seems impossible for three powers of this kind to fit together once the exponent is greater than two.”

That can guide research, but it is not a proof.

2. A rigorous proof for humans

Now there is a chain of arguments that specialists can review.

But that chain relies on conventions, notation, experience, and a huge mental library of previous results.

A paper may say things like:

“Applying the standard argument…”

“By the previous lemma, the result follows immediately.”

“The other case is analogous.”

To an expert reader, those phrases may be completely acceptable.

The author does not need to redefine natural numbers, addition, equality, or the logical rules that justify substituting equals for equals.

The mathematical community shares that context.

3. A formal proof

A formal proof removes that dependence on human interpretation from the verification process.

Definitions must exist inside the system. Hypotheses must be explicitly available. Referenced theorems must already have proofs or belong to the accepted axiomatic base. Every transformation has to be legal under the system’s rules.

Instead of:

“This follows by a standard argument.”

a verifier needs something conceptually closer to:

hypotheses
   ↓
lemma A
   ↓
lemma B
   ↓
valid inference rule
   ↓
conclusion

The computer does not need to be “persuaded” by the proof. It needs to be able to replay its validity step by step.

So isn’t mathematics already formal?

In the foundations of mathematics, yes: there is a precise notion of a formal system made of symbols, axioms, and inference rules.

In principle, large parts of modern mathematics can be represented inside suitable formal systems.

But that does not mean every textbook, paper, or blackboard proof is written that way.

Mathematicians work at a much more convenient level of abstraction for humans.

A useful analogy comes from software architecture.

An engineer may draw:

client → API → database

That can describe the architecture correctly, but it is not executable software.

To run it, you still need types, interfaces, error conditions, data formats, dependencies, and thousands of implementation details.

A mathematical proof is similar.

A human proof can correctly describe the logical route without spelling out every micro-step required for a machine to execute it as a formal derivation.

Formalization makes rigor executable.

A tiny example: 1 + 1 = 2

For us,

[ 1 + 1 = 2 ]

is immediate.

A formal system still needs some representation of:

natural numbers;
the number 1;
the number 2;
addition;
equality;
the rules that allow the expression to be reduced or proved.

Modern proof assistants already provide much of that infrastructure through libraries, so users do not start from nothing.

But the principle remains: verification cannot depend on the machine “understanding what we meant.”

Fermat makes the distinction visible

Fermat’s Last Theorem says, in its familiar form, that for positive integers and exponents greater than two there are no solutions to:

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

The statement fits on one line.

The proof does not.

Andrew Wiles, together with later work with Richard Taylor, solved the problem in the 1990s using deep mathematics involving elliptic curves, modular forms, Galois representations, and number theory.

For mathematicians, that was already a rigorous proof.

“Formalizing Fermat” does not mean making a previously informal or untrustworthy argument valid.

It means translating a sufficiently complete mathematical route into objects and proofs that Lean can check mechanically.

Anthropic’s published repository contains a Lean statement with this structure:

theorem fermat_last_theorem
    (n : ℕ)
    (hn : 3 ≤ n)
    (a b c : ℕ)
    (ha : 0 < a)
    (hb : 0 < b)
    (hc : 0 < c) :
    a ^ n + b ^ n ≠ c ^ n

Now it is not enough to say that n is greater than two.

Its type is explicit. The variables a, b, and c are typed. Positivity appears as hypotheses. The conclusion is written in the language Lean knows how to check.

And that is only the statement.

The difficult part is the enormous network of results required to reach it.

What exactly did Lean check?

According to Anthropic, Claude worked on the formalization for 11 days, largely autonomously, and produced about 13 million lines of Lean. The project generated tens of thousands of intermediate theorems; Anthropic reports 30,300 proved during the effort and 29,500 used in the final proof.

The published proof was then built and checked by the Lean kernel.

Anthropic’s repository also includes additional verification. Its FinalCheck.lean ensures the theorem depends only on Lean’s three standard axioms, and a comparator confirms that the proved statement corresponds to the Fermat statement used by Mathlib.

The team also ran an independent second checker, nanoda, a Lean kernel implementation written in Rust.

That does not mean a computer has achieved some metaphysical form of absolute certainty.

There is still a trusted base:

axioms
  ↓
logical rules
  ↓
Lean kernel
  ↓
formal proof
  ↓
theorem

But that base is much smaller and more explicit than asking human reviewers to manually inspect millions of proof steps.

The crucial point is that we do not need to trust Claude because it “reasoned correctly.”

We can let Claude propose millions of steps and trust a much smaller verifier to accept only the ones that obey the rules.

The powerful pattern: probabilistic generator + deterministic verifier

This creates an important connection to agent engineering.

A language model is probabilistic. It can make mistakes. It can pursue a useless path. It can state something false.

Lean plays a different role.

Claude proposes
      ↓
candidate proof
      ↓
Lean checks
   ↙       ↘
reject       accept
  ↓             ↓
retry        valid result

That is a very attractive loop for autonomous systems.

The model does not need to be infallible.

It needs to operate inside an environment where important errors can be detected automatically.

This resembles giving a coding agent compilers, type checkers, linters, and very strong tests.

The difference is that formal proof checking can cover logical correctness far more strongly than ordinary software tests usually can.

The hard problem was not only proving—it was coordinating

Another notable part of Anthropic’s work is that the first multi-agent attempts failed.

Agents lost track of the project’s global state and stopped collaborating effectively.

The successful setup used Prove2Me together with a Claude Code-based multi-agent harness.

Prove2Me maintained a DAG—a directed acyclic graph—of theorem statements and dependencies.

Conceptually:

                 Fermat
                    │
          ┌─────────┴─────────┐
          │                   │
      theorem A           theorem B
          │                   │
     ┌────┴────┐         ┌────┴────┐
     │         │         │         │
   lemma A1   lemma A2   lemma B1   lemma B2

Each agent could see which pieces were ready to work on, which ones depended on others, and which results could be reused.

The graph functioned as external memory and coordination structure.

That matters far beyond mathematics.

For long-running tasks, it is not enough to keep expanding the model’s context window. Project state needs to exist outside the model in artifacts that agents can inspect, verify, and share.

Formalization is not merely “explaining in more detail”

An extremely detailed explanation for humans can still fail to be a formalization.

You can write a hundred pages explaining why a proof works and still be using natural language.

A formal proof is not defined by length. It is defined by being encoded inside a system whose rules allow a machine to verify the derivation.

That is why two complementary artifacts can coexist:

human exposition
  → optimized for understanding

formal proof
  → optimized for mechanical verification

Anthropic also emphasizes that formalization should not replace human-readable exposition.

The two serve different purposes.

Can a formal proof still be wrong?

The careful answer is that the risk moves.

A proof accepted by Lean should not contain an invalid logical step relative to the rules and axioms Lean is checking.

But we still need to ask:

Did we formalize the right theorem?
Do the definitions represent what we think they represent?
Which axioms were used?
Is the kernel correct?
Does the toolchain preserve what it claims to preserve?

That is why Anthropic’s artifact checks the final statement, records the axioms used, and includes a second kernel verification.

Formalization does not eliminate epistemology.

It drastically reduces the amount of reasoning we must accept merely because a human or an AI says it is correct.

Why does this matter now?

For decades, mathematical formalization was expensive because people had to manually translate arguments written for humans into extremely detailed proof code.

AI changes the economics of that process.

If agents can handle much of the mechanical translation and Lean can verify the result, a new pipeline becomes possible:

paper / textbook / mathematical idea
            ↓
formalization agents
            ↓
Lean / Mathlib
            ↓
automatic verification
            ↓
reusable formal proof

That could have several consequences.

Finding errors in existing literature

Results accepted for years could be checked with a depth that human peer review does not always have the time or resources to provide.

Reviewing mathematics produced by AI

If models begin generating more novel mathematical results, the community needs a scalable way to validate them.

AI plus formalization offers one possible answer: do not trust the model’s prose; require an artifact the verifier can check.

Building reusable libraries

Once a theory is formalized, future researchers can build on top of it without re-proving every result from scratch.

Changing the mathematician’s role

Some work may shift from writing every tiny proof detail toward choosing the right definitions, designing strategies, interpreting results, and creating clear human explanations.

The interesting paradox

Mathematics has always aimed at rigor.

That aspiration is not new.

What is new is our ability to represent rigor in a format that a machine can execute as verification.

So the best answer to “isn’t mathematics already formal?” is:

Mathematics can be founded formally, but everyday human mathematics is usually written in a rigorous language that still depends on interpretation, context, and shared knowledge. Formalization removes that dependence from the verification stage.

Fermat’s Last Theorem shows why that distinction is becoming practical rather than merely philosophical.

When a fleet of agents can generate millions of proof steps and a small kernel can check them, formalization becomes more than a specialist technique. It starts to look like infrastructure for doing science with AI systems operating at a scale no human reviewer could inspect line by line.