AI Agents and the Fermat's Last Theorem Formal Proof: What Machine-Verifiable Proofs Actually Deliver

When an AI system claims to have “completed a formal proof of Fermat’s Last Theorem,” what it delivers is not a new mathematical result. It is a logical chain that a machine can re-check statement by statement. The interesting part of the story is not “can AI do mathematics,” but what machine verification means as an engineering problem.

1. First, what did “verified” actually verify?

Fermat’s Last Theorem states that for any integer n > 2, the equation xⁿ + yⁿ = zⁿ has no positive integer solutions. The result itself has long been settled by humans: Andrew Wiles announced the proof outline in 1993, peers found a critical gap, the repaired version was formally published in 1995, and the core paper runs over 120 pages.

What the AI system did was take an already-simplified classical proof route — the Darmon–Diamond–Taylor version — and rewrite it from a human-readable argument into a machine-checkable formal script. Formal verification systems operate under extremely strict rules: they do not accept the human habit of writing “obviously” or “it follows easily.” Every assertion has to state what type its objects have, which premises it depends on, and which rules derive it. Any logical gap immediately becomes a check that fails to compile.

So “verified” means precisely this: the full derivation chain, from the initial axioms and lemmas through to the final theorem, passed a mechanical check by the checker. It does not mean the machine reinvented the proof strategy, and it does not mean the 120-page paper was translated sentence by sentence into code.

2. Two text formats, two different problems

A math paper serves human understanding. The author assumes the reader shares a large body of background, compresses routine derivations into a single line, and relies on trained readers to fill in the gaps. Peer review raises confidence, but it is still bounded by reviewers’ time, attention, and coverage of knowledge — it verifies that “the argument looks sound,” not that “every step is airtight.”

A formal script serves machine checking. The goal is not to be readable but to make every logical step a decidable check item. Consequently the length explodes: a large share of the text goes to type annotations, intermediate helper lemmas, and explicit handling of edge cases. The publicly reported figure for this case is roughly 13 million lines of formal script, possibly more than 5x the size of mainstream mathematics formalization libraries.

That resolves an apparent contradiction. A paper of a hundred-plus pages and a script of tens of millions of lines, following the same proof route, are doing two fundamentally different jobs. The paper lets mathematicians see the idea; the formal script makes the conclusion repeatable and checkable. One optimizes for brevity and insight, the other for completeness and certainty. Neither replaces the other, and neither compresses into the other — reduce the paper to a line of code and you lose checkability; reduce the script back to a paper and you lose certainty.

3. How AI agents fit into the pipeline

Putting a large language model into formal verification is essentially solving a search-and-repair problem: in an enormous proof space, find a complete path that reasons backward from the goal to lemmas that are already established. The setup splits into three cooperating layers.

Layer 1: the proof assistant acts as a deterministic judge.
The formal verification system — an interactive theorem prover — is the foundation of the whole pipeline. It carries a built-in formal logic and type system, and it returns a binary verdict on any proof script submitted: accepted, or an error. The value of this layer is that it cannot be fooled. A model cannot bluff its way past it with vague natural language, and logical errors surface immediately.

Layer 2: the LLM acts as a proof generator.
Given the current proof state — goals already proven, lemmas available, contextual assumptions — the model produces the next tactic or proof term. The typical loop is: the model proposes a step, the judge checks it, and on failure the model reads the error message, backtracks, and regenerates. That forms a closed generate–verify–feedback loop. A schematic proof script looks roughly like this (pseudocode, illustrating structure rather than any specific system’s syntax):

theorem no_positive_solution
    (x y z : Integer) (n : Nat)
    (hn : 3 ≤ n) (pos : 0 < x ∧ 0 < y ∧ 0 < z) :
    x^n + y^n ≠ z^n := by
  -- every placeholder must be filled in: types, premises, referenced lemmas
  -- model proposes a tactic here -> judge checks it -> on failure, backtrack and retry from the error
  ...

Layer 3: multi-agent collaboration handles division of labor and repair.
A proof path leading to Fermat’s Last Theorem has to cross a large number of intermediate theorems. A single model driving forward linearly breaks down easily somewhere in the middle of a long chain. The practical setup is therefore a collaborative system of dozens of agents: different agents decompose subgoals, attempt candidate proofs in parallel, review each other’s results, locate gaps at failure points, and write the missing lemmas. You can think of it as a task force with clear division of labor plus one ruthlessly impartial inspector. The final assembled main proof chain referenced roughly 29,500 intermediate theorems.

4. What the scale numbers mean

The core figures reported for the case are worth reading one at a time:

• About 11 days. From the perspective of heavy human involvement, this is a very short cycle. But it measures the amount of formalization engineering on an existing route, not the difficulty of the mathematics.
• 13 million lines of script. The value of this number is coverage, not length as such. It is probably far longer than necessary — an engineering artifact of remarkable completeness rather than elegance.
• About 29,300 theorems cited (roughly 30,300 proved along the way). The hard part is not writing a single theorem; it is making them join up correctly into one seamless chain.
• About 6 billion output tokens. This indicates the compute and cost magnitude of tasks of this kind, and it is a key input for judging how reusable the approach is.

5. The core difficulty: dependency management

Long proofs are most often broken by their dependency graph. Once a proof references tens of thousands of lemmas, the question is no longer “is this lemma correct,” but:

1. Cycles and gaps. Dependencies between lemmas must form a directed acyclic graph. A single missing or self-contradictory link invalidates everything upstream of it.
2. Local edits trigger global recomputation. Changing a low-level lemma can affect the checked status of hundreds or thousands of theorems above it. This is fundamentally an incremental compilation and dependency caching problem.
3. Naming and reuse conflicts. When tens of thousands of theorems coexist, avoiding duplicate proofs and letting agents quickly retrieve an equivalent lemma that already exists directly determines how fast the loop converges.

For software engineers, this dependency structure is closely isomorphic to build systems, package managers, and module graphs: who depends on whom, which artifacts must be re-verified after one change, and how to cache intermediate results that already passed. That is exactly the engineering problem shared by large-scale formal verification and large codebases.

6. Boundaries: what this can and cannot do

Three boundaries need to be stated plainly:

• It did not invent a new proof. It used a classical route that humans had already simplified. What the AI did was translate and expand, not originate or gain insight.
• It did not reproduce the original paper line by line. The script of tens of millions of lines is a re-expansion of the proof logic and does not correspond one-to-one with paragraphs of the paper.
• It is systems engineering, not a one-shot inference by a single model. Dozens of agents, the verifier, retrieval, and repair mechanisms worked together to reach the result; crediting a single model would be inaccurate.

The honest positioning of current AI in formalization, then, is closer to a highly productive proof engineer assistant: strong at mechanically and completely expanding an idea that is already clear, and at catching errors, but still heavily dependent on humans for proposing entirely new mathematical frameworks and for judging what is worth proving.

7. Lessons for software engineering practice

Setting the mathematics aside, the pipeline offers three directly transferable ideas for software development:

1. Put AI to work inside a decidable loop. Compiler, type checker, test suite, and verifier act as the impartial judge, and the model self-corrects through generate–verify–feedback — which is far more reliable than having a model produce a single output that “looks correct.”
2. Multi-agent division of labor plus deterministic inspection is a general pattern for very large tasks. Splitting a complex goal into sub-tasks that can run in parallel and be verified independently is what makes efficiency and correctness achievable at the same time.
3. Dependency-graph thinking determines scalability. Whether it is a proof chain, a build artifact graph, or microservice call relationships, explicit dependency management with incremental re-verification and caching is the dividing line between a system that scales and one that does not.

The real significance of this work is not that “AI can now do math problems.” It is that it demonstrates a paradigm for producing machine-verifiable, engineering-manageable output — upgrading “looks right” to “was actually checked.” That is precisely what formal verification adds beyond traditional peer review, and where it is most valuable for rigorous engineering.