Topologie von Flächen XVI

Das 4-Farben-Problem und Computerbeweise in der Mathematik.

Als 4-Farben-Problem bezeichnet man die Frage, ob sich jede Landkarte (auf der Sphäre) mit 4 Farben färben läßt, so daß benachbarte Länder unterschiedliche Farbe haben.

Das Bild zeigt eine Färbung der Provinzen Ecuador’s mit 4 Farben. Wenn man berücksichtigt, daß auch noch der Ozean und die Nachbarländer gefärbt werden müssen, wird es schon erheblich schwieriger eine Färbung mit 4 Farben zu finden. Dagegen ist es sehr einfach eine Färbung mit 6 Farben zu finden. (Man färbe Kolumbien mit der Farbe von Napo, den Ozean und Peru mit der 5. und 6. Farbe.)

Die nächste Frage wäre natürlich, wie man dann eine noch größere Landkarte weiterfärbt .

Das Beispiel zeigt jedenfalls, daß das Färben einer Landkarte mit 5 oder 6 Farben erheblich einfacher sein sollte als mit 4 Farben.

Der 5-Farben-Satz (also der Satz, daß sich jede Landkarte auf der Sphäre mit 5 Farben färben läßt) ist tatsächlich bereits im 19. Jahrhundert von Heawood bewiesen worden. Man findet einen 3-Seiten-Beweis im ‘Buch der Beweise’ von Aigner-Ziegler (Seite 204-206) oder auf Wikipedia.

Der 6-Farben-Satz ist so einfach, daß wir sogar hier einen Beweis geben können.

Satz: Jede Landkarte auf einer Sphäre läßt sich mit 6 Farben färben.
Beweis durch vollständige Induktion nach der Anzahl der Länder:
Der Induktionsanfang (für eine Karte mit nur einem Land) ist natürlich klar.
Sei der Satz schon bewiesen für Landkarten mit n Ländern.
Wir haben jetzt eine Karte mit n+1 Ländern. Wenn es ein Land gibt, daß nur 5 (oder weniger) Nachbarn hat, sind wir fertig: wir benutzen die Induktionsvoraussetzung, um die anderen n Länder mit 6 Farben zu färben. Weil das letzte Land nur 5 Nachbarn hat, gibt es eine Farbe, die von seinen Nachbarn nicht verwendet wurde und mit der wir dieses letzte Land also färben können.
Wir müssen also beweisen: für jede Zerlegung der Sphäre gibt es ein Land, das höchstens 5 Nachbarn hat.
Dies beweisen wir nun mit Hilfe der Eulerschen Polyederformel: wenn wir die Länder als (krummlinige) Vielecke auffassen, und mit E,F,K die Gesamtzahl der Ecken, Kanten, Flächen bezeichnen, dann ist E-K+F=2.
Andererseits ist 3E≤2K, weil jede Kante 2 Ecken hat, aber an jeder Ecke mindestens 3 Kanten zusammenkommen. Wenn jedes Land mindestens 6 Nachbarn hätte, d.h. jede Fläche mindestens 6 Kanten hätte (und natürlich jede Kante zu 2 Flächen gehört), dann wäre 2F≤6K 6F≤2K. Damit ergibt sich aber der Widerspruch
2=E-K+F ≤ 2/3 K – K + 1/3 K=0.
Wegen diesem Widerspruch muß es also mindestens ein Land mit höchstens 5 Nachbarn geben. Damit funktioniert der Induktionsbeweis wie oben beschrieben.

Der Kern des obigen Beweises ist: es gibt bestimmte geometrische Strukturen (nämlich Dreieck oder Viereck oder Fünfeck), die in jeder Landkarte vorkommen müssen (zumindest eine der drei).
Aus der Unvermeidbarkeit einer dieser Strukturen folgt das Funktionieren des Induktionsbeweises für den 6-Farben-Satz. (Übrigens beruht auch der etwas kompliziertere Induktionsbeweis des 5-Farben-Satzes auf der Unvermeidbarkeit einer dieser Strukturen.)

Für den Beweis des 4-Farben-Satzes reichen diese drei unvermeidbaren Strukturen (Dreieck, Viereck, Fünfeck) nicht mehr. Man hat lange versucht, andere Strukturen zu finden, aus deren Unvermeidbarkeit der 4-Farben-Satz folgt. Solche Strukturen gibt es tatsächlich. Allerdings so viele, daß man sie nur mit Computerhilfe in den Griff bekommt.

Dies gelang zuerst Kenneth Appel und Wolfgang Haken 1976/77. In ihrem ersten Beweis fanden sie 1825 unvermeidbare Strukturen, in einer späteren Version kamen sie mit 1478 aus.

Aus der Wikipedia: In ihrem Beweis bauten sie auf Ideen von Heinrich Heesch auf, der in den 1960er Jahren ebenfalls an der TU Hannover an einem Beweis mit Computerhilfe arbeitete, aber nur ungenügende finanzielle Unterstützung erhielt und auch sonst relativ isoliert. Appel und Haken benötigten für ihren Beweis 1200 Stunden Rechenzeit auf einer IBM 360 mit 64 kB Arbeitsspeicher, die an der Universität sonst nur Verwaltungs-Zwecken diente. Ihre Arbeit an dem Beweis dauerte rund vier Jahre und begann 1972. Dabei wurden sie auch von den Kindern von Appel unterstützte (sein Sohn Andrew ist inzwischen auch Professor für Informatik in Princeton). Zur Feier des Beweises führte die Universität von Illinois einen neuen Poststempel Four colors suffice ein. Anscheinend wurde der Großteil der Programmierung (in Assembler-Sprache) von Appel durchgeführt, während der Topologe Haken konzeptionelle Ideen beisteuerte.

Der Computerbeweis des 4-Farben-Problems führte nach seiner Veröffentlichung 1977 zu großen Diskussionen. Es ging um die Frage, ob ein Computerbeweis, der so umfangreich ist, daß kein Mensch seine Richtigkeit überprüfen kann, den Ansprüchen an einen mathematischen Beweis genügt. Befördert wurden diese Diskussionen noch durch einige kleinere Fehler in Details, die in den nächsten Jahren gefunden wurden, sich aber alle leicht korrigieren ließen. (1982 hatte Ulrich Schmidt in seiner Diplomarbeit 40% des Beweises von Hand überprüft, dabei 15 Fehler gefunden, von denen aber nur einer wirklich eine inhaltliche Korrektur des Beweises nötig machte.)

1996 fanden Robertson, Sanders, Seymour, Thomas einen Beweis mit ‘nur’ 633 unvermeidbaren Strukturen. Auch diese können bisher nur von einem Computer geprüft werden.

Heute gelten Computerbeweise zwar als allgemein akzeptiert, die meisten Mathematiker bevorzugen aber schon Beweise, deren Richtigkeit man selbst nachprüfen kann.

Ein relativ aktuelles Beispiel ist Hales’ Beweis der Kepler-Vermutung: die effektivste Packung von Kugeln im 3-dimensionalen Raum (d.h. mit geringstmöglichem freigelassenem Volumen) entsteht durch Anordnung der Kugeln in einem 6-Eck-Muster. (Annals of Mathematics (2) 162, No. 3, 1065-1185, 2005)

Ein anderes Beispiel eines mit Computerhilfe bewiesenen Satzes ist der Satz von Gabai-Meyerhoff-Thurston, daß homotopie-hyperbolische 3-Mannigfaltigkeiten hyperbolisch sind. (Annals of Mathematics (2) 157, No. 2, 335-431, 2003) Dieser Satz folgt aber inzwischen auch aus Perelman’s Arbeiten über Geometrisierung, so daß man ihn jetzt also auch ohne Computer beweisen kann.

Es gibt nach wie vor viele Graphentheoretiker, die versuchen, einen ‘verstehbaren’ Beweis des 4-Farben-Satzes zu finden.

Diverse Graphfärbungsprogramme findet man übrigens bei Joseph Culberson.

Nachtrag: Ein Souvenir, das mir von Herrn Grassmann aus Mühlenbeck zugeschickt wurde:

Teil 1, Teil 2, Teil 3, Teil 4, Teil 5, Teil 6, Teil 7 , Teil 8, Teil 9 , Teil 10 ,Teil 11, Teil 12, Teil 13, Teil 14, Teil 15

Neil Robertson, Daniel P. Sanders, Paul Seymour, Robin Thomas (1996). A new proof of the four-colour theorem Electronic Research Announcements of the American Mathematical Society, 02 (01), 17-26 DOI: 10.1090/S1079-6762-96-00003-0