Four-Color Theorem

The four-color theorem states that any map in a plane can be colored using four colors in such a way that regions sharing a common boundary (other than a single point) do not share the same color. This problem is sometimes also called Guthrie's problem after F. Guthrie, who first conjectured the theorem in 1852. The conjecture was then communicated to de Morgan and thence into the general community. In 1878, Cayley wrote the first paper on the conjecture.

The cyclic coloring conjecture is a related extension of the four-color theorem for planar embeddings.

Fallacious proofs were given independently by Kempe (1879) and Tait (1880). Kempe's proof was accepted for a decade until Heawood showed an error using a map with 25 regions, published as Fig. 18 (although a map with nine regions suffices to show the fallacy). This map is discussed in the Heawood four-color map entry. The Heawood conjecture provided a very general assertion for map coloring, showing that in a genus 0 space (including the sphere or plane), four colors suffice. Ringel and Youngs (1968) proved that for genus , the upper bound provided by the Heawood conjecture also gives the necessary number of colors, with the exception of the Klein bottle (for which the Heawood formula gives seven, but the correct bound is six).

Six colors can be proven to suffice for the case, and this number can easily be reduced to five, but reducing the number of colors all the way to four proved very difficult. Appel and Haken (1977) constructed the first computer-assisted proof that four colors were sufficient. Its exhaustive computer analysis of many discrete cases initially made independent verification difficult. A shorter, independent proof was constructed by Robertson et al. (1996a), with an overview by Thomas (1998).

In December 2004, G. Gonthier of Microsoft Research in Cambridge, England (working with B. Werner of INRIA in France) announced a formal verification of the Robertson et al. proof by formulating the problem in the equational logic program Coq and confirming the validity of each of its steps, removing the remaining doubts about the logical correctness of the computer-assisted proof (Devlin 2005, Knight 2005).

Inoue et al. (2026) gave an algorithm for four-coloring an -vertex planar graph, improving the previous bound of Robertson et al. (1996b). They showed that every planar graph embedding of a triangulated graph contains either linearly many pairwise non-touching reducible configurations or linearly many pairwise non-crossing obstructing cycles of length at most five. These configurations and cycles permit reductions to smaller coloring problems, allowing the algorithm to reduce the problem size by a constant factor at each recursive step.

J. Ferro (pers. comm., Nov. 8, 2005) has debunked a number of purported "short" proofs of the four-color theorem.

Martin Gardner (1975) played an April Fool's joke by asserting that the McGregor map consisting of 110 regions required five colors and constitutes a counterexample to the four-color theorem. Wagon (2002) used the Kempe's coloring algorithm to color all its regions with four colors, without needing random color interchanges.