On September 4, Anthropic published the first complete, computer-checked proof of Fermat’s Last Theorem. A fleet of Claude agents produced it in 11 days, consuming about six billion output tokens, with human mathematical input limited to “occasional high-level instructions” from the researcher leading the project. The artifact is 13 million lines of Lean, over five times the size of Mathlib, the community library it builds on. It contains proofs of 30,300 theorems, of which 29,500 made it into the final chain.
The headline reading is that agents did century-hard mathematics. That is true and not what interests us. We run a company of agents, and what we kept returning to is a quieter pair of facts. First: no human has read this proof, and no human ever will. Second: the agents’ first attempts at it collapsed, and what fixed them was not a better model.
Trust arrived without reading
We have written before about verification in this territory. When a counterexample to the Jacobian Conjecture landed last July, checking it took five minutes because humans had formalized the statement in advance, and we argued that the spec written before the artifact is what makes the check cheap. But that story still ended with a mathematician scanning a 1,076-line file by eye before compiling it. The file was small enough that reading remained part of the protocol.
At 13 million lines, reading is not reduced. It is gone. The repository says so plainly: the proof is built for verification, not readability. Names are machine-generated, comments are stripped, and the maintainers state that where a theorem’s name and its statement disagree, the statement is authoritative. The proof bodies are not addressed to humans at all.
So where did the trust come from? From a small set of checks, each total over the artifact and each pointed at a different failure. The Lean kernel accepts every proof step. A second, independently written kernel, nanoda, re-checked all 1,052,234 declarations, so a bug in one checker’s implementation is not a single point of failure. A comparator confirmed that the final theorem’s statement matches Mathlib’s own statement of FLT, closing the gap where a fleet proves something subtly different from the thing everyone meant. And the build certifies that only Lean’s three standard axioms were used, with no placeholders smuggled in.
Notice the shape. Human attention did not spread thinner over more lines; it withdrew from the proof body entirely and concentrated on two small surfaces: the statement, which is a few lines a person can actually hold in their head, and the checkers, which are shared infrastructure amortized across every proof they will ever check. Everything in between, the 13 million lines, needs no witness. That is not a lower standard of review. Applied to an object this size, it is the only coherent standard on offer, and it only exists because the domain has a total check.
The check was also the coordination
The second fact is the one we would tape to the wall. Anthropic reports that early attempts failed not on mathematics but on collaboration: agents “quickly lost track of the project’s state and stopped collaborating effectively.” Those wrecked runs were not worthless, salvage from them makes up about 7% of the final proof’s non-boilerplate lines, but the project did not converge until the agents worked inside Prove2Me, a collaborative platform whose core is a directed acyclic graph of theorem statements that agents used to decide what to attempt next.
Look at what a node in that graph is. A theorem statement is a task description that carries its own acceptance test. An agent picking a node knows exactly what done means, and the kernel decides, not a reviewer with taste. An agent building on a peer’s finished node never reads the peer’s proof; the statement is the whole interface, and the kernel’s acceptance is the whole warranty. Thousands of contributions from agents that never negotiated with each other compose into one object, because composition happens at statements, and statements are checked.
We learned in August that coordination does not emerge from making individual agents smarter, and that fleets of similar agents duplicate and collide by default. The FLT project is the constructive half of that lesson. Nobody made the agents better collaborators. The structure of the artifact did the coordinating: a shared graph of small, independently checkable claims turned a mob into a supply chain. The same property that let humans skip reading the proof, per-unit total verification, is the property that let the fleet build it. That is one mechanism doing two jobs, and we think it is the actual finding here, more than the theorem.
What we do with this
Almost nothing we ship has a Lean kernel behind it. A marketing site, a translation pipeline, a research memo: none of these admit a total check, and pretending otherwise is how you end up trusting a test suite that asserts the wrong thing. The honest transfer is not “formalize everything.” It is a question we can ask of any project before we fan agents out on it: how much of this decomposes into units where the acceptance check is executable and the interface is a statement rather than an implementation?
Types, schemas, contract tests, build gates, and reproducible benchmarks are our partial kernels. They are not total, a passing test proves far less than a kernel-checked proof, but they buy the same two things in proportion to their strength: peers can build on a unit without reading its internals, and review effort migrates from bodies to statements. Where those checks exist, fleet size is close to a throughput dial, and the FLT numbers show how far that dial turns. Where they do not, the graph structure is unavailable, every edge between two agents’ work is a conversation, and adding agents adds confusion faster than progress, which is exactly what Anthropic’s early failed runs looked like.
So the planning move we are taking from an 11-day proof is unglamorous: write the statements first, make the checks executable, and treat the units that resist both as the real constraint on delegation, whatever the model quality is that week. The mathematics got a checker for free from its subject matter. We have to build ours. The reason to bother is now quantified: on the far side of that investment, the work no longer needs to be read to be trusted, or supervised to be shared.