Comment by mdiesel
He probably did know it, it's remarkably simple. I can't remember how to format maths in a HN comment though to put it here.
He probably did know it, it's remarkably simple. I can't remember how to format maths in a HN comment though to put it here.
import FLT
theorem PNat.pow_add_pow_ne_pow
(x y z : ℕ+)
(n : ℕ) (hn : n > 2) :
x^n + y^n ≠ z^n := PNat.pow_add_pow_ne_pow_of_FermatLastTheorem FLT.Wiles_Taylor_Wiles x y z n hn
Yeah, I just figured out how to simply reconcile general relativity and quantum mechanics, but I am writing on my phone and it's too tedius to write here.