The Fermat Milestone Is an Orchestration Breakthrough, Not a Math Discovery

Fermat's Last Theorem did not get proved again. Something more operational happened. Anthropic took one of mathematics' most famous verified results, translated the full argument into code that a proof assistant can check, and released the artifact for inspection. The theorem was already true. The new capability is that an agent system converted a mountain of human mathematical literature into a machine-verifiable dependency structure at a speed that had looked ridiculous a year earlier.

On September 4, Anthropic announced what it calls the first complete computer-checked proof of Fermat's Last Theorem. A Claude-based system worked largely autonomously for 11 days, produced about 13 million lines of Lean, proved roughly 30,300 theorems during the run, and used about 29,500 of them in the final proof. Dozens of agents participated. Anthropic published the repository under an Apache 2.0 license, which makes this more than a press-release benchmark.

Kevin Buzzard, the Imperial College mathematician leading a separate multi-year effort to formalize the theorem, did not merely clap from the sidelines. He says he compiled Anthropic's code and ran the comparator against it. His verdict is that it checks out. He also says the result closes the final open item on Freek Wiedijk's list of 100 formalization challenges, a benchmark that has been running for about 20 years. That is serious independent validation from the person with the strongest incentive to notice the shortcuts.

Precision matters because the headline is easy to inflate. Andrew Wiles developed the proof in the 1990s, with Richard Taylor helping repair a gap identified during review. Anthropic's artifact follows a known route through the Frey, Serre, Ribet, Wiles, and Taylor-Wiles argument, specifically a 1995 exposition by Henri Darmon, Fred Diamond, and Richard Taylor. Buzzard says the artifact adds essentially no new mathematics. It formalizes the old proof at an unprecedented scale.

That distinction is not a downgrade. Discovery asks whether somebody found a mathematical idea that was not known before. Formalization asks whether every dependency in an argument can be represented precisely enough for a small software kernel to verify. Human papers routinely omit steps that specialists consider obvious, rely on shared conventions, and cite results spread across decades of literature. Lean does not nod politely and move on. It requires the chain to close.

The brute scale shows what closing the chain demanded. Anthropic says the proof is more than five times the size of Mathlib, the community library it builds upon. The repository exposes 29,511 theorem pages and 1,450 definition modules. Buzzard describes more than 13.4 million lines and says the project took nearly 20 times as long to compile as Mathlib on a 96-core machine. This is not elegant code by human-library standards. It is a working industrial artifact.

The first attempt failed for the same reason long-running agent projects usually fail: intelligence was not the only bottleneck. Anthropic says its agents initially made progress, then lost track of project state and stopped collaborating effectively. Those failed attempts still contributed about 7 percent of the non-boilerplate lines in the final artifact, but the overall workflow stalled. The models could solve local problems. The system could not reliably remember which local problems were finished, blocked, duplicated, or downstream of something broken.

The fix was Prove2Me, an open collaborative formalization platform created by Anthropic researcher Tianyi Peng and collaborators at Columbia University. Prove2Me represented theorem statements as a directed acyclic graph. Each node described a result to prove. Each edge captured a dependency. An agent could inspect the graph, choose available work, and feed completed theorems back into the shared structure. The proof stopped being one impossible document and became a coordinated production system.

That graph did more than assign tickets. Anthropic says Prove2Me separated theorem statements from proof implementations so Lean did not have to recompile the entire project whenever one proof changed. It also attached natural-language descriptions to theorem nodes so agents could search for reusable results without reading millions of lines. Shared state, dependency visibility, targeted compilation, and semantic retrieval did the heavy lifting that a longer prompt could not.

This is the founder-builder lesson hiding inside the mathematics. When agents struggle on long projects, the lazy diagnosis is that the model needs to be smarter. Sometimes it does. Often the model is trapped inside an operating environment that treats memory as chat history and collaboration as agents yelling updates at one another. Prove2Me gave the swarm a real work graph, typed deliverables, a deterministic checker, and a definition of done. The orchestration turned capability into throughput.

Human input did not disappear. Anthropic says Peng occasionally supplied high-level instructions, including which mathematical areas deserved priority. The system also relied on a general-purpose internal research model that Anthropic describes as roughly comparable to Claude Fable 5.1, not an off-the-shelf public model operating without supervision. The company reports about six billion output tokens. It does not disclose a reliable all-in dollar cost, so attempts to convert the run into a clean price tag are speculation.

The verification stack is deliberately layered. The repository says a from-scratch build on Lean 4.33.1 checked all 60,475 modules and every declaration. A separate comparator matched the proved statement and its constants against a challenge expressed through stock Mathlib. An independent Lean kernel implementation written in Rust, called nanoda, accepted an export containing more than one million declarations. The maintainers patched nanoda for progress reporting and speed, and state that those changes did not weaken its typing rules.

The repository also tries to close obvious escape hatches. Its default build checks that the final theorem depends on exactly Lean's three standard axioms: propositional extensionality, classical choice, and quotient soundness. The project modules are scanned for added axioms, unfinished proof placeholders such as `sorry`, native decision shortcuts, unsafe code, external implementations, and other mechanisms that could make a result look proven without supplying the intended proof. That is what trustworthy automation looks like: do not ask the system whether it cheated. Design checks that make common forms of cheating visible.

Even then, verification is not magic. Anthropic's own repository states the trust boundary clearly. The result depends on the correctness of the Lean kernel, nanoda, and the checking tools. A machine can verify the formal statement and all of its logical dependencies, but it cannot guarantee that an English theorem name means what a human reader assumes. The Lean statement is authoritative. Generated summaries and labels are navigation aids, not mathematical truth.

Buzzard performed another useful sanity check after questions about whether the agents might have exploited a software weakness. He says he spent hours examining the repository, inspected the small amount of code that was not a mathematical definition or theorem proof, and sampled the mathematical material. His conclusion was that it genuinely develops the theory needed for the established argument. He calls his method imperfect. That caveat is exactly why the review is credible.

The accomplishment also sits on top of a large commons. The repository credits Mathlib, Buzzard's Imperial College project, and a prior formalization covering regular primes. Its attribution file identifies 106 files containing material from the latter projects and 23 that reproduce Mathlib text. Anthropic did not begin with raw axioms and invent modern number theory in 11 days. The agents consumed a structured base created by mathematicians, software maintainers, research funders, and open-source contributors.

That dependency changes the labor story. Autoformalization can generate working proof code faster than humans can comfortably review, refactor, document, and integrate it. Buzzard says Mathlib maintainers are already constrained by reviewer time and reluctant to accept low-quality AI-generated contributions. A 13 million-line standalone artifact can be correct while still being far too large, redundant, or specialized for a carefully maintained shared library. Verification clears one gate. Stewardship is another profession.

Buzzard's own funded project therefore does not become pointless. He is formalizing a more modern proof, building reusable number-theory objects inside Mathlib, and creating documentation humans can navigate. Anthropic labels its repository a research artifact that is not maintained and does not accept contributions. One project optimized for reaching a verified root theorem. The other is building durable public infrastructure. Those goals overlap, but they are not substitutes.

The near-term value is not that mathematicians can stop understanding proofs. It is that the cost structure of checking them may change. A formal artifact can expose hidden assumptions, missing lemmas, circular dependencies, and imprecise statements before a human referee burns months tracing the same chain. Human attention can move toward choosing the right statement, judging novelty, evaluating whether definitions are useful, and writing an explanation that another mathematician can actually understand.

The longer-term risk is a flood of formally valid junk. A system can produce thousands of correct lemmas that are badly named, needlessly specific, difficult to reuse, or irrelevant to any worthwhile question. Software teams already know this disease. Passing tests does not make a codebase good. Mathematical institutions will need stronger contribution filters, provenance, dependency hygiene, generated-artifact policies, and incentives for the unglamorous work of compression and maintenance.

The architecture travels beyond math because most serious agent work has the same shape. Scientific analysis, chip design, legal review, security engineering, and complex software all involve a large dependency graph, local tasks, shared artifacts, expensive validation, and a final result that cannot be trusted merely because the agent sounds confident. Replace theorem nodes with experiments, design constraints, claims, or test cases. The operating pattern remains: decompose the work, expose the dependencies, persist state outside the conversation, and make completion answer to a checker.

What Anthropic demonstrated is therefore narrower than autonomous scientific discovery and more valuable than a stunt. The model did not wake up with Wiles' insight. A coordinated system converted existing knowledge into an auditable form and survived a project whose scale exceeded any one context window. The next proof point is not another famous theorem chosen for the headline. It is whether researchers can reproduce the build, audit the proof path, compress the artifact, upstream reusable pieces, disclose the compute honestly, and apply the workflow to mathematics whose correctness is genuinely uncertain.

That is the line to watch. Models can already generate more plausible reasoning than experts have time to inspect. If formalization scales, the answer is not to trust the models harder. It is to make their work collide with explicit statements, dependency graphs, small verification kernels, and human judgment at the points where meaning and value enter the system. Fermat's Last Theorem was the test case. The real product is a new way to turn sprawling machine effort into evidence.

LaunchPad positionThe important capability is not a model reciting advanced mathematics. It is an external coordination and verification system that lets many agents decompose a giant proof, preserve shared state, reuse finished work, and submit every dependency to a small checker. That architecture travels far beyond mathematics.