Ian Stewart - Concepts of Modern Mathematics

In Chapter 11 we had a four-colour problem and a five-colour theorem. On 22 July 1972 two mathematicians at the University of Illinois, Kenneth Appel and Wolfgang Haken, announced a proof that every map on the plane can be coloured with four colours, resolving the long-standing question. The snag with their proof is that it involves an immense amount of computing time - they used about 1200 hours, but a check might be performed in 300 on a big machine - and a single error might destroy the proof completely. Contrary to popular opinion, computers do make errors even when their programmers do not. The problems raised by this are as much philosophical as technical (is a proof checked by a human any more likely to be accurate than one checked by computer?) and look like causing some problems in future. At the present moment, the AppelHaken proof has not been fully checked by an independent program, although those parts that have been checked appear to be error-free. Philosophy apart, most mathematicians would probably agree that the theorem is proved provided such a check is carried out in full. The philosophical problem is an interesting one, however, because it involves the difference between a logical proof and a satisfactory one. I shall return to this once weve seen how it goes.

The proof of the five-colour theorem given in Chapter 11 is essentially due to A. B. Kempe (1879). Let us recall it briefly. It makes use of a reduction process (which involves a number of different cases) to show that the given map may be coloured provided another map, with fewer regions, can be coloured. By applying this process over and over again we must, since the number of regions decreases at each stage, eventually reach a map with as many or fewer regions than we have colours. This map is manifestly colourable, therefore reversing the reduction step by step, so was the previous one, and the one before that, and... the original.

Kempe went further than we have done (arguing for five colours): he added an argument purporting to prove that four would suffice (involving extra cases in the reduction). The mathematicians of the time seem to have accepted this proof without a qualm, until in 1890 P. J. Heawood pointed out the mistake. The proof we have given above, as Heawood also pointed out, remains valid for five -colourability.

The basic strategy of our proof for five colours and the Appel-Haken proof and even Kempes fallacious attempt - is the same. (Kempe simply failed to carry it out correctly.) For our present purposes this emerges more clearly if we recast our proof in a slightly different form. The idea is to argue by contradiction and suppose that there does exist a map requiring more than five colours. There is then such a map having the least possible number of regions (in trade jargon, a minimal criminal ), say M. By definition, every map with fewer regions than M can be coloured in five colours.

Next we show that M must contain at least one of a list of configurations, namely . Then we consider one of these configurations and concoct an argument of the following kind. From any map M which contains it, we show how to derive another map M with fewer regions. This M is so constructed that, if it is five-colourable, so is M. Thus the burden of colourability shifts from M to the simpler map M. (In our proof on pages 169-73, M is obtained from M by merging regions, as indicated.) We concoct such arguments (which may differ in detail) for each configuration in our list.