The Four Color Theorem, or, I Am An Old Geezer

I was introduced to the Four Color Theorem when I was in college. The theorem dates back to 1852, when Francis Guthrie was coloring a map of the counties of England. He noticed that he needed only four colors to fill in the map, so that no two adjacent counties had the same color. Guthrie, who later became a mathematician and botanist (a curious combination) in South Africa, communicated this observation to his professor, the mathematician Augustus De Morgan, and asked whether this was true in general. In other words, given any map containing bounded regions (counties, states, etc.), can we color all these regions with only four colors, and avoid having any two adjacent regions with the same color?

This may seem a trivial, possibly silly, theorem, but its eventual “proof”, in 1976, has divided the math world into two groups: the Young Turks, and the Old Geezers. It turns out that, in 1976, at the tender age of 24, I was an Old Geezer.

The theorem was extremely difficult to prove. By 1890 we had proof that five colors would be sufficient, but the proof that four colors would be sufficient seemed elusive. One proof was published in 1879, and another in 1880, but both were eventually shown to be incorrect. Curiously, it took 11 years in each case to show that the proofs had defects.

In June of 1976, Kenneth Appel and Wolfgang Haken at the University of Illinois announced that they had proven the theorem. Their proof was controversial: for the first time, a computer had played a central role in proving a theorem.

I will not go into the details of the proof other than to say that they used the counter-example method. Let’s say that I want to prove that not all states in the United States are south of Canada. I start by assuming the opposite, that all states are south of Canada, then look for one example (a counter-example) where this is not true (Alaska). Once I have proven the opposite to be false, the original must be true.

The counter-example that Appel and Haken sought was a map where the minimum number of colors required was five. When they showed that this counter-example didn’t exist, the original theorem, that a minimum of four would suffice, was proven. This involved two mathematical properties of maps: reducibility, and unavoidability. In searching for the counter-example, the two mathematicians reduced the number of maps that had to be examined from an infinite number to just 1,476. (This is the reducibility part of the proof.) These maps were checked by computer. The computers of the day were not as fast as today’s versions, so it took more than a thousand hours of computer time to check the maps. The unavoidability part of the proof was performed by hand, actually by Haken’s daughter, and involved the examination of 400 pages of microfiche.

This is the part that rubbed mathematicians the wrong way. I can prove that vertical angles are congruent on a 3 x 5 index card. I can prove the theorem of Pythagoras on a half-sheet of notebook paper. There are other proofs that are far longer and more involved, but I can get through them with a reasonable amount of work. The Appel-Haken proof, on the other hand, is beyond my ability to follow. I can check the math that reduces the number of maps from infinity to 1,476, but the checking of the maps by the computer is something I can’t do. What if there is a flaw in the computer program? How do we know that there is no flaw? And the mind-numbing examination of 400 pages of microfiche requires a determination that few of my fellow amateur mathematicians possess.

There was, in fact, a flaw in the proof, discovered by a masters student in 1981. It was in the unavoidability portion of the proof, the 400 pages of microfiche. Appel and Haken corrected the error, and found that the proof still held. The final word on their work is their book, published in 1989, that corrects the error discovered in 1981, and includes the 400 pages of microfiche. It has the gripping title Every Planar Map Is Four Colorable, and can be purchased here for a mere $121.03, at the time of this writing. That is one expensive paperback.

But the use of a computer to do work that is unreasonable for a human to do still sticks in the craw. The year 1976 was a watershed year in mathematics, separating mathematicians into two groups: those of us, the Old Geezers, who object to the use of an algorithm that, in itself, can’t be proven to be accurate; and the Young Turks, who buy the proof based primarily on the fact that no flaw in the algorithm has yet come to light. It is an unsatisfactory situation.

Mathematicians have continued working on the proof of the four color theorem. The number of reducible configurations has been lowered from 1,476 to 633, but, as before, the checking must be done by computer. Another group of mathematicians has found a way to avoid having to trust the various algorithms that have been used to examine the reducible configurations. They did this by using Coq, a computerized theorem proving program. We are down to trusting one program only.

My view is that the four color theorem is very likely true. It is also my view that we do not yet have definitive proof that it is true. I remain an Old Geezer.