That distinction matters. A Lean proof can offer an unusually strong kind of assurance about whether formal statements follow from explicitly accepted axioms and definitions. It does not by itself show that an AI understood the mathematics as a human mathematician does, nor does it eliminate the need to inspect whether the formal statement captures the intended result. Still, the reported artifact is a consequential test case for AI-assisted formalization, software verification, and the increasingly blurred boundary between mathematical research and large-scale engineering.
What Anthropic says it produced
Anthropic announced the work on September 4, 2026, describing an approximately 11-day effort in which dozens of collaborating Claude agents worked largely autonomously. The reported output is extraordinary in volume: about 13 million lines of Lean code, proofs for roughly 30,300 theorems, and about 29,500 of those theorems used by the final development.
Lean is a proof assistant: a programming environment in which definitions, statements, and proof steps are represented in a rigorous formal language. Its kernel checks whether a submitted proof conforms to its rules. In ordinary terms, that changes the question from “does this enormous argument look persuasive to a reader?” to “does the formal checker accept every required step under its specified foundations?”
The repository’s top-level result is reported to cover the familiar general form: for natural-number exponents (n \geq 3), no positive natural numbers (a), (b), and (c) satisfy (a^n + b^n = c^n). The default build also derives Mathlib’s existing statement of Fermat’s Last Theorem. Mathlib is the widely used community library of formalized mathematics for Lean.
The project reportedly includes safeguards intended to make shortcuts visible. It blocks sorry, a Lean facility that can stand in for a missing proof during development; blocks added axioms; and blocks native_decide, another mechanism the authors did not want used in the final result. Its recorded logical basis contains Lean’s three customary axioms: propositional extensionality, classical choice, and quotient soundness.
This is substantial, but the right conclusion is conditional. The repository itself frames validation as establishing the theorem given trust in the relevant kernels and checking tools. That is a much more precise claim than “proved with no assumptions.” Every formal system has a trust boundary: the kernel, the compiler and environment used to run it, the meaning of imported libraries, and the correctness of the statement being formalized all remain relevant.
Three checks, and what each one does
The project documents three distinct validation layers.
First is a from-scratch Lean build. This is the baseline reproducibility test: can the code be rebuilt and accepted by Lean rather than simply trusted as a supplied compiled artifact?
Second is a comparison check using leanprover/comparator. The reported setup compares the exported development against a challenge statement that depends only on Mathlib. This is designed to help establish that the result really connects the giant generated development to a clean target theorem, instead of quietly relying on an inappropriate dependency.
Third is an exported-environment check with nanoda, an independently written Lean kernel implemented in Rust. A separately implemented checker is useful because it can reduce reliance on a single kernel implementation. However, it is not magic independence: the report notes four Anthropic patches to nanoda, characterized as performance and progress changes rather than changes to type-checking rules. That characterization is important, but it is still something outside reviewers should scrutinize.
The distinction among these tests is more than procedural. A successful Lean compile shows that Lean accepts the code. Comparator tests whether the exported material matches a constrained challenge setting. A second kernel creates an additional implementation path for checking the formal environment. Together they make an accidental or obvious shortcut less likely; they do not answer every question about software supply chains or mathematical interpretation.
Independent checking is encouraging, not the same as peer review
Kevin Buzzard, who leads the continuing Fermat’s Last Theorem formalization work at Imperial College London, has said he compiled Anthropic’s codebase and ran comparator himself. He concluded that it checks out. He also puts the codebase above 13.4 million lines and reports that compilation took nearly 20 times as long as Mathlib on a 96-core machine.
That is meaningful external technical scrutiny, especially from a mathematician deeply familiar with Lean formalization and the subject area. It should not be inflated into a claim that the project has completed broad external peer review. The repository metadata reportedly marks the work as “self-assessed” and lists no reviewers. The available information also does not establish how many other independent groups have reproduced every published run, nor whether anyone has completed a line-by-line review of the generated mathematical development.
There is another limit inherent in formal verification. A checker can determine that a Lean theorem follows from its inputs. It cannot automatically establish that every generated theorem name, English explanation, or intended informal interpretation accurately corresponds to the formal object in the file. Formal syntax sharply narrows one class of errors; semantic correspondence remains a human task.
It formalizes existing mathematics rather than discovering it
Fermat’s Last Theorem says that no positive integer solutions exist for (a^n+b^n=c^n) when (n) is greater than two. Andrew Wiles’s work, subsequently completed with Richard Taylor, established the theorem in the 1990s. The reported Claude artifact follows the 1995 Darmon–Diamond–Taylor exposition of the Wiles/Taylor-Wiles approach.
Buzzard’s characterization is therefore crucial: this is an autoformalization advance, not new mathematics. In his assessment, it adds nothing mathematically beyond the existing literature. That is not a dismissal. Re-expressing a sophisticated proof so that a tiny proof kernel can verify it is an enormous undertaking, especially when the result spans advanced number theory and depends on a substantial ecosystem of supporting results.
The provenance also corrects any impression that agents reconstructed the argument from a blank page. Anthropic says human direction was limited to occasional high-level instructions, but the repository acknowledges its foundation in human-written open-source Lean and attributes material to the Imperial College FLT project, flt-regular, and Mathlib. The system also used Prove2Me, described as a collaborative platform and specialized harness through which agents can build on one another’s work.
In other words, this was not one chatbot typing a proof into a text box. It was a coordinated computational workflow operating on accumulated human mathematical knowledge, formal libraries, project code, and tooling.
A scope nuance behind the all-exponents theorem
The public top-level theorem is reported to state the result for every natural exponent (n \geq 3). Yet the route through the work needs careful description. Buzzard says Anthropic’s proof route establishes the case for prime exponents (p \geq 17), while existing formalized results for odd regular primes cover the other relevant prime exponents. The assembled repository can therefore expose the general all-(n) theorem while relying on previously formalized work for part of the necessary coverage.
That is normal in a formal library, where a final theorem can depend on earlier modules. But it makes a difference to claims about what the new AI-produced contribution specifically achieved. The final artifact may prove the full statement; it does not follow that every part of the proof stack was newly generated during this 11-day run.
Scale makes this a systems story as well as a math story
The numbers suggest that the central bottleneck is not merely model reasoning. It is coordination, storage, builds, and verification of a huge dependency graph.
The published instructions reportedly estimate a 67 GB working directory, up to 220 GB of intermediate C files, a five-hour-and-32-minute build with 96 jobs, and around 15 hours plus up to 300 GB of RAM for comparator checking. Those figures are not a complete measure of the original AI run’s cost; Anthropic disclosed about six billion output tokens, but the available material does not establish total compute spending, energy consumption, staff time, or whether a different organization could reproduce the result with publicly available models and tools.
For Windows and PC users, the practical conclusion is straightforward: this is not evidence that a typical desktop can now formally verify a landmark theorem on demand. The reported validation envelope resembles a serious shared compute or server workload. Storage capacity, abundant memory, many CPU cores, build tooling, and tolerance for long compilation times matter as much as the AI model itself.
It also illustrates a broader future for developer tools. In conventional software, unit tests can demonstrate expected behavior for selected cases. Formal methods aim for something stronger: proof that a program or critical property follows from a specification. If agent teams become capable of constructing large checked proof artifacts, the nearer-term applications may be safety-critical code, cryptographic implementations, compilers, protocols, and hardware specifications—not just headline-grabbing theorems.
The challenge will be usability. A 13-million-line artifact that checks is valuable, but it is not automatically readable, maintainable, or suitable for direct inclusion in a community library. Buzzard has emphasized that the project does not replace a more comprehensible development designed for long-term Mathlib integration. In software terms, passing a build is essential; maintainability, reviewability, and provenance still determine whether a project becomes durable infrastructure.
Do not confuse this with other AI math claims
The wider AI-mathematics race is easy to describe carelessly. Anthropic previously reported improving a lower bound from 41.6% to 67.2% for the fraction of zeros satisfying the Riemann hypothesis. It explicitly said Claude did not prove or disprove the Riemann hypothesis. That is a research advance on a related quantitative question, not a resolution of the famous conjecture.
OpenAI separately said in August 2026 that an internal version of its then-upcoming Astra model had resolved or made substantial progress on ten long-standing mathematics and theoretical-computer-science problems, with arguments formalized into Lean certificates. That is broader than a claim that an existing public model merely narrowed a handful of questions, and it should be evaluated on the evidence for each individual result.
Anthropic has also announced scientist support that includes free or discounted Claude Team seats and grants or API credits for high-impact projects. Formalization can be among the supported project types, but the program is not limited to mathematicians or formalization work.
The real milestone is trustworthy automation at scale
The strongest supported interpretation is neither “AI has solved Fermat’s Last Theorem” nor “this is just automated typesetting.” If the reported checks continue to reproduce under wider scrutiny, Claude’s work represents a notable demonstration that agent-based systems can construct an immense, kernel-checkable formalization of advanced, pre-existing mathematics while reusing the community’s software and proof infrastructure.
Its remaining questions are the ones that determine long-term significance: How reproducible is the workflow outside Anthropic? Can specialists audit the generated architecture and its relationship to the intended proof? Can artifacts of this size be made maintainable? And can the approach lower the cost of formal verification rather than merely move it into an enormous compute pipeline?
For now, the result is best understood as a demanding engineering benchmark for AI-assisted proof, backed by meaningful checks but not freed from the ordinary requirements of independent replication and expert review. That is still a remarkable development—and potentially a more useful one than a dramatic but imprecise claim of machine mathematical discovery.