anthropics/fermats-last-theorem
★ 1,284 stars
Lean
Covered in week 2026-W41 · the 2026-10 report
anthropics/fermats-last-theorem — 1,284 stars · Lean: what it does and why developers starred it, in a 30-second video review from 09 Oct 2026.
What fermats-last-theorem is
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).
From the repository README · read it on GitHub →