The Four Color Theorem

Graph Theory · Axiom Academy

A journey through one of mathematics' most famous problems and its groundbreaking computer-assisted proof 1. The Statement and Early History The Four Color Theorem: Every planar graph (or map) can be properly colored using at most four colors, such that no two adjacent vertices (or regions) share the same color. The conjecture originated in 1852 when Francis Guthrie, while coloring a map of England's counties, noticed that four colors seemed sufficient. His brother Frederick asked his mathematics professor, Augustus De Morgan, who found the question intriguing but couldn't solve it. 2. The 124-Year Quest for Proof For over a century, the Four Color Theorem resisted all attempts at proof. The problem appeared deceptively simple—anyone could understand it—yet it defied the greatest mathematical minds. Mathematical attempts focused on two key concepts developed by Kempe: Unavoidable configurations: Sets of graph structures where every planar graph must contain at least one Reducible configurations: Structures that, if they appear in a minimal counterexample, lead to a contradiction The proof strategy became clear: find an unavoidable set of reducible configurations. But the sheer number of cases to check seemed overwhelming. 3. The 1976 Computer-Assisted Proof Kenneth Appel and Wolfgang Haken at the University of Illinois finally proved the theorem in 1976, but their approach was revolutionary—and controversial. Identify an unavoidable set of 1,936 configurations

This is the written version of the interactive lesson above. See the full Graph Theory course.