abyiber.com
Back to Blog

The Four Color Theorem: The First Computer-Assisted Proof

Understanding the four color theorem, why it was controversial as the first major computer-assisted proof, the techniques of reducibility and discharging, and what it means for the nature of proof.

2025-07-25
Share
Proofsproofsfour-colorgraph-theorycomputer-assisted-proof

Terminology

Term Definition
Planar graph A graph that can be drawn in the plane with no edge crossings; every map corresponds to a planar graph
Graph coloring Assigning colors to vertices such that no two adjacent vertices share the same color
Chromatic number The minimum number of colors needed to properly color a graph, written $\chi(G)$
Reducibility A configuration is reducible if any map containing it can be 4-colored by reducing to a smaller map that is already 4-colorable
Discharging A counting technique that assigns "charges" to vertices/faces and redistributes them to prove that every map must contain a reducible configuration
Unavoidable set A set of configurations such that every planar graph must contain at least one of them
Euler's formula For a connected planar graph: V - E + F = 2, where V = vertices, E = edges, F = faces
Configuration A small subgraph pattern that may appear in a planar graph; the proof checks 1,476 specific configurations
Computer-assisted proof A mathematical proof where essential steps are verified by computer, because they involve too many cases for human checking

What & Why

The four color theorem states that every map can be colored with at most four colors such that no two adjacent regions share the same color. Conjectured in 1852 by Francis Guthrie, it resisted proof for over a century. When Kenneth Appel and Wolfgang Haken finally proved it in 1976, their proof required a computer to check 1,476 configurations, each verified through extensive computation.

This made it the first major theorem proved with essential computer assistance, and it ignited a philosophical firestorm. Is a proof that no human can fully verify really a proof? Can we trust a computer's output? These questions remain relevant today as formal verification, proof assistants, and computer-checked mathematics become increasingly important.

The theorem itself is a statement about planar graphs (the dual representation of maps). It says that every planar graph has chromatic number at most 4: \chi(G) \leq 4 for all planar G. The five color theorem (\chi(G) \leq 5) has a short, elegant proof. Reducing from 5 to 4 is where the difficulty lies, and where the computer becomes necessary.

How It Works

From Maps to Graphs

Every map corresponds to a planar graph: each region becomes a vertex, and two vertices are connected by an edge if their regions share a border. Coloring the map so no adjacent regions share a color is equivalent to properly coloring this graph.

Map (4 regions) A B C D = Graph (4 vertices, edges = shared borders) A B C D Adjacent regions = connected vertices. 4 colors suffice.

The Proof Strategy

The proof combines two techniques:

  1. Find an unavoidable set of configurations: a collection of subgraph patterns such that every planar graph must contain at least one.
  2. Show every configuration in the set is reducible: if a graph contains it, the graph can be 4-colored by reducing to a smaller graph.

Together, these imply that every planar graph is 4-colorable, by strong induction on the number of vertices.

Unavoidable Set Every planar graph contains at least one configuration Reducibility Each configuration can be reduced to a smaller graph By induction: every planar graph is 4-colorable Computer checks 1,476 configurations for reducibility ~1,200 hours of computation in 1976

Discharging: Proving Unavoidability

Discharging uses Euler's formula V - E + F = 2 to assign "charges" to vertices and faces. The total charge is fixed (related to 12, from Euler's formula). By redistributing charges according to specific rules, you show that some configuration must have positive charge, meaning it must appear in the graph.

Reducibility: The Computer's Role

For each of the 1,476 configurations, the computer verifies that any 4-coloring of the boundary can be extended to a 4-coloring of the interior (after possible Kempe chain recolorings). This case analysis is too large for human verification but straightforward for a computer.

The Controversy

Many mathematicians were uncomfortable with a proof that could not be checked by hand. The concerns were:

  • Could the computer program have bugs?
  • Is a proof that requires trust in hardware and software really a proof?
  • Does this set a precedent that undermines mathematical certainty?

In 1997, Robertson, Sanders, Seymour, and Thomas produced a simpler proof with 633 configurations. In 2005, Gonthier and Werner formally verified the theorem in the Coq proof assistant, providing machine-checked certainty that the proof is correct.

Complexity Analysis

Problem Complexity Notes
4-color a planar graph $O(n^2)$ Constructive algorithm exists (Robertson et al.)
3-color a planar graph NP-complete Not all planar graphs are 3-colorable
$k$-color a general graph NP-complete for $k \geq 3$ Even for $k = 3$
Check if a coloring is valid $O(E)$ Verify no adjacent vertices share a color

Euler's formula constrains planar graphs. For a simple connected planar graph:

$E \leq 3V - 6$

This means the average degree is less than 6, so every planar graph has a vertex of degree at most 5. This structural constraint is what makes 4-coloring possible (and what fails for non-planar graphs).

Implementation

ALGORITHM GreedyFiveColor(graph)
INPUT: graph: a planar graph (adjacency list)
OUTPUT: a valid 5-coloring of the vertices
BEGIN
  // Every planar graph has a vertex of degree <= 5
  IF graph has 0 vertices THEN
    RETURN empty coloring
  END IF

  // Find a vertex of degree <= 5
  v <- vertex in graph with degree <= 5

  // Remove v and recursively 5-color the rest
  smallerGraph <- graph with v removed
  coloring <- GreedyFiveColor(smallerGraph)

  // v has at most 5 neighbors, using at most 5 colors
  // If fewer than 5 colors used by neighbors, pick an unused color
  usedColors <- {coloring[u] : u is neighbor of v}

  IF LENGTH(usedColors) < 5 THEN
    coloring[v] <- smallest color NOT IN usedColors
  ELSE
    // All 5 colors used by neighbors: use Kempe chain argument
    coloring[v] <- KempeChainRecolor(graph, v, coloring)
  END IF

  RETURN coloring
END

ALGORITHM CheckReducibility(configuration, boundaryColorings)
INPUT: configuration: a subgraph pattern
       boundaryColorings: all valid 4-colorings of the boundary
OUTPUT: true if every boundary coloring extends to the interior
BEGIN
  FOR EACH boundaryColoring IN boundaryColorings DO
    extended <- false

    // Try all possible colorings of interior vertices
    FOR EACH interiorColoring OF interior vertices using 4 colors DO
      IF IS_VALID_COLORING(boundaryColoring + interiorColoring) THEN
        extended <- true
        BREAK
      END IF
    END FOR

    IF NOT extended THEN
      // Try Kempe chain recolorings of the boundary
      FOR EACH kempeVariant OF KempeRecolorings(boundaryColoring) DO
        FOR EACH interiorColoring OF interior vertices DO
          IF IS_VALID_COLORING(kempeVariant + interiorColoring) THEN
            extended <- true
            BREAK
          END IF
        END FOR
        IF extended THEN BREAK
      END FOR
    END IF

    IF NOT extended THEN
      RETURN false  // This configuration is NOT reducible
    END IF
  END FOR

  RETURN true  // All boundary colorings extend: configuration is reducible
END

ALGORITHM DischargeAndCheck(planarGraph)
INPUT: planarGraph: a planar graph
OUTPUT: a reducible configuration found in the graph
BEGIN
  // Assign initial charges using Euler's formula
  FOR EACH vertex v DO
    charge[v] <- 6 - degree(v)  // vertices of degree < 6 have positive charge
  END FOR

  // Apply discharging rules to redistribute charges
  APPLY_DISCHARGING_RULES(charge, planarGraph)

  // After discharging, some configuration must have positive total charge
  // Search for a configuration from the unavoidable set
  FOR EACH config IN UNAVOIDABLE_SET DO
    IF config APPEARS_IN planarGraph THEN
      RETURN config
    END IF
  END FOR
END

Real-World Applications

  • Map coloring in cartography and GIS systems uses graph coloring algorithms; the four color theorem guarantees that four colors always suffice for any map
  • Register allocation in compilers is a graph coloring problem: variables that are live simultaneously cannot share a register, and the interference graph must be colored with the available registers
  • Frequency assignment in wireless networks uses graph coloring to assign non-interfering frequencies to nearby transmitters
  • The formal verification of the four color theorem in Coq (2005) was a landmark for computer-verified mathematics, demonstrating that large proofs can be machine-checked with high confidence
  • Scheduling problems (exam timetabling, task scheduling) reduce to graph coloring, where the four color theorem provides bounds for planar constraint graphs
  • The philosophical debate about computer-assisted proofs continues to shape how the mathematical community views formal verification, proof assistants, and the role of computers in mathematics

Key Takeaways

  • The four color theorem states that every planar graph can be properly colored with at most 4 colors; conjectured in 1852, proved in 1976 by Appel and Haken
  • The proof uses two techniques: an unavoidable set (every planar graph contains at least one of 1,476 configurations) and reducibility (each configuration can be reduced to a smaller 4-colorable graph)
  • It was the first major theorem requiring essential computer assistance, as the reducibility of 1,476 configurations could not be checked by hand
  • The controversy it sparked about the nature of proof led to the development of formal verification: in 2005, the theorem was machine-verified in the Coq proof assistant
  • While 4-coloring planar graphs is polynomial ($O(n^2)$), 3-coloring planar graphs is NP-complete, showing the sharp boundary between tractable and intractable
  • Graph coloring has practical applications in register allocation, frequency assignment, scheduling, and map rendering