Generated by Codex with GPT 5.6 Sol XHigh

Techmeme surfaced Anthropic’s September 4 research note, “Formalizing Fermat’s Last Theorem”. The result is not a new proof of the theorem. It is the first complete version of the established proof that a computer can check from end to end—and Anthropic says a team of Claude agents produced it largely autonomously in 11 days.

Turning a famous proof into checked code

Fermat’s Last Theorem says that no positive integers satisfy (a^n + b^n = c^n) when (n > 2). Andrew Wiles proved it in the 1990s using a deep chain of results connecting number theory and algebraic geometry. Mathematicians have since wanted to translate that chain into a proof assistant such as Lean, which accepts a conclusion only when every logical step follows from precisely defined premises.

That translation is difficult because ordinary mathematical writing omits steps that specialists consider obvious and relies on a vast shared literature. Lean permits neither shortcut. A formalizer must define the objects, state all the intermediate claims and supply enough detail for the kernel—the small program at the heart of Lean—to type-check the entire dependency chain.

Claude’s formalization follows a streamlined presentation of the Wiles and Taylor-Wiles argument by Henri Darmon, Fred Diamond and Richard Taylor. It also builds on Mathlib, the community-maintained Lean library, and incorporates work from two existing formalization projects. The achievement therefore compresses a large amount of formalization labor; it does not replace the centuries of mathematics or years of open-source engineering beneath the result.

The scaffold mattered as much as the model

Anthropic reports that dozens of agents wrote about 13 million lines of Lean, generated roughly 30,300 intermediate theorems and used about 29,500 of them in the final proof. The run consumed around six billion output tokens from an internal general-purpose model described as comparable to Claude Fable 5.1. Human direction was limited mostly to occasional high-level prioritization.

The agents did not succeed simply by being pointed at the theorem. Early attempts lost track of project state and stopped coordinating. Progress accelerated only after the team moved the work into Prove2Me, an open collaboration system created by Anthropic researcher Tianyi Peng and colleagues at Columbia University.

Prove2Me represented the proof as a directed graph of theorem statements, allowing agents to see which subproblems were ready and which results other agents had completed. It separated statements from proofs to reduce compilation costs, and attached natural-language descriptions so completed work could be found and reused. The lesson extends beyond mathematics: long-horizon agent work depends on external state, explicit dependencies, cheap feedback and a shared search layer. Model capability alone was not enough.

What “computer-checked” establishes

The published Lean repository makes the central claim unusually testable. Its final theorem states Fermat’s Last Theorem using Lean’s natural numbers and ordinary arithmetic operations. A clean build checks every declaration and fails unless the proof uses exactly three standard Lean axioms. The repository says it contains no proof placeholders such as sorry, no added axioms and none of several other mechanisms that could bypass normal checking.

Anthropic also used Lean’s Comparator project to confirm that the proved statement matches Mathlib’s existing statement of the theorem and that the full dependency graph replays through the kernel. A second, independently implemented kernel called nanoda accepted an export containing more than one million declarations. Kevin Buzzard, who leads the long-running Imperial College formalization effort, reviewed the artifact and endorsed it as a genuine, assumption-free formalization built on the ordinary axioms used by Lean.

Those checks establish a narrow but powerful result: subject to the correctness of the kernels and checking tools, the stated theorem follows from the declared axioms. They do not make the artifact easy for a mathematician to read. The repository explicitly warns that tools cannot verify whether an intermediate theorem’s generated name accurately describes its meaning; the formal statement remains authoritative. Anthropic also patched nanoda to make several checks finish faster, though it says the patches did not change any typing rule. Independent reproduction is possible, but the published instructions call for substantial memory, disk space and computation.

Verification becomes the scalable layer

The deeper significance is not that AI has rediscovered Wiles’s ideas. It is that AI may be able to translate large bodies of existing mathematics into a form where correctness is mechanically auditable. That could expose hidden errors in accepted work and reduce the human burden of checking a growing stream of AI-assisted results.

Formal proof still does not replace explanation. Researchers need readable arguments to understand why a result works, judge whether its definitions capture the intended question and decide what new directions matter. But when generated mathematical output grows faster than the community can review it, pairing human exposition with machine-checkable formalization may become the practical trust boundary. This project suggests that the bottleneck is already shifting from typing millions of proof steps by hand to designing the formal target, the agent scaffold and the independent checks around it.