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.
Given the likely length of the shortest possible proof, I feel like Fermat is 100% vindicated - the proof won’t fit in the margin.
My strong hunch is that it was a joke - he knew how difficult the problem was and claiming he had a solution was I think a huge motivating factor for many mathematicians trying to prove it. The greatest nerd snipe troll in history.
Most likely an error. Some time after he wrote that margin note, he wrote a document proving a special case of the FLT (i.e. it's true for n satisfying some property). Why would he do that if he had already proved it?
I think that point actually agrees with GP's take (joking/lying about having had a proof too big to fit in the margin): He would do that because if he thought the problem was extremely difficult but didn't actually have a proof when writing the note he would still want to go on and try to pick away at the problem.
Maybe, we'd have to go back and ask him to be sure. I mostly just didn't want to leave an as of yet certainly unproven vindication about this hanging in a thread about finally having a formalized proof of the star topic :D
It seems unlikely to find 1920 level or so proof although it might be the case that a significantly easier/shorter proof exits via Vandiver conjecture + extra work or Effective Mordell conjecture but it also wouldn't surprise me if that would be even more complicated than the current proof of FLT.
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.
Given the likely length of the shortest possible proof, I feel like Fermat is 100% vindicated - the proof won’t fit in the margin.
My strong hunch is that it was a joke - he knew how difficult the problem was and claiming he had a solution was I think a huge motivating factor for many mathematicians trying to prove it. The greatest nerd snipe troll in history.
Most likely an error. Some time after he wrote that margin note, he wrote a document proving a special case of the FLT (i.e. it's true for n satisfying some property). Why would he do that if he had already proved it?
I think that point actually agrees with GP's take (joking/lying about having had a proof too big to fit in the margin): He would do that because if he thought the problem was extremely difficult but didn't actually have a proof when writing the note he would still want to go on and try to pick away at the problem.
Maybe, we'd have to go back and ask him to be sure. I mostly just didn't want to leave an as of yet certainly unproven vindication about this hanging in a thread about finally having a formalized proof of the star topic :D
I am really interested in whether AI will find a significantly easier (1920 level or so) proof of FLT.
It seems unlikely to find 1920 level or so proof although it might be the case that a significantly easier/shorter proof exits via Vandiver conjecture + extra work or Effective Mordell conjecture but it also wouldn't surprise me if that would be even more complicated than the current proof of FLT.
Maybe we need "de Moura complexity": the shortest Lean proof of a theorem.
And he was right to call it marvelous.