Fermat's Last Theorem in Lean 4
A complete, machine-checked proof of Fermat's Last Theorem has been successfully verified using the Lean 4 theorem prover. The project confirms the mathematical validity of the proof using standard axioms and independent kernel verification.
Why it matters
This represents a significant milestone in formal mathematics, demonstrating that complex, long-standing proofs can be fully verified by computer systems to ensure absolute correctness.
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.
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
Get smarter about the news
Sign up free for a feed built around what you actually care about, Dive Deeper research on any story, and the full text of every article.
Create free accountAlready have an account? Sign in