While pretty much everyone is certain Fermat was mistaken in believing he had a valid proof for the theorem, this is an expanded (compared to proof presentations) version of one proof - not the shortest presentation of the shortest valid proof.

I am really interested in whether AI will find a significantly easier (1920 level or so) proof of FLT.

Maybe we need "de Moura complexity": the shortest Lean proof of a theorem.

And he was right to call it marvelous.