Four and More Colors of Mathematics

Gödel’s Lost Letter and P=NP 2023-09-18

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 ${n}$ -vertex graphs can be 3-edge-colored with at most ${o(n)}$ 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.

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.

Four and More Colors of Mathematics

Gödel’s Lost Letter and P=NP 2023-09-18

Four Color Theorem

Other Articles

Open Problems