-- No three positive integers a, b, c satisfy aⁿ + bⁿ = cⁿ for n > 2. -- (Proved by Andrew Wiles 1995 — formalize it in Lean 4!) theorem fermat_last (a b c n : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hn : 2 < n) : a ^ n + b ^ n ≠ c ^ n :=