3 ms·
Something still feels off if the formal proof can't be understood. I don't dispute its correctness, but there's a big jump from 4 color theorem, where at least
by daxfohl 1y ago
Something still feels off if the formal proof can't be understood. I don't dispute its correctness, but there's a big jump from 4 color theorem, where at least mathematicians understood the program, to this, where GPT did the whole thing. Like if GPT ceased to exist, nobody would have a clue how to recreate the formalization. Or maybe there's a step in there that's a breakthrough to some other problem, but since it was generated, we'll never notice it.
- dwrensha 1y agoWhere do you see any mention of GPT? The computer-assisted component of the Noperthedron proof is a reasonably small sagemath program that was (as far as I know) written by humans: https://github.com/Jakob256/Rupert https://github.com/Jakob256/Rupert Perhaps you have confused this article with a recent unrelated announcement about a vibe-coded proof of an Erdos conjecture? https://borisalexeev.com/pdf/erdos707.pdf https://borisalexeev.com/pdf/erdos707.pdf
- daxfohl 1y agoOops you're right! I read these both yesterday and they blended together in my memory by the time I made this comment this morning. I knew something felt "off". Tangentially I'll have to reconsider my position on long but lossy context LLMs.