Four and More Colors of Mathematics
A memorial to Wolfgang Haken (1928–2022) and more in the AMS Notices
This month’s Notices of the American Mathematical Society for October 2023 has just been mailed to me.
This issue is special in several ways:
- It is large and thick with many pages;
- It has a lot of technical material on decision procedures;
- It has both a feature and a memorial for Wolfgang Haken, who passed away late last year.
Haken is best known for having obtained the first correct proof of the Four-Color Theorem (4CT) with Kenneth Appel, whom we memorialized ten years ago.
The feature, written by Danny Calegari, is on Haken’s solo resolution of another notable problem. Haken proved that whether a closed curve in 3-space is knotted is decidable. One section of the memorial article also covers this.
Four Color Theorem
Many years ago this theorem was a major result of great interest to those of us in computer science theory. Appel and Haken used an approach to the proof that had been tried before. But they needed to use tons of computing power. Their output was in principle hand-checkable but so voluminous—including a supplement on 450 pages of microfiche—as to put the task beyond brute-force human effort.
Beyond easily-corrected typos and redundancies in their initial preprint, there was a hole that took Haken two weeks to fix. This did not, however, presage further issues with the proof. Instead, it exposed a self-correcting mechanism of their approach which they had originally employed in the years before their 1976 announcement to give confidence that loose ends could be quickly closed by local means. We told how Appel’s daughter Laurel was involved in this check-and-patch process; Robin Wilson writing the last section of the memorial says the same of Haken’s daughter Dorothea Blostein—who is a computer scientist at Queens University in Canada.
By the time of Appel and Haken’s book in 1989, almost everyone agreed that all bugs had been either directly squashed or summarily handled. Some streamlined approaches possessing much independence from Haken’s original constructions, most notably a simplification and faster map-coloring algorithm in 1994, led to full acceptance. Ironically, these involved using computers for more facets of the construction and verification. In 2004, Georges Gonthier implemented the whole process in a formal verification system.
All of this made some cool points to those of us in complexity theory. What emerged was not just that computers were useful for generating and checking proofs, but that thinking algorithmically about the problem—including complexity measures for loose ends needing to be handled—led to proof strategies. I and my student Danupon Nanongkai and two other Tech students, Atish Das Sarma and Amita Gajewar, later proved a case of this. It has long been known that the four-color theorem is equivalent to all planar cubic bridgeless graphs being 3-edge-colorable. Call a vertex in a coloring “faulty” if the coloring gives it two edges of the same color.
Theorem 1 If planar cubic bridgeless
-vertex graphs can be 3-edge-colored with at most
faulty vertices then 4CT is true.
I explained how our “amplification” strategy works at the end of a 2009 post, which had lots of comments.
Other Articles
There are a lot of other articles with enticing titles. The feature on Haken by Calegari is not titled for Haken or anything obviously pertaining to him. The title, “Almost Sufficiently Large,” is a riff on a notion of sufficiently large topological manifolds that was coined by Friedhelm Waldhausen but came to be associated with Haken. The “almost” describes a frontier of manifolds that don’t quite meet the condition and open problems they leave. Here are other titles:
- Definability and Arithmetic
- 3-Dimensional Mirror Symmetry
- A Word from Juan C. Meza (former director of the Division of Mathematical Sciences at NSF)
- Data Science and Social Justice in the Mathematics Community
- How to Throw a Math Party for 500 People
- On the Geometry of Metric Spaces
-
Some Applications of
-actions on Affine Varieties
- The Tiling Book
- The Beauty of Roots
- Machine-Human Collaborations Accelerate Math Research
The last one mentions some other famous machine-aided proofs, but not 4CT.
Besides all these, the issue has a long section on early career experiences of mathematics graduates. Here there are a lot more “colors” of feelings and aspirations and dealing with adversity. Just as people have talked about chess becoming “played out” for over a century now, so have we heard the same about mathematics—but this issue attests the opposite.
Open Problems
The meta-open problem about 4CT remains still unsolved. The problem is, can a proof of the four color theorem be found that requires no computer search? Back then we wondered if a proof could be found that needed no search of a huge number of cases. Indeed.
Actually, what is curious about all acknowledged proofs of the Four Colour Theorem (4CT) is that they appeal to the existence, and manual identification, of an ‘unavoidable’ set containing a ‘sufficient’ number of explicitly defined configurations—each evidenced only by a computer as ‘reducible’—such that at least one of the configurations must occur in any chromatically distinguished, putatively minimal, planar map.
For instance:
Neil Robertson et al ‘identified’ 633 configurations as ‘sufficient’ in their 1997, also computer-dependent, proof of 4CT.
However, treating any specific number of ‘reducible’ configurations in an ‘unavoidable’ set as ‘sufficient’ entails a minimum number as ‘necessary and sufficient’.
The presentation [1] and conference paper [2] now show that:
(a) the minimum number of such configurations in a minimal planar map can only be 1; the one corresponding to the ‘unavoidable’ set of the single, ‘reducible’, 4-sided configuration identified by Alfred Kempe in his, seemingly fatally flawed, 1879 ‘proof’ of 4CT.
(b) although Kempe fallaciously concluded that a 5-sided configuration was also in the ‘unavoidable’ set, and appealed to unproven properties of ‘Kempe’ chains in a graphical representation to then argue for its ‘reducibility’, neither flaw in his ‘proof’ is fatal when the argument is expressed geometrically (not graphically);
(c) essentially, Kempe correctly argued that any planar map which admits a chromatic differentiation with a five-sided area C that shares non-zero boundaries with four, all differently coloured, neighbours can be 4-coloured
The argument that the Four Colour Theorem can, indeed, be treated as a mathematical ‘truth’ is addressed in the essay [3].
[1] Why the Perceived Flaw in Kempe’s 1879 Graphical ‘Proof’ of the Four Colour Theorem is Not Fatal When Expressed Geometrically. Presentation on 16th March 2022 to the Prof. P. C. Vaidya National Conference on Mathematical Sciences, 15-16 March 2022, Department of Mathematics, Sardar Patel University, Vallabh Vidyanagar – 388120, Gujarat, India.
https://www.dropbox.com/s/n7eww29476h0rey/
[2] A Geometrical Perspective of The Four Colour Theorem. The National Conference MSUMEC-I on Algebraic Graph Theory, Graph Theory and Analysis, 23–24 February 2023, Department of Mathematics, Manonmaniam Sundaranar University, Tirunelveli, Tamil Nadu, India.
https://www.dropbox.com/s/w59q6gk4esitmez/
[3] There is more to currently accepted, computer-assisted, proofs of the Four Colour Theorem than meets the eye!
https://www.dropbox.com/s/nloxqodpzzy9cm3/
(This is not a joke) There is a non-computer proof that all planar graphs are 9/2-colorable by Cranston and Rabern, from 2018, in the J of Comb Theory, Series B
The paper:
https://www.sciencedirect.com/science/article/pii/S009589561830025X
The version on arxiv:
https://arxiv.org/abs/1410.7233
Slides on the proof:
http://www.people.vcu.edu/~dcranston/slides/planar-fractional-SFU.pdf
My blog post on the proof including an interview with Cranston:
https://blog.computationalcomplexity.org/search?q=4.5
[quote] The problem is, can a proof of the four color theorem be found that requires no computer search? [unquote]
Depends upon how you phrase the question; and to what extent you are committed to seeking only a graphical proof of the Four Colour Theorem (4CT).
For instance, what is curious about all acknowledged proofs of 4CT is that they appeal to the existence, and manual identification, of an ‘unavoidable’ set containing a ‘sufficient’ number of explicitly defined configurations—each evidenced only by a computer as ‘reducible’—such that at least one of the configurations must occur in any chromatically distinguished, putatively minimal, planar map.
Thus:
Neil Robertson et al ‘identified’ 633 configurations as ‘sufficient’ in their 1997, also computer-dependent, proof of 4CT.
However, treating any specific number of ‘reducible’ configurations in an ‘unavoidable’ set as ‘sufficient’ entails a minimum number as ‘necessary and sufficient’.
The presentation [1] and conference paper [2] address precisely this point by arguing that:
(a) the minimum number of such configurations in a minimal planar map can only be the one corresponding to the ‘unavoidable’ set of the single, ‘reducible’, 4-sided configuration identified by Alfred Kempe in his, seemingly fatally flawed, 1879 ‘proof’ of 4CT.
(b) although Kempe fallaciously concluded that a 5-sided configuration was also in the ‘unavoidable’ set, and appealed to unproven properties of ‘Kempe’ chains in a graphical representation to then argue for its ‘reducibility’, neither flaw in his ‘proof’ is fatal when the argument is expressed geometrically (not graphically);
(c) essentially, Kempe correctly argued that any planar map which admits a chromatic differentiation with a five-sided area C that shares non-zero boundaries with four, all differently coloured, neighbours can be 4-coloured
Moreover, the argument that the Four Colour Theorem can, indeed, be treated as a mathematical ‘truth’ is addressed in the essay [3].
[1] Why the Perceived Flaw in Kempe’s 1879 Graphical ‘Proof’ of the Four Colour Theorem is Not Fatal When Expressed Geometrically. Presentation on 16th March 2022 to the Prof. P. C. Vaidya National Conference on Mathematical Sciences, 15-16 March 2022, Department of Mathematics, Sardar Patel University, Vallabh Vidyanagar – 388120, Gujarat, India.
[2] A Geometrical Perspective of The Four Colour Theorem. The National Conference MSUMEC-I on Algebraic Graph Theory, Graph Theory and Analysis, 23–24 February 2023, Department of Mathematics, Manonmaniam Sundaranar University, Tirunelveli, Tamil Nadu, India.
[3] There is more to currently accepted, computer-assisted, proofs of the Four Colour Theorem than meets the eye! Medium essay February 26th 2023.
https://picst.sunbangyan.cn/2024/02/28/b11b51d85cd26ce23854b51c8c3409e8.jpeg
We can know the structure of 5 color map (maximal graph with fewest number of nodes) by analyzing by Kempe Chain, we can know how G8 is growing to match the degrees, but there is no chance to stop growing nodes in this map.