A proof is not a library

Near the end of a file called PROOF-PATH.md, after eight sections that walk an argument from Frey curves down to cusp forms, there is a heading you would not write unless you were being careful: "Exact strength of the named steps". Under it, six short entries. "Mazur. Proved: irreducibility of E_P[p] for Frey curves (p ≥ 17 by the Eisenstein quotient; p ≤ 13 by Kummer or descent, not modular curves). Not proved: Mazur's theorems on rational isogenies or torsion of general curves." Then the same shape for Langlands-Tunnell, for modularity lifting, for Wiles, for Ribet. Each entry names a landmark of twentieth-century number theory and then says which slice of it is actually inside the repository.

Those thirty lines are the most useful thing in thirteen million, and they are the part nobody is quoting.

On 4 September, Anthropic published what it describes as the first end-to-end, computer-checked proof of Fermat's Last Theorem, together with the Lean sources. The account is unusually specific: eleven days, about six billion output tokens from an internal research model the company calls roughly comparable to Claude Fable 5.1, 29,500 intermediate theorems used in the final proof, 13 million lines of Lean, "over 5x the size of Mathlib, the principal community library". Mathematical input from humans is described as occasional high-level instructions from one researcher, quoted in the post as "Jacobian as a scheme sounds high priority" and "push [the] Mazur [theorem] to be done soon". The earlier attempts failed, the post says, because "agents had some early success, they quickly lost track of the project's state and stopped collaborating effectively".

Argue with none of the verification. It is the strongest part of the release. The theorem is proved, and the way it is proved is worth understanding before deciding what it is worth.

What a kernel actually checks

In Lean, a mathematical statement is a type and a proof is a term of that type. Checking a proof is therefore not reading it. It is type-checking: does this term inhabit that type. The job is done by a small kernel that terminates, has no opinions, and cannot be persuaded. Whatever it accepts, follows.

Two things make that guarantee auditable. First, a Lean term can be interrogated for what it ultimately rests on, and the repository's default build target pins the answer in place: the build fails unless fermat_last_theorem depends on exactly Lean's three standard axioms, propext, Classical.choice and Quot.sound, with no sorry (Lean's admitted hole, which compiles and proves nothing), no added axiom and no native_decide. Second, the kernel is small enough that other people reimplement it. nanoda is one such reimplementation, written in Rust, which takes a list of permitted axioms in its configuration and checks an exported environment against them. Anthropic reports it accepted an export of this one: "Checked 1052234 declarations with no errors."

The third check is the interesting one, because it guards the place where formal proofs really do go wrong. A proof can be impeccable and prove the wrong sentence. comparator, a tool in the Lean organisation's own repositories, builds a challenge file and a solution file separately, exports both, and compares declaration environments to establish that the solution proves "the same statement as provided in Challenge", uses no axioms beyond those permitted, and replays through the kernel. Anthropic ran it against a challenge that states Fermat's Last Theorem using only Mathlib. Verdict: Your solution is okay!

So the epistemic position at the top is tight. Given the Lean kernel, or nanoda instead of it, and a statement written in built-in naturals with +, ≤ and ≠, Fermat's Last Theorem follows from three axioms. Nothing in the rest of this piece disputes that.

What the kernel leaves entirely free

Now notice what the guarantee does not reach. The kernel constrains that each step follows from the last. It says nothing about which steps, how general they are, how long the route is, or what any of it is called. Names sit outside the checked object completely, and the README says so without flinching: "What no tool can check is that each intermediate theorem means what its name suggests; that is for the reader to judge." The sources, it adds, were "written to be checked rather than read": comments removed, machine-generated names, pipeline labels like P2M that are not mathematics, and where a name and a statement disagree, "the statement is what was proved".

Put those two facts together and you can predict the artifact before you open it. A generator searching against a free, total oracle will take the cheapest admissible route, and generality is expensive. Mazur's theorem in its usual form is a substantial piece of mathematics about rational isogenies and torsion on general elliptic curves. What the Frey contradiction needs is narrower: that E_P[p] has no Galois-stable line, handled above p = 17 by an Eisenstein-quotient argument carried out for this situation, with p = 11 and p ∈ {5, 7, 13} holding vacuously because those exponents are settled outright, by descent at 5 and by Kummer's theorem for regular primes above it. That is all the argument consumes, so that is what exists. The same pattern repeats: a Langlands-Tunnell in the octahedral case for surjective residual representations with cyclotomic determinant, level-conditioned modularity lifting at p = 3 and p ∈ {3, 5} for semistable models only, Ribet's level lowering as a congruence of traces at squarefree conductor-supported levels rather than for a general modular mod-p representation.

Cheapest is not the same as tidy, either. The level-lowering step turns out to re-derive modularity along the way, which makes the IsModular hypothesis above it, in the file's own words, "formally unused". A human writing a library would have noticed and restructured. A search that is rewarded for a green build has no reason to.

This is the ordinary behaviour of optimisation against a checkable objective, and it is the same phenomenon a learner meets under a less dignified name when a model games a reward model or a test suite. There is no gaming here. The proof is real. But the verifier still wrote the specification of the artifact, and generality, brevity, naming and readability were not in it.

The library was built by the other project

The contrast is not hypothetical, because the material this run started from came from people doing the opposite thing. The repository's attribution names 106 files containing material from two Apache-2.0 projects: flt-regular, for Kummer's theorem, and the Imperial College London FLT project led by Kevin Buzzard, from which it took the Frey package, Galois representations, deformation theory and patching. That project describes itself as an ongoing multi-author effort, funded by an EPSRC grant until September 2029, following a route planned out by Richard Taylor in discussions with Buzzard. Its visible deliverables are a blueprint and a documentation site: a proof written to be read, in pieces stated generally enough that Mathlib can absorb them.

So the division of labour that actually occurred is the reverse of the headline. The general, reusable machinery was human, slow and public. The machine supplied eleven days of gap-filling at a scale no group of people could match, and what came out the other end is five times the size of Mathlib and contributes nothing back to it. Anthropic says as much, mildly: "our proof is likely much longer than it needs to be".

The strongest case against reading this as a limitation is Anthropic's own, and it does not claim what the coverage claims. The post explicitly declines to offer formalisation as a substitute for exposition, and argues instead that it "may be the only feasible way for the mathematical community to keep up with AI-generated contributions". On that framing, reuse is beside the point. The artifact is not a contribution to number theory; it is a gate that machine-generated mathematics can be made to pass, and a gate you can run in fifteen hours on your own hardware is worth a great deal more than a referee report you wait two years for.

That is a good argument, and it survives. What it concedes is the thing worth holding onto: a gate does not accumulate. Mathlib became general because people read it and wanted the pieces, and the process that generalises a proof runs on legibility. This artifact has had legibility deliberately removed. Twelve more runs like it would leave the field with twelve certified sentences and no new mathematics, which is a real gain and a much smaller one than "Claude proved Fermat's Last Theorem" suggests.

Two things to take from this. When you meet a formal proof, read the statement first, then look for the strength disclosure; this repository wrote one, and its absence elsewhere is information rather than an oversight. And in any setting where a verifier supplies the reward, whether that is a kernel, a test suite or a type checker, assume the artifact will have exactly the properties the verifier checks and no others. Correctness is checked. Generality, minimality, reuse and the possibility of being read by a person are not, so they do not arrive for free, and they will not arrive by scaling.

Thirteen million lines, 1,052,234 declarations, two independent kernels, and the one irreplaceable human act in the whole exercise was somebody looking at a single line, a ^ n + b ^ n ≠ c ^ n, and agreeing that it says what Fermat said.