[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.

[prerok]

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.

[thiht]

The proof is pretty trivial anyway so it’s left as an exercise to the reader

[throw46395]

    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