Four color theorem

The four color theorem states that every possible geographical map can be colored with at most four colors in such a way that no two regions sharing a border segment (not just a point) receive the same color.

This theorem was conjectured in 1853 by Francis Guthrie. It is obvious that three colours are completely inadequate, and mathematicians were able to prove that five colors weere sufficient to color a map. However, it was not until 1977 that the conjecture was finally proven by Ken Appel and Wolfgang Haken. The proof reduced the infinitude of possible maps to 1936 configurations (later reduced to 1476 configurations) 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 came up with a new proof of the four color theorem. The trio had begun by trying to verify the Haken-Appel proof but gave up on doing so. They chose instead to come up with their own proof, using a slightly more efficient variant of Appel and Haken's ideas. Instead of having to check the 1,476 graphs which Haken and Appel needed to, they managed to reduce the number required for their proof to just 633 special cases and used these. This new proof also does contain parts which require the use of a computer and can't be checked by humans 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.

Formal statement in graph theory

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.

Real world counter examples

In the real world, not all countries are contiguous (e.g. Alaska as part of the US), and one typically requires that all parts of a country receive the same color. Under these conditions, four colors are not always sufficient. Consider for instance the map

                 -----------
                |     |     |
                | D   |  C  |
              --|   ----    |
             |  |  |    |   |
             |   --| A  |   |
         ----|  |   ----    |
        |    |  |  B   |    |
        | A  |   ------ ----
         ----|    E       |
              ------------

where the regions labeled 'A' belong to the same country. Five colors are required if those two regions are to receive the same color. In a similar manner, one can construct situations which require arbitrary many colors.

Does a situation like this exist on Earth?

References:

Appel, K. and Haken, W. "Every Planar Map is Four-Colorable" Providence, RI: American Mathematical Society, 1989
History of the Four Color Theorem (external link)