| ▲ | m_w_ 3 hours ago |
| > Along the way, it wrote 13 million lines of Lean and proved 29,500 intermediate theorems. Pretty insane. I suppose it lends further credence to the idea that anything that can be shown to be correct can be done by a model. |
|
| ▲ | kccqzy an hour ago | parent | next [-] |
| The next step, if Anthropic is interested, is definitely performing refactoring to cut down on the size of the proof. It’s clear to everyone including Anthropic that this proof isn’t as concise as it could have been. When it’s concise enough to be accepted into Mathlib is when victory truly is upon us. |
|
| ▲ | jameshart 3 hours ago | parent | prev | next [-] |
| There is no way Fermat could have fit that in the margin. Definitely vindicated. |
| |
| ▲ | zamadatix an hour ago | parent | next [-] | | 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. | | |
| ▲ | vlovich123 an hour ago | parent [-] | | 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. | | |
| ▲ | BeetleB an hour ago | parent | next [-] | | 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? | | |
| ▲ | zamadatix an hour ago | parent [-] | | 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. |
| |
| ▲ | zamadatix an hour ago | parent | prev [-] | | 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 |
|
| |
| ▲ | bananaflag 2 hours ago | parent | prev [-] | | I am really interested in whether AI will find a significantly easier (1920 level or so) proof of FLT. |
|
|
| ▲ | skobes 14 minutes ago | parent | prev | next [-] |
| Maybe I'm misunderstanding something about how all this works, but can we have any confidence that 13 million lines of AI-generated Lean code are... correct? How have we not merely substituted one verification problem for another? |
|
| ▲ | andriy_koval 2 hours ago | parent | prev [-] |
| especially compared to existing 129 pages proof by human |
| |
| ▲ | black_knight 37 minutes ago | parent | next [-] | | A human can cite previous published results. I am sure a lot of this development was formalising the prerequisites. | | |
| ▲ | andriy_koval 30 minutes ago | parent [-] | | > I am sure a lot of this development was formalising the prerequisites How can you be so sure its not result of inefficiency? | | |
| ▲ | black_knight 24 minutes ago | parent [-] | | Oh, I am quite sure there are inefficiencies! Just that they are not entirely inefficiencies. I have used Fable for formalisation and it will, unless I catch it, reprove results it previously had proven, inline, in other results. |
|
| |
| ▲ | dist-epoch 2 hours ago | parent | prev [-] | | Insert meme with 200 pages needed to prove 1+1=2 rigurously | | |
|
