Four Color Theorem

The Four Color Theorem, conjectured in 1852 and proved in 1976, states that any map can be colored with four colors such that adjacent regions have different colors. This translates to vertex coloring of planar graphs.

TheoremFour Color Theorem

Every planar graph has chromatic number at most 4: $\chi(G) \leq 4 \text{ for all planar } G$

Moreover, there exist planar graphs requiring exactly 4 colors (e.g., $K_4$ ), so the bound is tight.

The proof by Appel and Haken (1976) used computer verification of hundreds of configurations, making it the first major theorem proved with computer assistance—controversial at the time but now accepted.

ProofProof Overview

The proof strategy involves:

Unavoidable set: Identify configurations that every planar graph must contain
Reducible configurations: Show each configuration can be 4-colored if smaller graphs can
Computer verification: Check that an explicit finite set of configurations is both unavoidable and reducible

The computerized case analysis examined 1,936 configurations, later simplified to 633 by Robertson et al. (1996).

■

TheoremFive Color Theorem

Every planar graph is 5-colorable: $\chi(G) \leq 5$ for planar $G$ .

This theorem has a short human-verifiable proof using induction and Euler's formula, contrasting with the Four Color Theorem's complexity.

ExampleMaps Requiring Four Colors

Consider four countries arranged such that each borders all others—this requires $K_4$ , which needs 4 colors. While $K_4$ is the smallest example, complex planar graphs can also require 4 colors despite not containing $K_4$ directly.

Remark

Extensions to other surfaces: the torus requires 7 colors, the double torus 8 colors. The Heawood formula gives the chromatic number for surfaces of genus $g \geq 1$ as: $\chi(S_g) = \left\lfloor \frac{7 + \sqrt{1+48g}}{2} \right\rfloor$ Remarkably, this formula is exact for all $g \geq 1$ but fails for $g=0$ (sphere/plane) where the answer is 4, not 5.