Thirteen million lines of Lean make an arresting answer to a very short mathematical claim. Before reading that number as a measure of intelligence, look at what the files ask the computer to establish. A proof checker can do its job correctly while checking a statement different from the one a reader has in mind.
Anthropic’s September 4 research announcement describes an eleven-day effort that formalized Fermat’s Last Theorem. A Claude Code-based system produced about 13 million lines and proved 30,300 intermediate theorems, using 29,500 in the final proof. The work translates an established result into machine-checkable logic. Anthropic says it used an internal research model roughly comparable to Claude Fable 5.1, rather than demonstrating the capability of every public Claude model.
The Hacker News submission was the discovery signal. Anthropic’s report and proof repository supply the technical account. They give readers something more specific than an impressive answer: a target statement, a derivation and a route for checking whether one follows from the other.
Start with the sentence the computer is asked to prove
Fermat's Last Theorem states that no positive integers can satisfy the equation aⁿ + bⁿ = cⁿ when n is an integer greater than two. Andrew Wiles and Richard Taylor established the result in the 1990s through a proof built on modern number theory. The current project translates a route through that mathematics into the formal language of Lean.
The familiar name on a proof file cannot establish that connection by itself. The formal target could omit a condition, express a weaker claim or use a definition with an unexpected meaning. A reviewer needs to compare the encoded proposition with the theorem the project set out to formalize. That is a different job from checking each step of the derivation.
Anthropic's released repository exposes that target directly. The theorem quantifies over natural numbers, requires a positive exponent of at least three and positive values for a, b and c, then states that aⁿ + bⁿ cannot equal cⁿ. The repository's final checking entrypoint also derives Mathlib's own formulation of Fermat's Last Theorem from this statement.
Think of those as two questions with separate answers. Is this the intended statement? Does the submitted proof establish it? A successful compilation helps with the second under the checker’s rules. The comparison with the independently specified target addresses the first.
Read the assumptions beside the green result
The final check reports three standard Lean axioms: proposition extensionality, classical choice and quotient soundness. It also rejects common escape hatches such as unfinished sorry placeholders, added axioms and native computation shortcuts. These controls make the logical boundary explicit.
Those declared assumptions tell a reviewer what the green result rests on. A proof is checked within a formal system, whose rules need to be part of the account. Publishing them makes it possible to inspect the logical boundary alongside the final theorem.
The Lean comparator project supplies a second layer. It compares the submission with a reference challenge, constrains the permitted axioms and replays the environment through the Lean kernel. The repository reports that the comparator confirmed both the target statement and its dependencies.
A matching statement with a broken derivation leaves a proof unfinished. A valid derivation of the wrong target leaves the original question unanswered. Keeping both checks visible explains more than a single success badge, especially in a project too large to follow line by line.
A second checker and a second investigator add different evidence
Anthropic also reports that nanoda, a Lean kernel written independently in Rust, accepted an export of the same environment after four disclosed patches. Three patches speed up equality checking and one adds progress output. According to the repository, none changes the typing rules.
A second implementation gives some software errors another chance to be caught. It reduces reliance on one codebase. The reported run still belongs to Anthropic’s verification process. External replication would add another investigator who obtains the materials, follows the checking route and records what happened.
“Independent” needs an object here. The software implementation can be independent while the organization running it is the same. A second kernel and an outside reproduction add different kinds of confidence. Naming each makes the evidence easier to follow without asking one to stand in for the other.
The cost of that reproduction is substantial. Anthropic's repository estimates about 67 GB of disk for the initial build, reports a peak of 153 GB of memory at high parallelism and says its comparator run used 230 GB of memory over nearly fifteen hours. The nanoda path also requires a large exported environment. Those requirements make the artifact inspectable, but they limit how many independent teams can immediately reproduce the complete process.
A checked proof still needs a route for its reader
Lean follows the declared rules through the proof. A mathematician needs a route through the ideas too. The repository supplies a proof-path document, browser-readable pages, dependency graphs and exact statements for thousands of intermediate theorems. Those are ways into an artifact whose scale would otherwise make it difficult to navigate.
A checked artifact can establish its stated target while leaving work for someone who wants to understand, maintain or reuse the mathematics. These questions meet at the same files, but they reward different qualities. The checker needs valid steps. A future researcher also needs to find the steps that explain the route.
Line count describes scale, with little information about elegance. Anthropic says the proof is more than five times the size of Mathlib and likely much longer than necessary. The dependency structure offers a more useful path into it: which intermediate results connect, and where does earlier human mathematics enter?
That human foundation is extensive. The project follows a simplified version of the Wiles proof described by Henri Darmon, Fred Diamond and Richard Taylor. It builds on Lean, Mathlib, previous formalization projects and centuries of mathematics. Claude's contribution is the large-scale assembly and checking of that material through Anthropic's agent workflow.
Follow the checking route into another domain
The release puts several pieces of evidence within reach: the named target, an executable artifact, the assumptions and instructions for checking. Another team can follow that route and record its own result. The practical cost of doing so remains part of how widely the claim can be examined.
Our earlier EEBench analysis shows the boundary in another domain. A circuit design can pass simulation while leaving fabrication and physical measurement unresolved. A Lean proof has a different target, with specification and software assumptions of its own. In both cases, the useful question is exactly what passed and what remains outside the test.
A mathematician approaching the release has a more useful entry point than the thirteen-million-line total. Open the final theorem, follow a dependency and see where it connects to the checking record. The path through it lets someone else decide whether and how to build on the work.
