Four Color Theorem

Any planar map can be colored with 4 colors so no adjacent regions share a color

About

The Four Color Theorem (proved 1976 by Appel & Haken — first major computer-assisted proof) states that every planar map needs at most 4 colors.
Color:
Regions Grid Voronoi
Click a region to color it. Try to use only 4 colors!

History

1852: Guthrie conjectured it
1879: Kempe's "proof" — flawed
1890: Heawood found the flaw
1976: Appel & Haken proved it using 1200 hours of computer time
2005: Robertson et al gave a cleaner proof
2005: Gonthier verified it in Coq

Key Idea

Every planar graph has a vertex of degree ≤ 5. By induction + Kempe chain recoloring, 4 colors always suffice. The chromatic polynomial counts colorings.