What the Fermat's Last Theorem Lean 4 formalization by AI shows about verifier loops

The output of the run is therefore not a claim a reviewer has to weigh by taste. It is an artifact a kernel accepts or rejects, and the repository ships three checks. A from-scratch lake build of all 60,475 modules with Mathlib compiled from source; leanprover/comparator v4.33.0 run against verification/comparator/Challenge.lean, which states the theorem using only Mathlib, with the verdict "Your solution is okay!"; and nanoda 0.4.13, an independent Lean kernel written in Rust, which accepted an export of the same environment and reported "Checked 1052234 declarations with no errors".

The statement in Theorems/Thm_fermat_last_theorem.lean is written with Lean's built-in natural numbers, +, ≤, < and ≠. Its one Mathlib ingredient is ^ on ℕ, which Mathlib defines as Lean's built-in exponentiation. FinalCheck.lean derives Mathlib's own FermatLastTheorem from it, and comparator confirmed that the proved statement and every constant it mentions are identical to the challenge, that no other axiom is used, and that the whole proof, Mathlib included, replays through the Lean kernel.

The repository is explicit about the boundary of what this establishes. The checks show that the statement follows from the three axioms, given trust in the Lean kernel (or nanoda) and the checking tools. What no tool can check, in the README's own words, is that each intermediate theorem means what its name suggests; that is left to the reader, with PROOF-PATH.md naming the Lean theorem behind each step. That gap is the one every engineer meets when an agent turns a red test suite green: the machine confirmed a property, not necessarily the property you meant.

The baseline matters for reading the 11 days. Wiles's first proof, published in May 1995, ran to 129 pages and required months of painstaking work to verify. Formalization was expected to take years, and the blueprint the mathematical community has been using for just the initial phase of the effort Kevin Buzzard kicked off at Imperial College London in 2024 runs to 86 pages.

A number of Claude's initial attempts failed. Agents had some early success, then quickly lost track of the project's state and stopped collaborating effectively; those runs contributed about 7% of the non-boilerplate lines in the final proof. The effort succeeded after the switch to Prove2Me, an open collaborative platform for formalizing mathematics designed by Tianyi Peng and his collaborators at Columbia University, driven by a Claude Code-based multi-agent harness. Dozens of Claude agents then collaborated to define concepts, prove intermediate theorems, and use those theorems to prove harder statements.

Anthropic names three properties of that platform that did the work, and all three have direct analogues in ordinary software:

Read that as a shared task graph with typed interfaces, an interface and implementation split so a change to one body does not force a global rebuild, and a searchable index so an agent finds the existing helper instead of writing a fourth copy of it. Mathematical input from Tianyi Peng was limited to occasional high-level instructions such as "Jacobian as a scheme sounds high priority" and "push [the] Mazur [theorem] to be done soon."

Lean's sorry admits a goal without proving it, and the repository treats it as a build-breaking token: no module of the proof contains sorry, and Challenge.lean uses sorry by design and is not part of the package. The sources do not describe how Claude used sorry during the run, how many stubs were open at any point, or whether stubbing was part of the search strategy at all. What they do describe as the decomposition mechanism is Prove2Me's DAG of theorem statements, held in files separate from the proofs, with the links maintained independently.

The engineering analogue is a declared signature plus a test that asserts its contract, not a TODO comment. A TODO is invisible to the compiler; an unimplemented function with a type and a failing test is a node the toolchain can count, and a build gate turns the open set into a work queue with a hard exit condition. Without a gate the toolchain enforces, the most likely output of an agent fleet is code that satisfies the checker without doing the work.

Lean returns a binary verdict on every attempt, deterministically, which is what makes brute search over proof attempts viable in a way it is not against a human referee. The sources do not report how many Lean compilations were run, the per-attempt success rate, or the split of the six billion output tokens between generation and repair. What they do report in detail is the cost of checking the finished artifact once.

Kevin Buzzard compiled the codebase and ran comparator himself, and reports that it checks out. He puts the size at over 13.4 million lines and says it takes nearly 20 times as long to compile as Lean's mathematics library on a 96-core machine, and that Lean is sluggish jumping from file to file on a repository of this size even on the 500 GB machine Anthropic gave him access to. In the comments on his post, David Jao computed that six billion output tokens would be $300,000 at API prices; that is an inference from list pricing, not a figure Anthropic published, and Anthropic reports no dollar cost.

Three things transfer cleanly. First, the verifier has to be cheap enough to run per attempt and strict enough that passing means something; the FLT build fails on a single sorry or added axiom, and that is a CI policy anyone can copy. Second, orchestration state belongs outside the agent context, because the Prove2Me DAG exists precisely because agents lost track of the project's state. Third, compile-time economics dominate at scale, which is why separating statements from proofs into different files is listed alongside the DAG as a reason the second attempt worked.

What does not transfer is the completeness of the oracle. A type checker rules out a narrow class of errors and a test suite covers only the behaviours someone wrote down; neither is a kernel replay of every declaration beneath the top-level claim. Buzzard's read on the mathematical content is worth holding onto: he writes that the work "tells us essentially nothing" mathematically, because the formalization faithfully follows the early literature on the proof and adds nothing. The demonstration is about the loop, not about the theorem.

The proof follows the Darmon–Diamond–Taylor exposition from 1995 of the Wiles–Taylor–Wiles argument, via the Langlands–Tunnell theorem and Ribet's level-lowering theorem, not the modern route via Khare, Taylor and others that Buzzard has been formalizing. Buzzard reports that the repository develops Fontaine theory, to study flat deformations of Galois representations, and enough of Mazur's work on the Eisenstein ideal to conclude that no Frey curve can have a point of a particular order, and that the resulting argument covers only a restricted set of exponents; the published text of his post drops both the order and the exponent condition, so the specific values are not recoverable from the sources. He notes the remaining cases were already handled, because FLT was formalized for odd regular primes by Best–Birkbeck–Brasca–Rodriguez–van-der-Velde–Yang and the smallest irregular prime is 37, and Anthropic says its proof adapts pieces from the Imperial College London FLT project and the flt-regular project. Buzzard also records that this was the final theorem on Freek Wiedijk's list of 100 formalization challenges, closing a 20-year-old benchmark.

Several things the sources do not report: any per-attempt success rate, the number of Lean compilations, dollar cost beyond the token count, and how the Claude Code-based harness allocated work among agents. The repository is labelled a research artifact, not maintained and not accepting contributions; its 390 MB html/ folder carries a page for each of the 29,511 theorems and each of the 1,450 definition modules, was machine-tested in a Chromium-based browser only, and its English summaries and suggested references are generated automatically while the Lean statement is authoritative. Anthropic offers one smaller data point on scaffolding: three personal Claude Max plans, collaborating entirely through Prove2Me, jointly completed a formalization of Vinogradov's Three Primes Theorem in three days, which Anthropic reads as evidence that collaborative formalization of major results with consumer AI subscriptions is achievable with the right scaffold.

If you want to test the transfer on your own codebase, the cheap first move is the one the FLT repository makes: fail the build on the equivalent of a sorry, and put the task graph somewhere the agents read from rather than somewhere they have to remember.