Fermat’s Last Theorem for Exponent 3

This website serves as the blueprint for the project aimed at formalising Fermat’s Last Theorem for the exponent 3 using the Lean 4 proof assistant (FLT3). It offers comprehensive coverage of all necessary definitions, theorems, and proofs, presented in natural, informal language to facilitate understanding and implementation. The related code is being integrated into the Lean library of formalised mathematics (Mathlib) and imported as a dependency in the broader formalisation project of Fermat’s Last Theorem led by Kevin Buzzard and Richard Taylor (FLT).