What Is Mathematics? An Elementary Approach to Ideas and Methods, 2nd Edition (1996)

§6. THE FOUR COLOR THEOREM

The four color theorem was proved in June 1976 by Kenneth Appel and Wolfgang Haken. Their proof depends upon showing that some two thousand specific maps behave in a particular rather complicated way. Checking all these cases is immensely tedious, so they used a computer, which required several thousand hours to complete the checks. The proof can now be verified in a few hours, thanks to better theoretical methods and faster computers, but no “pencil and paper” proof has yet been found. Does a simpler proof exist? Nobody knows, although it has been shown that no substantially simpler proof can run along similar lines.

Courant and Robbins’s proof of the Five Color Theorem (p. 264) is an adaptation of work of Arthur Kempe, an attorney and amateur mathematician, who published a purported proof of the Four Color Theorem in 1879. It employs a variant on the method of mathematical induction (pp.9–20), the existence of a so-called “minimal criminal.” The basic idea is that if the Four Color Theorem is false, then there must exist maps that require a fifth color. If such “bad” maps exist, they can be incorporated into bigger maps in all sorts of ways, all of which will need a fifth color too. Since there is no point in making bad maps bigger, we go the opposite way and look at the smallest bad maps, colloquially known as minimal criminals. The existence of a minimal criminal follows from the principle of the smallest integer (p. 18), which is equivalent to the principle of mathematical induction. Minimal criminals are distinguished by the following properties: they need five colors, but any map with a smaller number of countries needs only four. The proof proceeds to exploit these properties to restrict the structure of a minimal criminal, until eventually it is shown that no minimal criminal exists. By contradiction (indirect proof, see p. 86), the theorem must be true.

Kempe’s idea was to take a minimal criminal and produce a smaller, related map. By minimality of the criminal, this smaller map can be four-colored. Then he tried to deduce that the original map can also be four-colored, the required contradiction. Specifically, his idea was to take a minimal criminal and shrink some suitable region down to a point. The resulting map has fewer regions, so it can be four-colored. It may not be possible to restore the shrunken region and find a color for it without changing the colors on the rest of the map, because the region that was shrunk may abut regions that between them already use up all four colors. However, if the region that is shrunk is a triangle (a region meeting only three others), there is no problem. If it is a square, then a cunning technique for swapping colors now called a “Kempe chain” can change one neighbouring color, which does the trick. If it is a pentagon, Kempe claimed, a similar argument works. And he could prove that every map must contain either a triangle, a square, or a pentagon, so there is always a suitable region to shrink and restore.

In 1890 Percy Heawood found a mistake in Kempe’s treatment of pentagonal regions. Heawood did notice that Kempe’s method can be patched up to give a proof that five colors always suffice: one extra color makes the pentagon easier to restore. This is the proof presented on p. 264. On the other hand, nobody could find a map that actually needed five colors.

In 1922 Philip Franklin proved that every map with 26 or fewer regions is four-colorable. His method laid the foundations for the eventual successful assault, with the idea of a reducible configuration. A configuration is just a connected set of regions from the map, together with information on how many regions are adjacent to each around the outside. To see what reducibility means, consider the example of shrinking and restoring a triangular region. Shrink the triangle to a point, and suppose that the resulting map, which has one region fewer, can be 4-coloured. Then so can the original map, because the triangle abuts only three regions, and that leaves a fourth colour spare when it is restored to the map. More generally, a configuration is reducible if the four-colorability of any map that contains it can be proved provided a smaller map is four-colorable. A similar argument proves squares are reducible. Kempe thought that pentagons were reducible, but he was wrong.

Evidently a minimal criminal cannot contain a reducible configuration. So if we show that every minimal criminal must contain a reducible configuration, we have the required contradiction. The most direct way to do this is to find a set of reducible configurations that is unavoidable, in the sense that any map—not just a minimal criminal—must contain a configuration in this set. Kempe effectively tried to do this. He proved, correctly, that the set {triangle, square, pentagon} is unavoidable, but he made an error when proving reducibility of the pentagon. Nevertheless, the basic strategy of his proof—find an unavoidable set of reducible configurations—was a brilliant idea.

In 1950 Heinrich Heesch became the first mathematician to state publicly that he believed the Four Color Theorem could be proved by finding an unavoidable set of reducible configurations. However, he realized that the unavoidable set would have to contain many more configurations than the three in Kempe’s failed attempt, because the pentagon must be replaced by a whole list of alternatives. In fact, Heesch estimated that about 10,000 configurations would be needed, each of moderate size. Further, he devised a method for proving unavoidability, based on a loose electrical analogy. Suppose a quantity of electrical charge is applied to each region, and then allowed to move into neighbouring regions by following various rules. For example, we might insist that the charge on any pentagon is split into equal parts and transferred to any of its neighbors, except triangles, squares, and pentagons. By analysing the general features of charge distributions, it can be shown that certain specific configurations must occur—otherwise charge “leaks away.” More complicated recipes lead to more complicated lists of unavoidable configurations.

In 1970 Wolfgang Haken found improvements to Heesch’s discharging method and started thinking seriously about solving the Four Color Problem. The main difficulty was the likely size of configurations in the unavoidable set. With an estimated 10,000 regions to check for reducibility, the whole computation could easily take a century. And if, at the end, just one configuration in the unavoidable set turned out not to be reducible, then the whole calculation would be worthless.

Between 1972 and 1974, Haken, together with Kenneth Appel, began an interactive dialogue with the computer to try to improve the chances of success. The first run of their computer program produced much useful information. They modified the program to overcome various flaws and tried again. More subtle problems emerged and were duly corrected. After some six months of this dialogue, Appel and Haken became convinced that their method of proving unavoidability had a good chance of success. In 1975 their research program moved from the exploratory phase to the final attack. In January 1976 they began construction of an unavoidable set with some 2000 regions, and by June 1976 the work was complete. Then they tested each configuration in this set for reducibility. Here the computer proved indispensable, duly reporting that every one of the 2000 configurations in Appel and Haken’s unavoidable set is reducible. This contradicts the assumed existence of a minimal criminal, so four colors alone suffice to color any planar map.

To what extent can an argument that relies on an enormous computation, which an unaided human brain cannot possibly check, be considered a proof? Stephen Tymoczko, a philosopher, wrote: “If we accept the four-color theorem as a theorem, then we are committed to changing the sense of ‘theorem,’ or more to the point, to changing the sense of the underlying concept of ‘proof’”. However, few practicing research mathematicians agree. One reason is that there exist mathematical proofs that do not rely on a computer, yet are so long and complicated that even after studying them for a decade, nobody could put his hand on his heart and declare them to be totally unflawed. For example the so-called “classification theorem for finite simple groups” is at least 10,000 pages long, required the efforts of over a hundred people and can be followed only by a highly trained specialist. However, mathematicians are generally convinced that the proof is correct. The reason is that the strategy makes sense, the details hang together, nobody has found a serious error, and the judgment of the people doing the work is at least as trustworthy as that of an outsider. That conviction would of course vanish if anybody—insider or outsider—found a mistake, but so far nobody has.

There is nothing in the Appel-Haken proof that is any less convincing than the classification theorem for finite simple groups. In fact, a computer is much less likely to make an error than a human, provided its program is correct. Appel and Haken’s proof strategy makes good logical sense; their unavoidable set was in any case obtained by hand; and there seems little reason to doubt the accuracy of the program used to check reducibility. Random “spot tests” have found nothing amiss. In a newspaper interview, Haken summed up the consensus view: “Anyone, anywhere along the line, can fill in the details and check them. The fact that a computer can run through more details in a few hours than a human could ever hope to do in a lifetime does not change the basic concept of mathematical proof. What has changed is not the theory but the practice of mathematics.”

Fig. 288. The Mandelbrot set has intricate structure on all scales of magnification.