This theorem was conjectured in 1853 by Francis Guthrie. It is obvious that three colors are completely inadequate, and it is not difficult to prove that five colors are sufficient to color a map. However, it was not until 1977 that the conjecture was finally proven by Kenneth Appel and Wolfgang Haken. They were assisted in some algorithmic work by J. Koch.

The proof reduced the infinitude of possible maps to 1,936 configurations (later reduced to 1,476) which had to be checked one by one by computer. The work was independently double checked with different programs and computers. In 1996, Neil Robertson, Daniel Sanders, Paul Seymour and Robin Thomas produced a similar proof which required checking 633 special cases. This new proof also contains parts which require the use of a computer and are impractical for humans to check alone.

The four color theorem was the first major theorem to be proven using a computer, and the proof was not accepted by all mathematicians because it could not directly be verified by a human. Ultimately, one had to have faith in the correctness of the compiler and hardware executing the program used for the proof. See experimental mathematics.

The lack of mathematical elegance was another factor; to paraphrase comments of the time "a good mathematical proof is like a poem -- this is a telephone directory!"

Table of contents |

2 Generalizations 3 Real world counter examples |

To formally state the theorem, it is easiest to rephrase it in graph theory. It then states that the vertices of every planar graph can be colored with at most four colors so that no two adjacent vertices receive the same color. Or "every planar graph is four-colorable" for short. Here, every region of the map is replaced by a vertex of the graph, and two vertices are connected by an edge if and only if the two regions share a border segment.

One can also consider the coloring problem on surfaces other than the plane. The problem on the sphere is equivalent to that on the plane. For closed (orientable or non-orientable) surfaces with positive genus, the maximum number *p* of colors needed depends on the surface's Euler characteristic χ according to the formula

----------- | | | | D | C | --| ---- | | | | | | | --| A | | ----| | ---- | | | | B | | | A | ------ ---- ----| E | ------------where the two regions labeled 'A' belong to the same country. Five colors are required if those two regions are to receive the same color. Similarly, one can construct maps that require an arbitrary high number of colors.

- Appel, K. and Haken, W.,
*Every Planar Map is Four-Colorable.*Providence, RI: American Mathematical Society, 1989 - O'Connor and Robertson,
*History of the Four Color Theorem*, MacTutor project, http://www-groups.dcs.st-and.ac.uk/~history/HistTopics/The_four_colour_theorem.html - Saaty and Kainen,
*The Four Color Problem: Assaults and Conquest*(ISBN 0-486-65092-8) - Robin Thomas, An Update on the Four-Color Theorem,
*Notices of the American Mathematical Society*, Volume 45, number 7 (August 1998)