Der Vier-Farben-Satz

Geschichte

Der Satz wurde erstmals 1852 von Francis Guthrie als Vermutung aufgestellt, als er in einer Karte die Grafschaften von England färben wollte. Es war offensichtlich, dass drei Farben nicht ausreichten – siehe Abbildung rechts – und man fünf in keinem konstruierten Beispiel brauchte. In einem Brief des Londoner Mathematikprofessors Augustus De Morgan vom 23. Oktober 1852 an den irischen Kollegen William Rowan Hamilton wurde die Vermutung erstmals diskutiert und veröffentlicht: „Genügen vier oder weniger Farben, um die Länder einer Karte so zu färben, dass benachbarte Länder verschiedene Farben tragen?“

Der englische Mathematiker Arthur Cayley stellte das Problem 1878 der mathematischen Gesellschaft Londons vor. Innerhalb nur eines Jahres fand Alfred Kempe einen scheinbaren Beweis für den Satz. Elf Jahre später, 1890, zeigte Percy Heawood, dass Kempes Beweisversuch fehlerhaft war. Ein zweiter fehlerhafter Beweisversuch, 1880 von Peter Guthrie Tait veröffentlicht, konnte ebenfalls elf Jahre lang nicht widerlegt werden. Erst 1891 zeigte Julius Petersen, dass auch Taits Ansatz nicht korrekt war. Heawood gab im Jahre 1890 mit der Widerlegung von Kempes „Vier-Farben-Beweis“ zusätzlich einen Beweis für den Fünf-Farben-Satz an, womit eine obere Grenze für die Färbung von planaren Graphen zum ersten Mal fehlerfrei bewiesen wurde. In Kempes fehlerhaftem Versuch steckten bereits grundlegende Ideen, die zum späteren Beweis durch Appel und Haken führten.

Heinrich Heesch entwickelte in den 1960er und 1970er Jahren einen ersten Entwurf eines Computerbeweises.

Dieser konnte von Kenneth Appel und Wolfgang Haken 1976 verbessert werden. Der Beweis reduzierte die Anzahl der problematischen Fälle von Unendlich auf 1936 (eine spätere Version sogar 1476), die durch einen Computer einzeln geprüft wurden.

1996 konnten Neil Robertson, Daniel Sanders, Paul Seymour und Robin Thomas einen modifizierten Computerbeweis finden, der die Fälle auf 633 reduzierte. Auch diese mussten per Computer geprüft werden.

2005 haben Georges Gonthier und Benjamin Werner einen formalen Beweis des Satzes in dem Beweisassistenten Coq konstruiert.

Der Vier-Farben-Satz war das erste große mathematische Problem, das mit Hilfe von Computern gelöst wurde. Deshalb wurde der Beweis von einigen Mathematikern nicht anerkannt, da er nicht direkt durch einen Menschen nachvollzogen werden kann. Schließlich muss man sich auf die Korrektheit des Compilers und der Hardware verlassen. Auch der Mangel an mathematischer Eleganz des Beweises wurde kritisiert.

Dieser Artikel basiert auf dem Artikel Vier-Farben-Satz aus der freien Enzyklopädie Wikipedia und steht unter der Doppellizenz GNU-Lizenz für freie Dokumentation und Creative Commons CC-BY-SA 3.0 Unported (Kurzfassung). In der Wikipedia ist eine Liste der Autoren verfügbar.