Fermat's Last Theorem Proved in Lean 4: Sept 4, 2026

Read the HTML overview from GitHub - rendered via https://htmlpreview.github.io. 

Overview · FLT in Lean 4

A rival attempt to achieve the same outcome has ended in admitted defeat.

Almost 30K theorems were traversed on the path to the proof. The theorem statement is as follows:

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

GitHub only shows raw HTML source (it does not render these in case of XSS and malicious scripts). HTML is always displayed as raw text.