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