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 6 days ago | parent | next [-]

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 5 days ago \| parent [-]
		The proof is pretty trivial anyway so it’s left as an exercise to the reader

▲ throw46395 6 days ago | parent | prev [-]

    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