Hacker News Reader

Comment by jameshart | Hacker News Reader

There is no way Fermat could have fit that in the margin. Definitely vindicated.

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

> Given the likely length of the shortest possible proof, I feel like Fermat is 100% vindicated - the proof won’t fit in the margin.

https://xkcd.com/1381/

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.

Yeah Vandiver was on my mind, this is why I said 1920. Wouldnt mind it more complicated, but with simpler concepts and most importantly concepts that feel like they have something to do with FLT (cyclotomic fields, not modular forms).

I read an interesting take that it won’t. Because it won’t be interesting any more. It’s like how no one talks about AI IMO Gold anymore or Stockfish being better than all humans. This kind of mathematics goes back to being a curiosity of humans and machines move to the next frontier.

In a sense, the proof is a demonstrator not an end in itself. To mathematics enthusiasts it is significant. To the AI it is Tuesday.

Enjoyed that idea. Not sure how true but it was enjoyable.

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

And he was right to call it marvelous.

Reply on news.ycombinator.com