Skip to content

Fermat's Last Theorem (Anthropic)

anthropics/fermats-last-theorem, by Anthropic, read at commit 6e837e75 (2026-09-24). The repository states that it proves Fermat's Last Theorem in Lean 4 along the route of Frey, Serre, Ribet, Wiles and Taylor-Wiles. This chapter runs no Lean and checks none of it: what it says about the proof is what the repository states. Its formalization.yaml describes the project so:

A complete, machine-checked Lean 4 proof of Fermat's Last Theorem, built on Mathlib: for every natural number n >= 3 there are no positive natural numbers a, b, c with a^n + b^n = c^n (declaration fermat_last_theorem). The default build target also derives Mathlib's own statement FermatLastTheorem. The argument is that of Frey, Serre, Ribet, Wiles and Taylor-Wiles; the named classical inputs (irreducibility of the Frey representation, Langlands-Tunnell, modularity lifting, modularity of semistable curves, level lowering) are proved within the development, in the strength the argument needs, rather than assumed.

Quoted from the project description in formalization.yaml of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0.

Its PROOF-PATH.md, “The route of the proof”, opens:

The argument is that of Frey, Serre, Ribet, Wiles and Taylor-Wiles, largely as in Darmon, Diamond and Taylor, run as a proof by contradiction. A theorem X.y is stated in Theorems/Thm_X_y.lean and proved in P2M/Sol/S_X_y.lean, whose import Theorems.Thm_… lines are exactly the theorems it cites. Where this prose and the Lean differ, the Lean is right. Named classical theorems are proved in the strength the argument needs; the last section says exactly what that is.

Quoted from PROOF-PATH.md of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0.

Portions derive from the Imperial College London FLT project led by Kevin Buzzard, from flt-regular and from Mathlib, all released under the Apache License 2.0; see NOTICE and ATTRIBUTION.md.

Quoted from the acknowledgements in formalization.yaml of anthropics/fermats-last-theorem at commit 6e837e75, Apache-2.0.

The repository's web pages list 29,511 theorems and mark 49 of them as landmarks. This chapter maps the 49 landmarks, one article each, in a part for each of the 6 steps of PROOF-PATH.md, as the web pages place them, and quotes from its other sections; the other 29,462 theorems are counted, not mapped. An article quotes its theorem's Lean statement, from the end of the file's imports and attribute lines to the top-level :=, lists the aliases the web pages give it, and links its line in the repository at the commit above. A theorem a step opens with, when the web pages place it in that step, takes the step's name as its title; any other has its Lean name. The web pages put fermat_last_theorem in a stage before the first step, so it opens part 1.

The repository's citation graph has 106,853 edges: the import Theorems.Thm_… lines of each proof module, which the repository documents as exactly the theorems the proof cites. Under Proof depends on, an article lists the landmarks its proof reaches through theorems that are not landmarks, 76 edges in all.

Where a landmark's name, or another declaration its statement file makes, is also the Lean name of an article in the Imperial FLT chapter, the landmark's article says so and links it. The names are compared as written, so a match says only that the names agree. At this commit none does. The repository's FreyPackage is adapted from the Imperial College London FLT project, as PROOF-PATH.md says, and the Imperial FLT chapter has an article on its FreyPackage.

The repository's README points to its documentation website, https://tianyipeng.github.io/fermats-last-theorem/, which it says has a page for each theorem; each article links its theorem's page there, and the data workflow links them only when the site serves the landmarks' pages.

The web pages also give each theorem an English title and summary, and suggested references. The repository says the English text is generated automatically from the Lean source, with the Lean statement authoritative, and that the references have not been individually verified, so this chapter leaves them out. PROOF-PATH.md, the formalization.yaml and the Lean statements are quoted as written, under the repository's Apache-2.0 license, with the repository and commit named where they are quoted.

The route

Facts

From the repository and its formalization.yaml; the review and automation statements are quoted as written.

  • Repository: anthropics/fermats-last-theorem, read at commit 6e837e75 (2026-09-24).
  • Lean toolchain v4.33.1, Mathlib at db584cd6.
  • License: Apache-2.0.
  • Authors: Anthropic.
  • Review status: “self-assessed”.
  • Review notes: “The proof is machine-checked: by the Lean kernel in a from-scratch build whose default target fails unless fermat_last_theorem depends on exactly propext, Classical.choice and Quot.sound; by leanprover/comparator against the Mathlib-only challenge statement in verification/comparator/Challenge.lean (statement and constants identical, no other axiom, full kernel replay including Mathlib); and by the independent kernel nanoda, which accepted every declaration of the exported environment. See README.md, "How it was verified".”
  • Automation: agent
  • Scope, as its status states: “The full statement of Fermat's Last Theorem for natural-number exponents n >= 3, proved from Lean's three standard axioms with every intermediate result proved in the development or taken from Mathlib; nothing is assumed from the literature.”

Main results

The main results its formalization.yaml lists, with the sorry count and axioms it gives for each, and where the source text declares them.

Literature

The sources its formalization.yaml names, with their relationship to it.

  • Modular elliptic curves and Fermat's Last Theorem, Andrew Wiles, Annals of Mathematics 141 (1995), 443-551 (article; adapts).
  • Ring-theoretic properties of certain Hecke algebras, Richard Taylor, Andrew Wiles, Annals of Mathematics 141 (1995), 553-572 (article; adapts).
  • Fermat's Last Theorem, Henri Darmon, Fred Diamond, Richard Taylor (article; adapts).

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.