The Four Color Theorem

The four color theorem (4CT) is a celebrated result in mathematics and computer science. It asserts that given any separation of a plane into contiguous regions, producing a figure called a map, no more than four colors are required to color the regions of the map so that no two adjacent regions have the same color.

First proposed in 1852, the theorem remained unproven for over a century. Its eventual demonstration in 1976 by Kenneth Appel and Wolfgang Haken marked a watershed moment in mathematical history, as it was the first major theorem to be proved using a computer.

Historical Development

The conjecture originated in October 1852, when Francis Guthrie, a recent graduate at the University of London, observed that four colors seemed sufficient to color any map of English counties while preparing an atlas. He posed the question to his brother Frederick, who passed it to their teacher, the prominent mathematician Augustus De Morgan.

De Morgan circulated the problem among his contemporaries, but a rigorous proof eluded them. The first published attempt by Alfred Kempe in 1879 was widely accepted for eleven years until Percy Heawood discovered a critical flaw in 1890. Heawood salvaged parts of Kempe's argument to prove the five-color theorem, which held until 1976.

The breakthrough came when Kenneth Appel and Wolfgang Haken of the University of Illinois successfully combined traditional mathematical reasoning with massive computational verification, finally settling the conjecture.

Mathematical Formulation

In modern terms, the four color theorem is expressed using graph theory. Any map can be abstracted as a planar graph G = (V, E), where:

Vertices (V)

Represent the regions (countries, states, etc.) of the map.

Edges (E)

Connect vertices whose corresponding regions share a border.

Coloring

A function c: V → {1, 2, 3, 4} such that c(u) ≠ c(v) for every edge (u, v).

The theorem states that the chromatic number χ(G) of any planar graph is at most 4. This is deeply connected to Euler's polyhedral formula V - E + F = 2, which constrains the average degree of vertices in planar graphs and guarantees the existence of a vertex with degree at most 5—a key insight used in early five-color proofs.

The Computer-Aided Proof

Appel and Haken's proof strategy relied on two core concepts: unavoidable sets and reducible configurations.

• Unavoidable Set: A collection of graph configurations such that every planar graph must contain at least one configuration from the set.
• Reducible Configuration: A configuration that cannot appear in a minimal counterexample to the four color theorem.

The mathematicians identified an unavoidable set of 1,936 reducible configurations (later refined to 633). Proving each configuration was reducible required examining thousands of cases, far beyond human capacity. They wrote a computer program that verified each case, running for approximately 1,200 hours on an IBM 360.

The result was controversial. Many mathematicians questioned whether a proof relying on machine verification could be considered "mathematical" in the traditional sense. Over time, however, the proof gained acceptance, and subsequent work by Robertson, Sanders, Seymour, and Thomas (1996–1997) simplified the configuration set and improved the verification algorithm, making it publicly reproducible.

Significance & Impact

The four color theorem fundamentally altered the landscape of mathematical practice:

1. Computational Mathematics: It legitimized computer-assisted proofs, paving the way for projects like the Flyspeck project (formal verification of the Kepler conjecture) and modern proof assistants like Coq and Lean.
2. Graph Theory & Algorithms: Map coloring is a special case of the broader graph coloring problem, which is NP-hard for general graphs. The 4CT shows that planar graphs are a tractable subclass, with applications in register allocation, scheduling, and frequency assignment.
3. Philosophy of Mathematics: It sparked enduring debates about the nature of proof, verification, and certainty. If a proof cannot be fully read by a human, what constitutes mathematical truth?

Despite its complexity, the theorem remains elegantly simple in statement: every planar map is 4-colorable. It stands as a testament to the power of combining human insight with computational might.