Claude formalised Fermat's Last Theorem in Lean: what 13 million checked lines teach about verifying agent output

On 4 September 2026 Anthropic published that Claude agents had produced the first end-to-end, computer-checked proof of Fermat's Last Theorem in Lean, the proof assistant, working largely autonomously over 11 days. The run wrote about 13 million lines of Lean, proved 30,300 theorems and used 29,500 of them in the final proof, and consumed about six billion output tokens from what Anthropic describes as "a general-purpose internal research model roughly comparable to Claude Fable 5.1". Dozens of agents worked together through a Claude Code based multi-agent harness. The full proof is on GitHub with a written walk-through.

Most of the coverage read this as a model doing research mathematics. That is not what happened, and the thing that did happen is more useful to anyone who ships software.

This is a verification result, not a new proof#

Andrew Wiles proved Fermat's Last Theorem in 1995, in a proof SiliconANGLE puts at 129 pages, and the result has been accepted for three decades. What did not exist was a version a computer could check from the axioms up, and producing one was a project people expected to take years. Kevin Buzzard at Imperial College London has led a community effort to formalise the theorem in Lean since 2024.

Anthropic is direct about which part is new: "Unlike recent AI-driven work on the Riemann hypothesis, which produced novel mathematics, what's novel here is the verification." The proof also leans on work that already existed. In Anthropic's words, it "adapts pieces from the Imperial College London FLT project led by Kevin Buzzard and the flt-regular project", and according to Techstrong the agents followed a simplified version of Wiles's argument and built on existing formalised mathematics.

So the achievement is not that a model understood Fermat. It is that a model turned an argument humans already trusted into 13 million lines that a machine could check, in less than two weeks.

Why 13 million unread lines are acceptable#

Anthropic notes that at 13 million lines, the proof is "over 5x the size of Mathlib", the community library of formal mathematics it builds on. No person is going to read it. No team could. If this were a pull request, it would be unreviewable by any standard we normally apply.

It does not need a reviewer, because of how the trust is arranged. Anthropic's description: "The finished proof was checked by Lean; it uses just Lean's three standard axioms, and a comparator confirmed that the theorem's statement matches Mathlib's own statement of FLT." Techstrong adds that it contains no omitted proofs, meaning no step was waved through with a placeholder.

That sentence contains three separate guarantees, and each one closes a different gap.

• The kernel checked every step. Lean's kernel is small and heavily scrutinised. If it accepts a proof, every inference in it follows from the ones before.
• Nothing extra was assumed. Three standard axioms means the agents did not quietly add a convenient assumption that makes the hard part disappear. A proof that assumes its conclusion is still a valid proof, just of nothing.
• The right theorem was proved. This is the one I would expect most teams to skip. A proof can be perfectly valid and prove a statement that is subtly different from the one you meant. The comparator checks the statement Claude proved against the statement the Mathlib community had already written down.

Put those together and the trusted surface shrinks from 13 million lines to a kernel, an axiom list and one theorem statement. That is the entire trick. The volume of output stopped mattering because the verification does not scale with it.

The first attempt failed on coordination, not capability#

The detail I found most instructive is the failure. Anthropic writes that "a number of Claude's initial attempts failed: while agents had some early success, they quickly lost track of the project's state and stopped collaborating effectively."

That is not a failure of mathematical ability. The agents could prove things. They could not keep a shared picture of what had been proved, what was still open and what depended on what.

The run succeeded after the switch to Prove2Me, which Anthropic describes as an open collaborative platform for formalising mathematics designed by Tianyi Peng and collaborators at Columbia University. The post lists exactly what it contributed:

1. "Maintaining a directed acyclic graph (DAG) of theorem statements that agents used to decide what proofs they should attempt next."
2. "Speeding up Lean compilation and minimizing resource consumption by separating theorem statements and proofs into different files."
3. "Enabling search and reuse by maintaining a natural-language description of each theorem statement."

Take the mathematics out and those are three of the oldest ideas in software engineering: a dependency graph that doubles as a work queue, a separation of interface from implementation so the build stays fast, and an index written in plain language so work can be found instead of redone.

None of it is new. It was still the difference between a failed run and eleven days. The state of the project had to live in a structure every agent could read, not inside any one agent's context. It is the same argument I made about the MCP specification going stateless: state that lives somewhere nobody can see is the state that fails in ways nobody can debug.

What plays the part of the kernel in ordinary software#

Formal mathematics is the rare domain where a complete checker already exists. Most software has nothing like it, and that is the honest limit of the lesson.

What we have instead are partial kernels, each of which checks one property completely and says nothing about the rest.

• A type checker proves the shapes line up. It says nothing about whether the logic is right.
• A schema validator proves a document is well formed. The SAP Ariba connector I built validates each cXML document locally against the 1.2.033 contract before transmission, which means a malformed document cannot leave. It does not mean the quantities in a well-formed one are correct.
• A database constraint proves an invariant holds no matter what code runs. In MyAdvisor.ai, tenant isolation is enforced with FORCE RLS in PostgreSQL rather than by every query remembering its filter. That is a guarantee about isolation, not about anything else the query does.
• A test suite proves the cases somebody thought of. As I wrote in the code got cheaper, the reading didn't, the bugs that cost the most are rarely in that set.

Each of these lets you accept output you did not read, but only for the property it checks. The useful question for any agent workflow is therefore not "did someone review this?" but "which properties of this output are checked by something mechanical, and which ones are only checked by me?" Everything in the second list is capped by how fast I can read.

The comparator is the part to copy#

If I had to pick one idea from this project to bring into everyday engineering, it would be the comparator rather than the kernel.

The kernel answers "is this internally valid?" The comparator answers "is this the thing we asked for?" Agent-written code fails the second question far more often than the first. It compiles, it passes the tests it wrote for itself, and it solves a slightly easier problem than the one in the ticket.

The Fermat project handled that by fixing the goal outside the work. Mathlib's statement of the theorem existed independently of the run, and the comparator made the agents' final statement answer to it.

The software version is to write the acceptance criteria, the property tests or the contract before the agent starts, keep them outside the agent's reach, and treat any change to them as a change that needs a human. That is where review effort belongs now. Not on the 13 million lines, but on the one statement they are meant to prove. It is the same principle behind "no source, no claim" in high-stakes AI: the guarantee comes from binding the output to something fixed and external, not from how convincing the output reads.

What Kevin Buzzard said#

Buzzard, whose project the proof adapts pieces from, was quoted by SiliconANGLE: "We see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon." In Anthropic's post he goes further: "If the automatic formalization of FLT is possible now, then we have taken a big step towards automatic formalization of the modern mathematical literature."

"Robust enough to be built upon" is the phrase to hold on to. A formal artefact is only valuable if the next person can depend on it without re-checking it, which is exactly what a kernel-verified result allows and a merely plausible one does not.

What I would watch next#

Three things would tell us whether this generalises beyond mathematics.

First, whether the artefact is actually built on. Buzzard's claim is testable: if other formalisation projects start importing results from this proof rather than redoing them, the "robust enough" claim holds.

Second, whether the Prove2Me pattern shows up in coding agent harnesses. A shared dependency graph of what is done and what is blocked, fast incremental builds, and a plain-language index of every unit of work are all things a multi-agent coding setup could adopt tomorrow. The Fermat run is evidence that without them, adding agents did not add progress.

Third, whether anyone ships a comparator for software. A tool that checks an agent's delivered behaviour against a specification the agent could not modify would be the closest thing ordinary code has to what made this proof trustworthy. Until that exists, the checker behind most agent output is still a person reading, and the throughput of agents is still capped by the throughput of that person.