Abstract
A major event in 1976 was the announcement that the Four Color Conjecture (4CC) had at long last become the Four Color Theorem (4CT). The proof by W. Haken, K. Appel, and J. Koch is published in the Illinois Journal of Mathematics, and their twoβpart article outlines the nature and reliability of the solution. The first section is a readable and informative historical survey. The reminder will appeal chiefly to specialists in graph theory. Although the logic of attack is relatively simple, the need to examine an immense number of individual cases is frustrating. Hopefully this first breakthrough will pave the way for a short elegant proof. For the second section, 1200 hours of computer time was required to verify the 4βcolor reducibility of nearly 1900 configurations. At this time there is no good way to condense the proof. In this digest we offer an exposition of the main ideas. The first and the last parts are intended for a general audience, but the intermediate sections assume more knowledge of graph theory proper. The usual statement of the 4CC goes as follows: βAll maps on the sphere or plane can be colored with four colors so that neighboring regions are never colored alike.β The form in which the 4CT was proved is βThere exists an unavoidable set of reducible configurations, relative to triangulations of the plane.β The initial part of our task is to explain how the 4CC comes to be expressed in such jargon. The next step is to show how one finds simple finite sets of unavoidable configurations. Then comes the question of how to prove reducibility, followed by a consideration of the known obstacles to reduction. Our concluding remarks and criticisms include a consideration of prospects for the future.