Mechanised theorem proving: exponents 3 and 4 of Fermat's last theorem using Isabelle
Roelof Oosterhuis · 2007
This thesis describes a formalisation of a proof of the cases n = 3 and 4 of Fermat’s last theorem (FLT), using the proof assistant Isabelle. The formalisation of the general FLT, stating that for all natural numbers n > 2 and all integers x, y, z we have.