The reason that the four-color theorem remains a fascinating problem for so many people and the source of so many cranks is not that the problem is easy to express.
It's that Kempe's proof, though in the end incorrect, is very elegant and digestible. Seeing why it is incorrect is actually really tricky! And once you have seen why it is incorrect it feels like it is just one or two corrections away from being a correct proof.
If you have not read the outline of Kempe's proof (the wikipedia article does a pretty fair job of it) then you definitely should. I promise you that you will waste at least a little bit of time trying to figure out how to fix the proof in two lines and become a world famous mathematician instantly.
It 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.
The reason that the four-color theorem remains a fascinating problem for so many people and the source of so many cranks is not that the problem is easy to express.
It's that Kempe's proof, though in the end incorrect, is very elegant and digestible. Seeing why it is incorrect is actually really tricky! And once you have seen why it is incorrect it feels like it is just one or two corrections away from being a correct proof.
If you have not read the outline of Kempe's proof (the wikipedia article does a pretty fair job of it) then you definitely should. I promise you that you will waste at least a little bit of time trying to figure out how to fix the proof in two lines and become a world famous mathematician instantly.
> "Georges Gonthier, a computer scientist at Inria in Paris"
somehow the article forgets to mention he was the guy who came up with the first Coq (now Rocq) formal proof of the Four Color Theorem..
It 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.
> 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?
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.