Four-Color Theorem — Graph Coloring and the Computer-Assisted Proof

1. The Theorem and Its History

Four-Color Theorem: Given any separation of a plane into contiguous regions, the regions can be colored using at most four colors so that no two adjacent regions have the same color. (Two regions are adjacent if they share a common boundary segment of positive length; corners don't count.)

• 1852: Francis Guthrie notices the four-color property while coloring a map of English counties and asks his brother Frederick, who asks Augustus De Morgan.
• 1879: Alfred Kempe publishes an alleged proof using "Kempe chains" — a technique that survives in modern proofs even though the full argument was flawed.
• 1880: Peter Tait proposes a different approach via Hamiltonian cycles — also later found insufficient.
• 1890: Percy Heawood finds the error in Kempe's proof but salvages it to prove the weaker five-color theorem.
• 1976: Kenneth Appel and Wolfgang Haken use a computer to verify 1,936 reducible configurations — a complete proof at last.
• 1997: Neil Robertson, Daniel Sanders, Paul Seymour, and Robin Thomas produce a cleaner computer-assisted proof using 633 configurations.
• 2005: Georges Gonthier formally verifies the theorem in Coq, a proof assistant system.

2. Graph Theory Formulation

A map coloring problem is equivalent to a graph coloring problem. Convert the map to a planar graph: one vertex per region, one edge between vertices whose regions share a boundary. The four-color theorem then states: every planar graph is 4-colorable.

3. The Five-Color Theorem

The simpler five-color theorem has an elegant proof by strong induction requiring no computer:

1. Every planar graph has a vertex v with degree ≤ 5 (by Euler's formula argument).
2. Remove v; by induction the remaining graph is 5-colorable.
3. Reinsert v. If its ≤5 neighbours use ≤4 colors, assign the fifth color to v. Done.
4. If all 5 neighbors use all 5 colors (in cyclic order c₁, c₂, c₃, c₄, c₅ around v), we need Kempe's trick:
5. Consider the subgraph induced by colors c₁ and c₃. If v₁ and v₃ are in different connected components, swap colors in v₁'s component — now both v₁ and v₃ use colors from {c₁,c₃}, freeing one for v.
6. If same component: there's a c₁-c₃ path from v₁ to v₃. Then v₂ and v₄ must be in different components of the c₂-c₄ subgraph (they can't cross the path). Swap v₂'s component to free c₂ for v.

The failure of this to extend directly to four colors is why the four-color proof requires checking thousands of configurations — Kempe's "fix" doesn't always work for step 4 when trying to prove four suffice.

4. The Appel-Haken Proof

The proof strategy uses two key concepts:

• Unavoidable set: A set of configurations such that every planar graph must contain at least one of them.
• Reducible configuration: A configuration that can be "reduced" — if a graph contains it, the graph is 4-colorable if and only if a smaller graph is. (Essentially: we can always extend a 4-coloring from the rest of the graph to include this piece.)

Appel and Haken found an unavoidable set of 1,936 configurations and proved each is reducible. Together these guarantee: any planar graph contains a reducible configuration, so it can be 4-colored by induction on size.

5. Greedy Graph Coloring

For practical graph coloring (not necessarily optimal), the greedy algorithm assigns the lowest available color to each vertex in sequence:

function greedyColor(graph) {
  const color = new Array(graph.n).fill(-1);
  for (let v = 0; v < graph.n; v++) {
    const usedColors = new Set(
      graph.adj[v].filter(u => color[u] !== -1).map(u => color[u])
    );
    let c = 0;
    while (usedColors.has(c)) c++;
    color[v] = c;
  }
  return color;
}

Greedy coloring uses at most Δ(G) + 1 colors (where Δ(G) is the maximum degree), but may use more than the chromatic number χ(G). The vertex ordering matters greatly — optimal orderings include largest-first (by degree), smallest-last, and DSatur (dynamic saturation heuristic).

Finding the exact chromatic number χ(G) is NP-complete in general. For planar graphs, 4-colorability is always guaranteed, but finding a 4-coloring efficiently (in polynomial time) is still an open problem — we only know P algorithms exist for {2,3}-coloring of planar graphs.

6. Chromatic Polynomial

The chromatic polynomial P(G, k) counts the number of proper k-colorings of graph G:

The chromatic number χ(G) is the smallest k > 0 for which P(G, k) > 0. Computing P(G, k) is #P-hard in general — exponentially more difficult than just deciding colorability.

7. Applications Beyond Maps

• Register allocation: In compiler optimization, variables are vertices; edges connect variables live at the same time. Coloring with ≤ K colors = allocating to K CPU registers without spilling to memory.
• Frequency assignment: Cell towers (vertices) in a radio network need different frequencies if their coverage areas overlap — minimum chromatic number minimizes the spectrum required.
• Scheduling: Tasks (vertices) sharing resources are adjacent; minimum coloring = minimum number of time slots needed.
• Sudoku: A 9×9 Sudoku is a graph coloring problem on 81 vertices with 9 colors where row/column/box constraints define the edges.
• GPU rendering — PBD constraint colouring: As described in the Position-Based Dynamics article, constraints sharing vertices form a graph — coloring it into groups enables parallel GPU processing.