Fermat's Last Theorem in Lean 4