Anthropic Claude Formalized Fermat’s Last Theorem. It Did Not Discover the Proof

Anthropic Claude completed an 11-day formalization of Fermat’s Last Theorem, but it did not discover the theorem or replace Andrew Wiles’s proof. The distinction matters because the achievement concerns verification, scale, and research automation. It is not a new solution to a previously unsolved problem.

Anthropic announced the result on September 4, 2026. The company says dozens of Claude agents produced 13 million lines of Lean code and proved 30,300 intermediate theorems. Of those results, 29,500 appear in the final proof.

Lean is a proof assistant, meaning it checks whether each formal step follows from explicit definitions, axioms, and earlier theorems. Formalization converts mathematics written for expert readers into instructions precise enough for Lean’s logical kernel to verify.

That process sounds clerical until the proof spans modern number theory, algebraic geometry, harmonic analysis, and representation theory. Human authors routinely omit familiar steps. Lean accepts none of those shortcuts.

The Claude Fermat proof therefore creates a sharper contest than AI versus mathematicians. The important comparison is machine-scale formalization versus carefully maintained, human-readable formal mathematics.

That tension places Kevin Buzzard’s ongoing Imperial College London project at the center of the story. Anthropic’s system reached an end-to-end checked result quickly, while the community project has emphasized reusable libraries, readable abstractions, and reviewed contributions.

Both routes can produce valid formal mathematics. They optimize for different outcomes, and Anthropic’s result forces researchers to decide which qualities matter after the kernel says yes.

What Anthropic Claude Actually Completed

Anthropic Claude translated an established mathematical argument into a complete machine-checked artifact, which is different from inventing the proof.

Fermat’s Last Theorem states that no positive integers satisfy aⁿ + bⁿ = cⁿ when n is greater than two. Pierre de Fermat wrote the claim around 1637, but no accepted general proof appeared for more than three centuries.

Andrew Wiles announced a proof in 1993. Reviewers later found a serious gap, which Wiles repaired with Richard Taylor before the corrected work appeared in 1995. That history is relevant because it demonstrates how difficult ordinary mathematical review can become.

Claude did not find another route around Wiles. According to Anthropic’s formalization account, the system followed a simplified exposition by Henri Darmon, Fred Diamond, and Richard Taylor.

The argument still rests on the mathematical chain created by Gerhard Frey, Jean-Pierre Serre, Ken Ribet, Wiles, Taylor, and many others. Claude’s task was to express that chain in Lean without relying on an expert reader to fill gaps.

Anthropic describes the result as the first complete computer-checked proof of Fermat’s Last Theorem. That language is defensible when “proof” refers to the finished formal artifact. It becomes misleading if readers interpret it as a new mathematical discovery.

A formal proof and an informal proof perform related but distinct jobs. A mathematical paper explains ideas to qualified humans, while a formal proof gives a logical kernel enough detail to verify every dependency.

Lean does not accept a sentence because specialists recognize it as standard. Every definition must exist. Every type must match. Every imported result must connect to the final statement through an explicit sequence of valid terms.

Anthropic says the effort began when researcher Tianyi Peng tested whether Claude could advance the formalization. Peng works with a Columbia University group that develops tools for AI-assisted formal mathematics.

The system initially struggled. Anthropic reports that early agents lost track of the project and stopped coordinating effectively. Those failed attempts still contributed about 7% of the final proof’s non-boilerplate lines.

The successful run used Prove2Me, an open collaboration platform that represents a formalization project as a directed acyclic graph. Each node captures a theorem statement, while dependencies tell agents which results must be completed first.

Claude agents used this structure to divide work, search existing results, prove intermediate statements, and reuse completed components. Anthropic paired the platform with a Claude Code multi-agent harness.

The company says the final campaign consumed about six billion output tokens from an internal general-purpose research model. Anthropic described that model as roughly comparable to Claude Fable 5.1.

Those numbers establish the scale of the computation, not the general reliability of Claude. Anthropic has not provided a success rate across comparable formalization projects or a complete denominator of failed campaigns.

The completed artifact is nevertheless concrete. Its public Lean repository states the theorem for positive natural numbers and every exponent of at least three.

The repository also includes a proof path, source files, verification materials, and browsable generated pages. That makes the central mathematical claim more inspectable than a demonstration shown only through screenshots or selected transcripts.

The release date also resolves the timing gap in the original hot-list item. Anthropic published its announcement on September 4, 2026, two days before this article’s publication date.

Why the Claude Lean 4 Result Matters

The meaningful change is that a general-purpose AI system crossed the scale barrier for formalizing a major body of established mathematics.

Before this release, formalizing Fermat’s Last Theorem was already an active international project. Kevin Buzzard leads an open effort at Imperial College London, supported through a grant scheduled to run until September 2029.

Its formalization project does more than pursue one final theorem. Contributors build reusable foundations in number theory, geometry, and related fields while reviewing how the pieces should enter Mathlib.

Mathlib is Lean’s community-maintained mathematics library. It gives formalizers shared definitions and previously checked theorems, much as software developers rely on established libraries rather than rebuilding every function.

The library remains only a partial encoding of published mathematics. A human proof can cite decades of literature and assume extensive specialist knowledge. A Lean project must either find each prerequisite in Mathlib or formalize it.

That missing infrastructure explains the size of Anthropic’s output. The company says its 13 million lines are more than five times the size of Mathlib, although it acknowledges that the generated proof is probably much longer than necessary.

Code volume is not a clean measure of mathematical depth. Generated files can contain repeated constructions, verbose proof terms, or artifacts that a human formalizer would replace with a reusable abstraction.

Still, the scale cannot be dismissed as ordinary autocomplete. The system had to connect tens of thousands of verified statements across a dependency graph and carry them into an exact final theorem.

Earlier formalization efforts had completed important subsets. A 2024 project produced a regular-prime proof covering a substantial family of cases using Kummer’s approach. That work also added useful algebraic number theory to Lean.

The full modern proof demands broader infrastructure. It connects a hypothetical solution of Fermat’s equation to a Frey elliptic curve, then combines modularity results with Ribet’s theorem to derive a contradiction.

Each phrase in that summary hides a large formal library. Elliptic curves, modular forms, Galois representations, deformation theory, and analytic estimates all require precise definitions and supporting theorems.

Anthropic’s result suggests that language models can now help manufacture this infrastructure at a much higher rate. That is the real pressure point for mathematics, software verification, and other fields built around formal reasoning.

The change also concerns project management. A single chatbot session would struggle to retain the state of millions of lines and thousands of dependent goals. The successful system externalized that state into Prove2Me.

The platform’s theorem graph gave agents a shared map. Natural-language descriptions made statements searchable, while separate files reduced compilation overhead and resource use.

The accompanying collaboration paper presents this architecture as a way to scale mathematical formalization across human and AI contributors. Anthropic’s experiment offers a prominent stress test of that idea.

This mechanism resembles large software engineering projects. Workers need small tasks, explicit interfaces, a dependency system, shared state, and automated checks. Intelligence alone does not keep the project coherent.

For AI developers, that is a significant lesson. Models become more useful on long tasks when the surrounding system preserves state and narrows each unit of work.

For mathematicians, the result changes the expected cost of formalization. A theorem that once appeared to require years of coordinated labor was encoded by an AI-centered workflow in less than two weeks.

That does not make human work obsolete. It changes where human effort becomes scarce. Selecting representations, designing reusable libraries, interpreting results, and auditing project quality become more important when code generation accelerates.

The Main Contest Is Speed Versus Reusability

The primary opponent is not another AI laboratory, but the human-curated approach to building formal mathematics as durable shared infrastructure.

Anthropic’s artifact optimized for reaching the final theorem. Buzzard’s community project also aims to prove Fermat’s Last Theorem, but it treats the route as a chance to expand Mathlib carefully.

These priorities overlap without being identical. A large generated artifact can prove the target statement while remaining difficult to read, maintain, or reuse.

Anthropic calls its repository a research artifact. It explicitly says the project is not maintained and is not accepting contributions. That signals that the release should not be mistaken for a polished extension of Mathlib.

The distinction resembles production software. A program can pass its tests and still contain duplication, unclear interfaces, or designs that make later changes expensive.

Formal mathematics adds another layer. Lean checks whether declarations are logically valid, but it does not decide whether a definition captures a concept elegantly. It also cannot determine whether an intermediate theorem has the most useful generality.

A human formalizer might spend days choosing an abstraction that supports many future proofs. An autonomous campaign targeting one root theorem can prefer a local construction that closes the current goal faster.

That does not make the local construction wrong. It changes the value produced. One route delivers a checked endpoint, while the other seeks a reviewed mathematical library.

Anthropic says failed early attempts contributed code to the final run. Reusing that work demonstrates flexibility, but it also raises questions about consistency across layers created under different strategies.

The proof’s immense size makes manual line-by-line review unrealistic. Researchers instead need architectural summaries, dependency maps, and independently executable checks.

Anthropic provides a PROOF-PATH.md document connecting mathematical milestones to Lean declarations. That is an important bridge between machine acceptance and human comprehension.

Kevin Buzzard reviewed the artifact and offered unusually strong support. In Anthropic’s announcement, he said the achievement shows that AI autoformalization artifacts are sufficiently reliable to support additional layers of work.

His endorsement matters because he leads the major human collaboration pursuing the same formalization target. It does not mean the two projects now have identical goals.

The community project can still contribute cleaned definitions, smaller proofs, documentation, and reusable components. Anthropic’s result can also help identify which missing areas deserve consolidation.

This creates a plausible division of labor. AI agents can produce a broad formal scaffold, while specialists compress, reorganize, and upstream the useful parts.

Yet cleanup is not automatically cheaper than careful construction. Generated code can impose a review burden if its internal choices are difficult to understand.

The relevant metric is therefore not lines produced per day. Researchers should measure how much verified code survives expert review, enters shared libraries, and reduces effort on future projects.

This matters beyond pure mathematics. Formal methods support compiler correctness, hardware verification, cryptographic protocols, and safety-critical software.

Organizations may soon generate machine-checked artifacts at a scale that overwhelms human reviewers. They will need records that connect claims to specifications, source materials, tests, and approval decisions.

A searchable AI knowledge base can preserve those connections across long projects. It cannot certify a proof, but it can keep evidence and review history accessible.

The strongest outcome would combine both approaches. AI supplies speed and coverage, while a maintained community library supplies intelligibility, reuse, and governance.

Anthropic Claude has shown that the first side can operate at surprising scale. The harder question is how much of its output can become durable mathematical infrastructure.

Lean Checked the Proof, but Trust Still Has Layers

A successful kernel check provides unusually strong evidence of logical validity, but it does not answer every question about process, quality, or interpretation.

Anthropic’s repository includes several defenses against common shortcuts. Its final build rejects proofs that depend on sorry, a Lean mechanism used to leave an unfinished obligation temporarily accepted.

The project also checks that no new axioms were inserted to manufacture the desired result. The final theorem depends on three standard Lean axioms: propositional extensionality, classical choice, and quotient soundness.

A comparator verifies that Anthropic’s theorem statement matches Mathlib’s formulation of Fermat’s Last Theorem. This step addresses a basic specification risk: proving a weaker statement while attaching the famous name.

The repository reports that all 60,475 modules built from source under Lean 4.33.1. Every declaration passed through the Lean kernel.

Anthropic also tested an export with nanoda, an independent Lean kernel written in Rust. The second checker accepted 1,052,234 declarations without errors.

These checks make the mathematical conclusion much stronger than an ordinary company claim. The public artifact can be downloaded, rebuilt, and inspected by independent researchers.

However, a proof assistant guarantees only that the formal statement follows within its logical environment. Trust still includes the kernel implementation, compiler environment, hardware, build process, and correspondence between symbols and intended mathematics.

Using two kernels reduces one part of that risk. It does not eliminate every possible implementation problem, especially because Anthropic applied four performance-related patches to nanoda.

The repository says those patches do not alter typing rules. Independent experts can inspect that claim because the code and patches are public.

The more important limitation concerns meaning. Lean does not care whether a theorem named “Mazur” corresponds to the version mathematicians expect. It checks the exact encoded statement and how that statement supports the final result.

For Fermat’s Last Theorem, the final expression is unusually simple. It states that positive natural numbers cannot satisfy the familiar equation for exponents of at least three.

That simplicity narrows the interpretation gap at the root. The intermediate path remains much harder for humans to understand.

There is also a difference between verifying the proof and verifying Anthropic’s autonomy story. A successful build does not establish which steps Claude chose, how often humans intervened, or how many unsuccessful attempts preceded the published run.

Anthropic says Peng provided only occasional high-level instructions. Examples included prioritizing Jacobians and pushing work on Mazur’s theorem.

Readers cannot derive that operational history from the proof object. It depends on Anthropic’s records and reporting.

The internal model creates another limitation. Outside teams cannot reproduce the exact generation process because the company used a research system that was not publicly available.

They can reproduce the verification outcome. They cannot yet determine how reliably the same setup completes other large formalization projects.

The distinction should shape the headline judgment. It is reasonable to say the proof artifact has strong machine-checkable support. It is too early to infer that Claude can routinely formalize any major mathematical work within days.

A single success can come from a favorable theorem, extensive existing literature, useful prior Lean projects, an effective scaffold, and intensive computation.

Fermat’s Last Theorem also has a well-understood destination. The system was formalizing known mathematics, not deciding whether a proposed new result was significant.

Novel research adds additional uncertainty. A model must find the right question, establish novelty, select useful definitions, and explain why other researchers should care.

Anthropic itself distinguishes this project from its reported work on the Riemann hypothesis. The Fermat result is primarily an advance in verification, not a new mathematical theorem.

That narrower description does not diminish the work. It identifies exactly why the Claude Lean 4 artifact matters and which conclusions the evidence supports.

Anthropic Claude Shifts the AI Math Race Toward Verification

The result pressures AI laboratories to pair mathematical claims with artifacts that independent systems can check.

OpenAI, Google DeepMind, and Anthropic have all used mathematics to demonstrate improvements in reasoning. Competition problems provide convenient scores because graders already know the answers.

Research mathematics presents a more difficult evaluation problem. A fluent proof can contain a hidden gap, misuse a theorem, or quietly change its assumptions.

Human review does not scale easily when models can generate thousands of candidate arguments. Producing ideas becomes cheap while expert attention remains limited.

Formalization changes that balance. A Lean kernel can reject invalid formal steps without becoming tired or persuaded by confident language.

It cannot judge originality or relevance, but it can remove a large class of logical errors before specialists spend time on deeper evaluation.

Anthropic argues that future mathematical papers may routinely include formal proofs alongside human-readable explanations. Its Fermat release makes that prediction more credible.

The idea has historical support. Thomas Hales’s proof of the Kepler conjecture prompted years of review before he led the Flyspeck project, which eventually formalized the result.

That process required a large human effort. If AI can reduce the encoding burden, formal verification becomes practical for a wider range of research.

The competitive pressure is therefore clear. Labs that announce mathematical advances will face stronger demands to release Lean, Rocq, Isabelle, or comparable artifacts.

A natural-language paper may no longer provide sufficient evidence when the same system can also generate a machine-checkable version. Claims without formal artifacts may receive more skepticism.

However, not every field is ready for this shift. Formal libraries remain uneven, and some areas lack the definitions needed to state current research cleanly.

Even when formalization is possible, converting a creative proof into maintainable code can require substantial judgment. Systems may generate enormous local libraries instead of contributing compact general tools.

The compute burden also matters. Six billion output tokens and dozens of collaborating agents represent a major experiment, even without discussing commercial cost.

Anthropic offers a smaller counterexample. It says three consumer subscriptions, coordinated through Prove2Me, formalized Vinogradov’s Three Primes Theorem in three days.

That internal experiment has less public evidence than the Fermat repository. Still, it suggests that the workflow might shrink as models and scaffolds improve.

The industry comparison should focus on complete systems rather than model names. Retrieval, state management, compilation, theorem search, task allocation, and verification all contributed to the outcome.

A model that performs well on isolated Lean problems may fail on a multi-million-line campaign. Another model with better orchestration can succeed despite weaker one-shot scores.

Anthropic Claude therefore raises the bar in two ways. It demonstrates scale, and it exposes enough of the finished artifact for others to challenge the central claim.

Competitors can respond with shorter proofs, stronger automation, cleaner library integration, or prospective evaluations across many projects.

Mathematics will benefit if this competition rewards verifiability instead of dramatic unsupported claims. It will suffer if laboratories flood specialists with huge artifacts that technically compile but remain impossible to navigate.

The next standard should include both machine acceptance and human usability. Formal truth is essential, but research also depends on explanation, abstraction, and shared understanding.

Three Tests Will Show Whether This Changes Mathematics

The Fermat formalization becomes a lasting shift only if outsiders reproduce it, experts reuse it, and the method succeeds beyond one famous target.

The first signal is independent reconstruction. Researchers should clone the public repository, rebuild every module from source, rerun the comparator, and inspect the second-kernel verification.

Successful replications would strengthen confidence that the artifact behaves as documented. Reports of hidden dependencies, impractical resource requirements, or inconsistent builds would weaken that conclusion.

Independent reviewers should also inspect whether the final theorem reaches the expected statement without prohibited escape mechanisms. The repository already supplies checks, but third-party execution is the stronger test.

The second signal is reuse. Mathlib maintainers and formal mathematicians should identify which definitions and intermediate results can enter maintained libraries.

If substantial components become accepted infrastructure, Anthropic’s 13 million lines will have created value beyond one terminal theorem. If almost none survive review, the artifact will look more like a costly certificate.

This test will also clarify the relationship with Imperial College London’s ongoing project. The community effort can compare its abstractions with Anthropic’s route and decide whether the generated work accelerates its roadmap.

A shorter, reorganized proof would not invalidate Claude’s accomplishment. It would show that machine generation and human curation serve complementary roles.

The third signal is prospective performance on new projects. Anthropic should define formalization targets before running its system and report failures alongside successes.

Useful metrics include completion rate, token use, human intervention, build success, reused library code, and expert review time. Without those denominators, one celebrated result cannot establish reliability.

Future targets should vary in mathematical structure. A system that succeeds on one number-theory proof may struggle with topology, probability, category theory, or analysis.

Researchers should also compare known-proof formalization with novel theorem discovery. The latter requires different safeguards because no trusted informal argument exists at the beginning.

These tests matter to more than mathematicians. Developers building long-running agents face the same challenges of state loss, duplicated work, hidden assumptions, and expensive verification.

Anthropic’s strongest idea may be the architecture rather than the theorem. Externalized task graphs, small verifiable units, and independent checks make large agent projects easier to audit.

Knowledge workers should apply the same principle at a smaller scale. Preserve sources, intermediate claims, rejected alternatives, and review decisions instead of trusting a polished final response.

The Claude Fermat proof does not mean AI rediscovered one of mathematics’ most famous results. It means an AI-centered system converted an enormous established argument into a form that two logical kernels accepted.

That is a narrower achievement than “Claude solved Fermat’s Last Theorem,” but it may be more useful. It offers a path for handling the verification burden created by rapidly generated AI research.

The next question is practical: will independent teams turn this artifact into reusable mathematics, or will it remain an extraordinary one-off demonstration? Watch the rebuilds, the Mathlib contributions, and the next prospectively documented campaigns. Those signals will reveal whether anthropic claude changed formal mathematics or simply completed its most visible stress test.