Claude formalises Fermat’s Last Theorem, but it did not discover the proof

Anthropic says a team of Claude agents has completed a computer-checked formalisation of Fermat’s Last Theorem in Lean after 11 days of work. The theorem itself was proved by Andrew Wiles and Richard Taylor in the 1990s. The new result concerns the conversion of that mathematics into code that a proof assistant can check.[1][3]

What we know

Anthropic reports that Claude produced about 13 million lines of Lean and 29,500 intermediate theorems used in the final proof.[1] The public repository contains a Lean 4 formalisation based on the argument of Frey, Serre, Ribet, Wiles and Taylor-Wiles.[2] The repository’s browser documentation separately lists 29,511 theorem statements in the final dependency tree.[2] The repository reports a full build with Lean 4.33.1 and Mathlib v4.33.0, a comparison against Mathlib’s statement, and a second check using nanoda, an independent Lean kernel written in Rust.[2] The project used Prove2Me, a platform that organises theorem dependencies and lets multiple agents work on separate parts of a formalisation.[1][5]

What we don’t know

The final code can be checked by Lean, but that does not independently establish Anthropic’s account of how much human work was involved in the 11-day period, how the agents were directed, or how much existing code and infrastructure they reused.[1][2] The available sources also do not amount to a full independent audit of the repository. Nature reports the result and quotes mathematicians, but its article is journalism about the project rather than a reproducibility study.[3]

Why it matters

The result shows a practical division of labour between language models and proof assistants. Claude generated and repaired formal proof code; Lean checked whether the resulting terms followed the rules of the formal system.[1][2] Formal checking does not remove the need for mathematical judgement, because researchers still need to confirm that the encoded statement and definitions mean what they intend.[2]

Three-panel diagram showing an existing Fermat proof moving through Lean formalisation to machine checking, with a note that formalisation is not discovery — A simplified evidence map of the reported workflow. The machine checks concern the Lean artefact, not the autonomy of the AI system.

From a known proof to a checked artefact

Fermat’s Last Theorem states that no positive integers a, b and c satisfy aⁿ + bⁿ = cⁿ when n is greater than 2. For n equal to 2, Pythagorean triples provide counterexamples to the corresponding statement, including the familiar 3, 4, 5 triple.[3][6]

The modern proof is far removed from that short equation. It uses advanced number theory involving elliptic curves, modular forms and Galois representations.[4][7] The central R=T strategy relates a deformation ring to a Hecke algebra.[7]

Claude did not discover this mathematical route. The repository identifies the formalisation as following a version of the Wiles, Darmon, Diamond and Taylor argument, and credits earlier community projects and Mathlib.[1][2]

The difficult engineering task was to express the argument in Lean. Informal mathematical writing omits many steps that are obvious to a trained reader. Lean requires those steps to be represented in a form its kernel can check. A large project therefore becomes a dependency graph of definitions, lemmas and theorems rather than a single conversation with a chatbot.[1][5]

What the verification establishes

The repository says that the default build checks the theorem with Lean’s standard axioms and that it contains no added axiom, sorry, native_decide or unsafe declaration.[2] It also says that the theorem was checked against Mathlib’s own formulation and replayed through a second kernel.[2]

Taken together, those reported checks support a narrow conclusion: the published Lean artefact is reported to prove the stated Lean theorem under the assumptions of the Lean kernel and its checking tools. That is stronger than a plausible AI-generated explanation, but narrower than the claim that an AI independently created the underlying mathematics.[2]

The repository is also explicit about the cost of reproducing the checks. It reports roughly 67 GB of disk for the build, very high memory requirements, and additional time and memory for the comparator and second-kernel checks.[2] Those requirements matter because an open repository is not automatically an independently reproduced result. Reproduction requires the specified toolchain, hardware and commands[2].

The remaining boundary

The most defensible description is that Claude helped formalise an existing proof and produced an artefact that the project says has passed several machine checks. It is not that Claude has independently solved Fermat’s problem from first principles.

The next test is whether mathematicians outside Anthropic can build the repository and inspect the dependency chain. The repository describes itself as a research artefact that is not maintained and does not accept contributions, so its immediate value is better described as an open, machine-checkable representation than as a maintained library.[2] External reproduction would give the reported checks a stronger independent basis.

Claude formalises Fermat’s Last Theorem, but it did not discover the proof

From a known proof to a checked artefact

What the verification establishes

The remaining boundary

Sources

Share:

Leave a comment Cancel reply