Der Vierfarbensatz besagt, dass jede auf einer Ebene gezeichnete Karte mit höchstens vier Farben gefärbt werden kann, sodass keine zwei Regionen mit gemeinsamer Grenze dieselbe Farbe haben. Zwei Regionen, die sich nur in einem Punkt berühren, dürfen dieselbe Farbe teilen. Der Satz gilt für jede Karte, ganz gleich, wie kompliziert sie ist.
Die Regionen 1, 2, 3 und 4 grenzen jeweils an mehrere andere. Die linke Region mit Farbe 4 und die rechte Region mit Farbe 4 teilen keine Grenze und dürfen deshalb dieselbe Farbe haben. Genau 4 Farben werden hier benötigt.
Francis Guthrie vermutete den Satz 1852 beim Färben einer Karte englischer Grafschaften. Er bemerkte, dass vier Farben immer auszureichen schienen, konnte es aber nicht beweisen. Das Problem widerstand 124 Jahre lang allen Mathematikern. Viele falsche Beweise wurden veröffentlicht und widerlegt. Fünf Farben reichen immer aus und lassen sich von Hand mit Eulers Formel für planare Graphen beweisen.
Vom ersten Verdacht bis zum Beweis vergingen 124 Jahre. Der Beweis von 1976 war der erste große mathematische Satz, der von einem Computer verifiziert wurde.
Der Beweis von Kenneth Appel und Wolfgang Haken aus dem Jahr 1976 war der erste große mathematische Satz, der mit Hilfe eines Computers bewiesen wurde. Er reduzierte alle möglichen Karten auf 1.936 Konfigurationen und ließ einen Computer jede einzelne über mehr als 1.200 Stunden CPU-Zeit überprüfen. Viele Mathematiker fühlten sich mit einem Beweis unwohl, den man nicht von Hand nachprüfen konnte. Ein menschenlesbarer Beweis, falls es ihn gibt, ist bis heute nicht gefunden.
Fünf äußere Regionen, also eine ungerade Anzahl, zwingen den Ring dazu, 3 Farben zu verwenden: Ein 5-Zyklus lässt sich nicht mit nur 2 Farben färben. Die zentrale Region grenzt an alle fünf äußeren Regionen und berührt damit alle drei Ringfarben. Sie braucht deshalb eine vierte Farbe. Das zeigt, dass vier Farben manchmal wirklich nötig sind.
Jede auf einer Ebene gezeichnete Karte kann mit höchstens vier Farben gefärbt werden, sodass keine zwei Regionen mit gemeinsamer Grenze dieselbe Farbe haben. Francis Guthrie formulierte die Vermutung 1852. Appel und Haken bewiesen sie 1976, indem sie 1.936 Konfigurationen per Computer überprüften, und machten sie so zum ersten großen Satz mit Computerunterstützung. Eine kürzere Überprüfung von Robertson, Sanders, Seymour und Thomas reduzierte dies 1997 auf 633 Konfigurationen. Auf einem Torus gilt der Satz nicht, dort können sieben Farben nötig sein.