fermats-last-theorem README

The project's README from github.com/anthropics/fermats-last-theorem. As one markdown file: README.md.

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

theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n

and the default build target FinalCheck.lean contains

/-- info: 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms fermat_last_theorem

so the build fails unless the proof rests on exactly Lean's three standard axioms (no sorry, no added axiom, no native_decide). FinalCheck.lean also derives Mathlib's own statement, FermatLastTheorem, from this theorem.

How it was verified

No module contains axiom, sorry, native_decide, unsafe, extern, implemented_by, partial def or #eval (Challenge.lean uses sorry by design and is not part of the package).

Together, these checks establish that the statement above follows from the three axioms, given trust in the Lean kernel (or nanoda) and the checking tools. The statement is written with Lean's built-in natural numbers, +, ≤, < and ≠; its one Mathlib ingredient is ^ on ℕ, which Mathlib defines as Lean's built-in exponentiation, and comparator checks that every definition the statement mentions is identical to stock Mathlib's. Nothing else in Mathlib has to be trusted, because the kernel checks everything beneath the statement. What no tool can check is that each intermediate theorem means what its name suggests; that is for the reader to judge, and PROOF-PATH.md names the Lean theorem behind each step and states exactly how strong each named classical result is as proved here.

Reading the proof in a browser

The html/ folder (about 390 MB) presents this repository as static web pages: the route of the proof step by step; a page for each of the 29,511 theorems (the exact Lean statement, what it cites and what cites it, and an expandable dependency graph) and for each of the 1,450 definition modules (the full source and which statements use it); a search box over all theorem and definition names; the landmark theorems as a graph; and README.md, PROOF-PATH.md and ATTRIBUTION.md rendered with cross-links. The folder is part of this repository, so a clone or a ZIP download already contains it (if you obtained html/ as a separate archive, unpack it at the repository root). Open html/index.html in a web browser; everything works offline, with no web server. The pages were machine-tested in a Chromium-based browser only, and html/README-DOCS.md explains what is quoted from the Lean files and what is generated (the English summaries and suggested references are generated automatically; the Lean statement is authoritative).

Check it yourself

git clone <this repository> 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.

fermats-last-theorem (anthropics/fermats-last-theorem)

Searching Database…

1.3K ·GitHub
Fermats-last-theorem
Что это?Полное, проверенное машиной доказательство Великой теоремы Ферма на Lean 4 поверх Mathlib, идущее по линии Фрея — Серра — Рибета — Уайлса — Тейлора — Уайлса и перепроверенное двумя независимыми ядрами.
Это библиотека, которую можно импортировать, или что-то другое?Это исследовательский артефакт: замороженный репозиторий с доказательством на Lean, который не поддерживается и не принимает вклад; он задуман для проверки и чтения, а не для использования как зависимости.
Как на самом деле читать или проверять доказательство?Склонируйте репозиторий и откройте html/index.html в браузере на Chromium, чтобы офлайн, без сервера, просмотреть все 29 511 теорем и 1 450 определений; чтобы проверить всё самому, пересоберите проект с Lake, а затем запустите скрипты comparator и nanoda.
Что нужно, чтобы собрать и проверить всё самому?Linux или macOS, менеджер тулчейнов elan (он ставит Lean 4.33.1 из lean-toolchain) и сетевое соединение, поскольку Lake компилирует Mathlib из исходников под этот конкретный тулчейн.
Насколько тяжела полная проверка?Очень тяжела: сборка с нуля заняла 5 ч 32 мин на 96 задачах с пиком памяти 153 ГБ, проверка comparator — около 15 часов с пиком 230 ГБ, а понадобится примерно 67 ГБ диска под .lake плюс до 220 ГБ временных C-файлов.
Почему можно верить, что доказательство не тривиальное и не фальшивое?Сборка по умолчанию падает, если финальная теорема опирается не ровно на три стандартные аксиомы Lean (propext, Classical.choice, Quot.sound); в доказательстве нет sorry, добавленных аксиом и native_decide, а независимый инструмент comparator проверяет, что доказанное утверждение совпадает с контрольным файлом только на Mathlib.
Проверялось ли доказательство более чем одним инструментом?Да: помимо обычного ядра Lean, независимое ядро nanoda на Rust перепроверило экспортированную версию всего окружения — 1 052 234 декларации — без единой ошибки.
Кто на самом деле написал код на Lean?Исходники на Lean написали ИИ-агенты, опираясь на написанный людьми open-source-код из проекта FLT Имперского колледжа Лондона, flt-regular и Mathlib, а арбитром выступает сам Lean; код писался для машинной проверки, а не для человеческого чтения.
Что лежит в папке html/?Около 390 МБ статических офлайн-страниц, пошагово раскрывающих путь доказательства: по странице на теорему и модуль определений с графами зависимостей, поисковая строка и отрендеренные версии README.md, PROOF-PATH.md и ATTRIBUTION.md.
What are similar projects?NavierStokesAndEuler, math, integer-mult-bounds, fluid_lean, sympy, Choir, open-ontologies, explainer
Which topics is it in?lean, theorem-proving, verification, science, math, mathematics, academic, computer-science, academic-research, offline, anthropic, documentation
Creator
anthropics
Size
227.1 MB
Stars
1.3K
Updated
CommitSep 24
Age
1mo
Commits · 90 Days