As much as I hate it, I don't think we'll ever get a proof of the four color theorem that isn't enumerating cases.
When you have an integral or the sum of an infinite series that comes out to pi, you know there must be some satisfying explanation involving a circle.
Contrast with "Examples of patterns that eventually fail" on math stackexchange[^1]. When a pattern ends at 906150257, you don't really expect the proof for that to be something beautiful. The reason for the exact value of an upper bound is that it isn't smaller and it isn't bigger.
There's a relationship between e, i, pi, and -1 comes from a deeper relationship between complex numbers and rotation.
The relationship between planar graphs, vertex coloring, and 4 might just be because we put planar graphs and vertex coloring in the same room and 4 popped out, instead of 3 or 5.
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 article mentions at the end the problem of coloring graphs on other surfaces. It's worth noting, it's known, for every surface, what the maximum chromatic number is of a graph on that surface: https://en.wikipedia.org/wiki/Heawood_conjecture
The odd thing about the Ringel-Youngs theorem is that proving the upper bound on the chromatic number is, with the exception of the case of the sphere (i.e., planar graphs, i.e. the four color theorem), not that hard. For the sphere, the lower bound is easy and the upper bound is hard; for other surfaces, the upper bound is easy and the hard part, if any, is the lower bound! (And then also the Klein bottle is an exception and requires only 6 colors instead of 7, so that one also requires a separate more-involved upper bound argument, but nothing on the scale of the four-color theorem...)
I never accepted the proof of the original, because in my view a proof needs to be convincing as well as correct. Not every mathematician has this view, but language-wise I'd prefer to call the original proof a "verification of correctness" rather than a proof. The new proof is similar - more of a formal correctness verification.
What is the point of proof if not to actually convince the reader that the statement is correct? After all, most modern pure math is not terribly relevant to solve practical problems anyway, so if it's not convincing, then what?
I have this same discussion with folks applying formal methods to prove the correctness of software where I work. Often the "proof" is harder to read than the original code and I certainly don't feel anyone has proven anything to me.
this reminds me of a debate about science education - somewhere in elementary school we had to study various proofs that the world was round, mostly with historical context. some people now argue that we don't need this to be part of the curriculum any more - the answer is "we have gone to space and seen it, here are the photos!"
one of the best things about it is not the proof per se, but the fact that mathematicians continue to work on the theorem. bodes well for interesting mathematical research not being killed by AI proofs.
As much as I hate it, I don't think we'll ever get a proof of the four color theorem that isn't enumerating cases.
When you have an integral or the sum of an infinite series that comes out to pi, you know there must be some satisfying explanation involving a circle.
Contrast with "Examples of patterns that eventually fail" on math stackexchange[^1]. When a pattern ends at 906150257, you don't really expect the proof for that to be something beautiful. The reason for the exact value of an upper bound is that it isn't smaller and it isn't bigger.
There's a relationship between e, i, pi, and -1 comes from a deeper relationship between complex numbers and rotation.
The relationship between planar graphs, vertex coloring, and 4 might just be because we put planar graphs and vertex coloring in the same room and 4 popped out, instead of 3 or 5.
[^1]: https://math.stackexchange.com/a/111461
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 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.
if it didn't you would likely be reading about it in far more mainstream press outlets :)
> "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..
The article mentions at the end the problem of coloring graphs on other surfaces. It's worth noting, it's known, for every surface, what the maximum chromatic number is of a graph on that surface: https://en.wikipedia.org/wiki/Heawood_conjecture
The odd thing about the Ringel-Youngs theorem is that proving the upper bound on the chromatic number is, with the exception of the case of the sphere (i.e., planar graphs, i.e. the four color theorem), not that hard. For the sphere, the lower bound is easy and the upper bound is hard; for other surfaces, the upper bound is easy and the hard part, if any, is the lower bound! (And then also the Klein bottle is an exception and requires only 6 colors instead of 7, so that one also requires a separate more-involved upper bound argument, but nothing on the scale of the four-color theorem...)
I never accepted the proof of the original, because in my view a proof needs to be convincing as well as correct. Not every mathematician has this view, but language-wise I'd prefer to call the original proof a "verification of correctness" rather than a proof. The new proof is similar - more of a formal correctness verification.
What is the point of proof if not to actually convince the reader that the statement is correct? After all, most modern pure math is not terribly relevant to solve practical problems anyway, so if it's not convincing, then what?
I have this same discussion with folks applying formal methods to prove the correctness of software where I work. Often the "proof" is harder to read than the original code and I certainly don't feel anyone has proven anything to me.
this reminds me of a debate about science education - somewhere in elementary school we had to study various proofs that the world was round, mostly with historical context. some people now argue that we don't need this to be part of the curriculum any more - the answer is "we have gone to space and seen it, here are the photos!"
one of the best things about it is not the proof per se, but the fact that mathematicians continue to work on the theorem. bodes well for interesting mathematical research not being killed by AI proofs.