The Four-Color Theorem 1852–1976(ams.org)
ams.org
The Four-Color Theorem 1852–1976
https://www.ams.org/journals/notices/202603/noti3305/noti3305.html
6 comments
Agree 100% -- wonderful history here. And with such a simple statement, hard to believe / accept the "reason" is that it works for 633 limiting cases.
As somebody noticed, we're very lucky to live in a universe where many key things are utterly simple (like basic arithemetics), or allow for acceptable simple approximations (like classical mechanics). There was a sci-fi story set in a world orbiting a binary star, where discovering the laws of celestial mechanics feels like an intractable problem, and even predicting seasons is barely possible.
Professor Appel was my boss when I was a system administrator for the UIUC Math department, working my way through grad school. He was one of the best bosses I’ve had over the past thirty years and had a real knack for dealing with the immature twenty something’s (like me).
He was incredibly humble about the 4 color proof, and well, just about everything. He continued to learn new things — I remember him asking me to help him debug some PostScript and I couldn’t believe it was happening.
He was incredibly humble about the 4 color proof, and well, just about everything. He continued to learn new things — I remember him asking me to help him debug some PostScript and I couldn’t believe it was happening.
A proof of this theorem was also formalized in the Rocq proof assistant (called Coq back then). See here for more: https://inria.hal.science/hal-04034866/document
Referenced at the very end; I came here to mention the sheer size of this effort. 60,000 lines is incredible. I can barely review 1,000 lines of Python without wanting to become a manual laborer instead.
> Ten years later their approach was fully machine-checked by the French computer scientist Georges Gonthier who verified 60,000 lines of formal language proof before declaring that their proof was indeed correct
> Ten years later their approach was fully machine-checked by the French computer scientist Georges Gonthier who verified 60,000 lines of formal language proof before declaring that their proof was indeed correct
Deep down, I'm still hoping someone or something will find a beautiful proof that is more elegant than brute-force counting and verifying that four colors suffice for all unavoidable configurations that reduce to all other possible configurations. According to the article, there are 633 of those configurations. No idea if a more elegant proof is possible, but I hope it is.