anthropics/fermats-last-theorem

anthropics/fermats-last-theorem

Language: Lean

License: Apache-2.0

Stars: 461

Forks: 30

Open issues: 1

Created: 2026-09-04T14:21:04Z

Pushed: 2026-09-04T14:59:12Z

Default branch: main

Fork: no

Archived: no

README:

Fermat's Last Theorem in Lean 4

A complete, machine-checked proof of Fermat's Last Theorem in Lean 4, built on Mathlib (Lean 4.33.1; Mathlib v4.33.0, pinned by commit in lakefile.lean). The argument is that of Frey, Serre, Ribet, Wiles and Taylor-Wiles. PROOF-PATH.md names each step and the Lean theorem that carries it, and the html/ folder presents the whole proof as web pages you can browse offline (see "Reading the proof in a browser" below).

Research artifact. Not maintained and not accepting contributions.

The statement

Theorems/Thm_fermat_last_theorem.lean declares

~~~lean theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 flt && cd flt LEAN_NUM_THREADS=96 lake build # one job per hardware thread by default; lower it to bound memory (about 5 GB per job) verification/comparator/run.sh # verdict: last line of .verify-work/wrapper/comparator.log verification/nanoda/run.sh # after the comparator script; verdict: .verify-work/nanoda/run-*/nanoda.stdout ~~~

Lean prints a large number of deprecation and style-linter warnings while building. They do not affect the result. The build has succeeded when its output ends with 'flt_mathlib' depends on axioms: [propext, Classical.choice, Quot.sound] and Build completed successfully. Each script fetches and builds its checker at a pinned version and exits 0 on success.

About the sources

FinalCheck.lean is the default target; Theorems/ holds the statements, P2M/Sol/ the proofs (each importing the statements it cites), Definitions/ the definitions, verification/ the two checks, html/ the web pages described above and tools/docs-site/ the program that generated them. The Lean sources were produced by AI agents building on human-written open-source Lean, with Lean as the arbiter, and are written to be checked rather than read: names are machine-generated, labels such as P2M or hexadecimal suffixes are pipeline labels rather than mathematics, and where a name and a statement disagree the statement is what was proved. Comments were removed, apart from upstream notices, doc strings and citations (listed in ATTRIBUTION.md) and the expected-output comment that #guard_msgs checks.

Licence and attribution

Copyright 2026 Anthropic, PBC; released under the Apache License 2.0 (LICENSE). Portions derive from three Apache-2.0 projects credited in NOTICE: the Imperial College London FLT project led by Kevin Buzzard (Frey package, Galois representations, deformation theory, patching and more), flt-regular (Kummer's theorem) and Mathlib. ATTRIBUTION.md lists the 106 files containing material from the first two, with upstream file, copyright holder and authors, and the 23 files that reproduce Mathlib text (the excerpts in Definitions/Def_Compat_Mathlib430.lean and twenty-two modules that re-prove a Mathlib lemma in place). The web pages bundle KaTeX and Graphviz (compiled to WebAssembly) under their own licences, listed in html/assets/vendor/LICENSES.txt. Lean and the packages in lake-manifest.json are fetched at build time, not distributed here. If you recognise unattributed material, the omission is unintentional.