alt Hacker NewsIt better not have 100s of individually checked configurations
Edit: damn it.
I was just thinking last night about the four color theorem in the context of the recent Navier-Stokes drama, and Tao's Mastodon post on the uselessness of inscrutable computer-generated formalizations. I would love for an AI company find a proof of the four-color theorem without individually checked configurations, and optimize it for human comprehensibility.
Replies
gowld • today at 6:20 PM
I would love to have a unicorn pegasus, but some things might just be impossible.
Even something as simple as the computer you are posting from is not optimized for human comprehensibilty, in its full detail.
> The proof — ... — is in some ways even more complicated than its predecessors.
Damn it in deed.
But perhaps it will open a door to new proofs? Perhaps in other areas?