In der Geschichte der Mathematik ist einer der berühmtesten und gleichzeitig umstrittensten Sätze der “Vier-Farben-Satz” (Four Color Theorem). Er ist eine so einfache Behauptung, dass sogar ein Grundschüler sie verstehen kann: “Für jede ebene Landkarte reichen vier Farben aus, um sie so zu färben, dass benachbarte Regionen unterschiedliche Farben haben.” Dennoch erforderte sein Beweis mehr als ein Jahrhundert und einen Paradigmenwechsel namens “Computerbeweis”, der die Grundlagen der Mathematik als Disziplin erschütterte.

In diesem Artikel werden wir das Gesamtbild des Vier-Farben-Satzes aus mathematischer, historischer und philosophischer Perspektive gründlich entschlüsseln, beginnend mit einer einfachen Frage aus dem Jahr 1852 über die Herausforderungen und Rückschläge von Genies bis hin zum Höhepunkt der modernen Mathematik, die eine neue Intelligenz namens Computer zu ihrem Verbündeten machte. Insbesondere werden wir tief in tiefgründige mathematische Themen wie die geometrische Struktur von Kempes falschem Beweis und Heawoods Gegenbeispiel, den vollständigen Beweis des Fünf-Farben-Satzes, die Mathematik der Entladungsmethode (Discharging Method), den Algorithmus von Appel und Haken, die Details des formalen Beweises durch Coq und die Verbindung zur NP-Vollständigkeit eintauchen.

Kapitel 1: 1852, Francis Guthries einfache Frage und die Erhebung zur Graphentheorie

Die Formulierung des Kartenfärbungsproblems

Die Geschichte beginnt 1852 bei Francis Guthrie, einem jungen Mann, der gerade seinen Abschluss am University College London in England gemacht hatte. Als er eine Karte der englischen Grafschaften kolorierte, bemerkte er eine merkwürdige Tatsache: “Egal wie komplex eine Karte ist, reichen nicht vier Farben aus, um sie so zu färben, dass benachbarte Grafschaften unterschiedliche Farben haben?”

Francis teilte diese Frage seinem jüngeren Bruder Frederick Guthrie mit, der zu dieser Zeit Mathematik am University College studierte. Frederick legte dieses Problem seinem Betreuer Augustus De Morgan vor, einem der führenden Mathematiker seiner Zeit. De Morgan war sofort von der Faszination dieses Problems gefesselt und teilte es in Briefen mit Freunden wie William Rowan Hamilton. Dies war der Moment, in dem das in der Geschichte der Mathematik strahlende “Vier-Farben-Problem” geboren wurde.

Eulerscher Polyedersatz und die Dualität planarer Graphen

Um das Problem der Kartenfärbung mathematisch rigoros zu behandeln, ist eine Formulierung in die Graphentheorie unerlässlich. Wenn man jede Region (Land oder Grafschaft) auf der Karte als “Knoten” (Vertex) betrachtet und benachbarte Regionen durch “Kanten” (Edge) verbindet, erhält man einen “planaren Graphen” (Planar Graph), bei dem sich die Kanten auf der Ebene nicht schneiden. Diese Transformation ist als Operation zur Erstellung eines “dualen Graphen” (Dual Graph) bekannt. Die Grenzen der ursprünglichen Karte entsprechen den Kanten des Graphen und die Flächen den Knoten.

Das Vier-Farben-Problem lässt sich auf das Knoten-Färbungsproblem (Vertex Coloring Problem) von Graphen reduzieren: “Können die Knoten eines beliebigen planaren Graphen mit vier Farben so gefärbt werden, dass benachbarte Knoten unterschiedliche Farben haben?”

Hier spielt der von Leonhard Euler entdeckte Polyedersatz eine äußerst wichtige Rolle. In einem zusammenhängenden planaren Graphen mit $V$ Knoten, $E$ Kanten und $F$ Flächen gilt die folgende invariante Beziehung:

Durch die Kombination dieses Satzes mit den grundlegenden Eigenschaften planarer Graphen lassen sich starke Einschränkungen bezüglich der Struktur planarer Graphen ableiten. Wir nehmen an, dass der Graph ein einfacher Graph ohne Mehrfachkanten oder Selbstschleifen ist, und betrachten weiter einen “maximal planaren Graphen” (Maximal Planar Graph), bei dem alle Flächen Dreiecke sind. Da das Hinzufügen von Kanten zu einem beliebigen planaren Graphen, um ihn maximal planar zu machen, die chromatische Zahl nicht erhöht, reicht es aus, den Vier-Farben-Satz für maximal planare Graphen zu beweisen.

In einem maximal planaren Graphen ist jede Fläche von genau drei Kanten begrenzt. Da eine Kante genau zwei Flächen begrenzt, gilt streng die folgende Beziehung zwischen der Anzahl der Flächen und der Anzahl der Kanten:

Wenn wir dies in Eulers Formel einsetzen, um $F$ zu eliminieren. Indem wir $F = \frac{2}{3}E$ in $V - E + F = 2$ einsetzen, erhalten wir:

In allgemeinen einfachen planaren Graphen werden Flächen von drei oder mehr Kanten begrenzt, sodass $3F \leq 2E$ gilt, was zu der folgenden Ungleichung führt:

Diese Ungleichung zeigt, dass es eine strikte Obergrenze für die Kantendichte in planaren Graphen gibt. Betrachten wir von hier aus den Grad (Degree, $\deg(v)$) jedes Knotens. Die Summe der Grade aller Knoten im Graphen ist genau das Doppelte der Anzahl der Kanten (Handschlaglemma).

Unter Verwendung der vorherigen Ungleichung $2E \leq 6V - 12$ erhalten wir:

Wenn wir beide Seiten durch die Anzahl der Knoten $V$ dividieren, erhalten wir den durchschnittlichen Grad der Knoten:

Die Tatsache, dass der durchschnittliche Grad strikt kleiner als 6 ist, beweist mathematisch vollständig, dass “mindestens ein Knoten einen Grad von 5 oder weniger haben muss”. Das heißt, in jedem einfachen planaren Graphen gibt es mindestens einen Knoten, dessen Grad entweder 1, 2, 3, 4 oder 5 ist. Diese Tatsache ist der grundlegendste Ausgangspunkt für das Konzept der später beschriebenen “unvermeidbaren Konfigurationen” und der absolute Kern des Beweises des Vier-Farben-Satzes.

Kapitel 2: Alfred Kempes “Beweis” und der Zusammenbruch nach 11 Jahren

Das Konzept der Kempe-Ketten und der brillante “Beweis”

Im Jahr 1879 veröffentlichte Alfred Bray Kempe, ein englischer Anwalt und Mathematiker, schließlich einen “Beweis” des Vier-Farben-Problems in den Zeitschriften “Nature” und dem “American Journal of Mathematics”. Sein Beweis war äußerst originell und wurde in den folgenden 11 Jahren von der mathematischen Welt allgemein als korrekt akzeptiert.

Der Kern von Kempes Beweis war eine revolutionäre Idee, die heute als “Kempe-Kette” (Kempe Chain) bekannt ist. Er verwendete vollständige Induktion. Er nahm an, dass der Vier-Farben-Satz für alle planaren Graphen mit $k$ Knoten gilt, und versuchte zu zeigen, dass er auch für Graphen mit $k+1$ Knoten gilt.

Aus dem zuvor erwähnten Eulerschen Satz folgt, dass in jedem planaren Graphen $G$ mit $k+1$ Knoten notwendigerweise ein Knoten $v$ existiert, dessen Grad 5 oder weniger ist. Betrachten wir einen Graphen $G'$, der durch Entfernen des Knotens $v$ und der damit verbundenen Kanten aus dem Graphen $G$ entsteht. Da $G'$ $k$ Knoten hat, kann er gemäß der Induktionsvoraussetzung mit vier Farben (hier nennen wir sie Rot, Blau, Grün und Gelb) gefärbt werden. Danach setzen wir $v$ wieder ein und versuchen, ihn zu färben.

1. Wenn der Grad von $v$ 3 oder weniger ist: $v$ hat höchstens 3 benachbarte Knoten. Daher wird mindestens eine der 4 Farben nicht für die benachbarten Knoten verwendet. Der Beweis ist abgeschlossen, wenn wir diese ungenutzte Farbe für $v$ verwenden.
2. Wenn der Grad von $v$ 4 ist: Angenommen, die 4 an $v$ angrenzenden Knoten (im Uhrzeigersinn $v_1, v_2, v_3, v_4$ genannt) sind alle mit unterschiedlichen Farben (Rot, Blau, Grün, Gelb) gefärbt. Betrachten wir nun den Teilgraphen, der durch Extrahieren nur der mit “Rot” und “Grün” gefärbten Knoten und der sie verbindenden Kanten aus dem gesamten Graphen entsteht. Wenn $v_1$ (Rot) und $v_3$ (Grün) innerhalb dieses rot-grünen Teilgraphen nicht verbunden sind (d.h. es gibt keinen Pfad von $v_1$ nach $v_3$, der nur aus roten und grünen Knoten besteht), können wir die Farben der zusammenhängenden Komponente, die $v_1$ enthält, vertauschen (Rot zu Grün, Grün zu Rot). Dies wird als “Umkehrung der Kempe-Kette” bezeichnet. Nach der Umkehrung wird $v_1$ grün, und die umgebenden Farben reduzieren sich auf drei: Blau, Grün, Grün und Gelb. Nun ist es möglich, $v$ rot zu färben. Wenn $v_1$ und $v_3$ verbunden sind, teilt der rot-grüne Pfad zwischen $v_1$ und $v_3$ aufgrund der topologischen Eigenschaften planarer Graphen (Jordanscher Kurvensatz) $v_2$ (Blau) und $v_4$ (Gelb). Daher können $v_2$ und $v_4$ absolut nicht durch eine blau-gelbe Kempe-Kette verbunden sein, und wir können die blau-gelbe Komponente umkehren, die $v_2$ enthält. In jedem Fall kann die Anzahl der Farben um $v$ auf 3 reduziert werden, sodass $v$ gefärbt werden kann.
3. Wenn der Grad von $v$ 5 ist: Betrachten wir den Fall, dass die 5 Knoten um $v$ herum, $v_1, v_2, v_3, v_4, v_5$, mit Rot, Blau, Grün, Gelb bzw. Rot gefärbt sind (da es 5 Knoten gibt, überschneidet sich eine Farbe). Kempe erweiterte das Argument für den Grad 4 und behauptete, dass durch die geschickte Kombination der Umkehrung zweier verschiedener Kempe-Ketten (z. B. einer rot-grünen Kette und einer rot-gelben Kette) die Farben um $v$ herum immer auf 3 oder weniger reduziert werden könnten. Sein Ansatz bestand in der doppelten Anwendung der Logik, dass, wenn die eine verbunden ist, die andere getrennt wird.

Dieser Beweis erschien intuitiv, elegant und frei von logischen Lücken. Die Mathematiker der damaligen Zeit zweifelten nicht daran, dass das Vier-Farben-Problem damit vollständig gelöst sei.

Heawoods Gegenbeispiel-Graph: Der fatale Fehler sich kreuzender “doppelter Kempe-Ketten”

Im Jahr 1890 las jedoch Percy John Heawood, ein damals 29-jähriger Mathematiker, Kempes Arbeit aufmerksam durch und entdeckte einen fatalen logischen Sprung in dem Argument bezüglich Knoten vom Grad 5.

Kempe hatte stillschweigend angenommen, dass bei der getrennten Umkehrung zweier Kempe-Ketten (z. B. einer blau-grünen Kette und einer blau-gelben Kette) diese unabhängig voneinander umkehrbar sind. Heawood bewies jedoch geometrisch und streng, dass, wenn diese beiden Ketten einige Knoten gemeinsam haben, die Umkehrung der ersten Kette den Färbungszustand des Graphen ändert, wodurch die Konnektivität der zweiten Kette verändert wird.

Heawood konstruierte einen konkreten Gegenbeispiel-Graphen (heute bekannt als “Heawood-Graph” oder dessen Ableitungen, ein maximal planarer Graph aus 25 Knoten). Es wurde gezeigt, dass, wenn man Kempes Algorithmus anwendet, um die Farben um den Knoten $v$ vom Grad 5 in diesem Graphen zu reduzieren, in dem Moment, in dem die blau-grüne Kette umgekehrt wird, die blau-gelbe Kette, die ursprünglich nicht verbunden war, verbunden wird, und wenn man anschließend die blau-gelbe Kette umkehrt, der zuvor umgekehrte grüne Knoten wieder zu seiner ursprünglichen Farbe zurückkehrt, was zu einer Schleife führt, in der die Anzahl der Farben nicht reduziert wird.

Kempes “gleichzeitiger Austausch von doppelten Kempe-Ketten” war ein Trugschluss, der aus der Unterschätzung der komplexen Verflechtungen planarer Graphen resultierte, bei denen lokale topologische Trennungsbeziehungen global nicht aufrechterhalten werden können. Mit dieser Entdeckung fiel Kempes Beweis des Vier-Farben-Satzes vollständig in sich zusammen.

Der vollständige mathematische Beweis des Fünf-Farben-Satzes

Kempes Beweis war zusammengebrochen, aber Heawood hatte ihn nicht nur zerstört. Er erkannte, dass Kempes Idee (Kempe-Kette) an sich äußerst nützlich war, und nutzte sie, um rigoros den “Fünf-Farben-Satz” (Five Color Theorem) zu beweisen, der besagt, dass “jeder planare Graph notwendigerweise mit 5 Farben gefärbt werden kann”. Der vollständige Beweisprozess für den Fünf-Farben-Satz lautet wie folgt:

Satz: Jeder planare Graph $G$ ist mit 5 Farben knotenfärbbar. Beweis: Wir verwenden vollständige Induktion über die Anzahl der Knoten $n$. Der Fall $n \leq 5$ ist trivial. Angenommen, alle planaren Graphen mit $n=k$ können mit 5 Farben gefärbt werden, wir betrachten einen planaren Graphen $G$ mit $n=k+1$. Aufgrund der aus der Eulerschen Formel abgeleiteten Tatsache gibt es in $G$ immer einen Knoten $v$ mit Grad 5 oder weniger. Da der Graph $G' = G - \{v\}$, der durch Entfernen von $v$ aus $G$ entsteht, $k$ Knoten hat, kann er gemäß der Induktionsvoraussetzung mit 5 Farben (Farbe 1, Farbe 2, Farbe 3, Farbe 4, Farbe 5) gefärbt werden. Betrachten wir die Rückgabe von $v$, während die Färbung von $G'$ erhalten bleibt.

• Fall 1: $\deg(v) < 5$. Da $v$ höchstens 4 benachbarte Knoten hat, wird mindestens eine der 5 Farben nicht für die benachbarten Knoten verwendet. Diese Farbe kann für $v$ verwendet werden.
• Fall 2: $\deg(v) = 5$. Angenommen, die 5 an $v$ angrenzenden Knoten $v_1, v_2, v_3, v_4, v_5$ (im Uhrzeigersinn angeordnet) sind alle mit unterschiedlichen Farben (in der Reihenfolge Farbe 1, Farbe 2, Farbe 3, Farbe 4, Farbe 5) gefärbt. (Wenn dieselbe Farbe mehr als einmal verwendet wird, bleibt mindestens eine ungenutzte Farbe übrig, mit der $v$ gefärbt werden kann). Hier betrachten wir im Graphen $G'$ den induzierten Teilgraphen, der nur aus Knoten besteht, die mit Farbe 1 und Farbe 3 gefärbt sind, und sei die zusammenhängende Komponente, die $v_1$ enthält, $C_{13}$ (dies ist eine Kempe-Kette).
  • Unterfall 2a: $v_3 \notin C_{13}$. Das heißt, es gibt keinen Pfad von $v_1$ nach $v_3$, der nur durch Knoten der Farbe 1 und Farbe 3 führt. In diesem Fall bleibt die Gültigkeit der Färbung erhalten, selbst wenn die Farben aller Knoten in $C_{13}$ vertauscht werden (Farbe 1 $\leftrightarrow$ Farbe 3). Nach der Umkehrung ist $v_1$ Farbe 3 und $v_3$ ist ebenfalls Farbe 3, sodass es keine Farbe 1 mehr um $v$ gibt. Daher kann $v$ mit Farbe 1 gefärbt werden.
  • Unterfall 2b: $v_3 \in C_{13}$. Das heißt, es existiert ein Pfad $P_{13}$ bestehend aus Knoten der Farbe 1 und Farbe 3, der $v_1$ und $v_3$ verbindet. Dieser Pfad $P_{13}$ bildet zusammen mit dem Knoten $v$ und den Kanten $(v, v_1), (v, v_3)$ eine geschlossene Kurve (Kreis) auf der Ebene. Aufgrund der Eigenschaften planarer Graphen (Jordanscher Kurvensatz) teilt dieser Kreis die Ebene in eine Innenseite und eine Außenseite. Die Knoten $v_2$ und $v_4$ befinden sich auf verschiedenen Seiten dieses Kreises (einer innen, der andere außen). Betrachten wir nun die Kempe-Kette $C_{24}$, die aus Knoten besteht, die mit Farbe 2 und Farbe 4 gefärbt sind. Angenommen, $v_2$ und $v_4$ wären durch diese Kette verbunden, dann müsste ein Pfad $P_{24}$ existieren, der $v_2$ und $v_4$ verbindet. $P_{24}$ muss jedoch kreuzungsfrei auf dem planaren Graphen verlaufen und kann den durch $P_{13}$ gebildeten Kreis nicht überqueren (was der Definition eines planaren Graphen widersprechen würde). Daher existiert ein Pfad der Farbe 2 und Farbe 4, der $v_2$ und $v_4$ verbindet, absolut nicht. Das heißt, die Kempe-Kette $C_{24}$ der Farbe 2 und Farbe 4, die $v_2$ enthält, schließt $v_4$ nicht ein. Wenn wir also die Farben innerhalb von $C_{24}$ umkehren (Farbe 2 $\leftrightarrow$ Farbe 4), wird $v_2$ zu Farbe 4, und Farbe 2 verschwindet aus der Umgebung von $v$. Schließlich kann $v$ mit Farbe 2 gefärbt werden.

Auf diese Weise kann $v$ in jedem Fall gefärbt werden, und der Fünf-Farben-Satz ist durch vollständige Induktion vollständig bewiesen. $\blacksquare$

Dieser Beweis macht auf wunderschöne Weise Gebrauch von der Topologie planarer Graphen (Jordanscher Kurvensatz) und zeigt, wie robust Kempes Konzept der “Kempe-Kette” bei der Anwendung auf einzelne, nicht kreuzende Ketten ist. Der Weg zu “vier Farben” wird von hier aus jedoch in ein unermessliches Meer von Berechnungen übergehen, über die neuen Paradigmen der “Reduzibilität” und der “unvermeidbaren Mengen”.

Kapitel 3: Die Mathematik der Entladungsmethode (Discharging Method) und die Ableitung unvermeidbarer Konfigurationen

Nach Heawood begannen Mathematiker zu erforschen, welche Struktur ein “minimales Gegenbeispiel” (Minimum Counterexample) haben sollte (oder nicht haben sollte), falls ein solches existiert, das nicht mit vier Farben gefärbt werden kann. Hier werden zwei mächtige Konzepte wichtig: “reduzible Konfigurationen” (Reducible Configuration) und “unvermeidbare Mengen” (Unavoidable Set).

Reduzibilität (Reducibility)

Eine reduzible Konfiguration ist ein lokales Teilarrangement (Muster) von Knoten, das “absolut nicht in dem Graphen existieren kann, wenn der gesamte Graph nicht mit vier Farben gefärbt werden kann (d.h. ein minimales Gegenbeispiel ist)”. Beispielsweise sind “Knoten mit Grad 3 oder weniger” oder “Knoten mit Grad 4” reduzible Konfigurationen. Denn wie zuvor erwähnt, würde ihre Existenz es ermöglichen, das Problem durch Reduktion mittels Kempe-Ketten auf einen kleineren Graphen zurückzuführen (zu reduzieren), was im Widerspruch zu der Annahme stünde, dass es sich um ein “minimales Gegenbeispiel” handelt. Im Jahr 1913 bewies George David Birkhoff, dass eine bestimmte Konfiguration aus 6 Knoten, der sogenannte “Birkhoff-Diamant” (Birkhoff’s diamond), ebenfalls reduzibel ist. Die Entdeckung reduzibler Konfigurationen schritt voran, aber ein Beweis konnte erst erbracht werden, wenn garantiert war, dass diese “notwendigerweise in jedem Graphen existieren”.

Die mathematische Struktur der Entladungsmethode (Discharging Method)

Die endgültige Strategie zum Beweis des Vier-Farben-Satzes läuft darauf hinaus, “eine unvermeidbare Menge zu finden, die vollständig aus reduziblen Konfigurationen besteht”. Eine unvermeidbare Menge ist eine Liste von Konfigurationen, bei der “jeder planare Graph (genauer gesagt, jeder maximal planare Graph) notwendigerweise mindestens eine Konfiguration aus dieser Menge enthalten muss”.

Ein äußerst mächtiges Werkzeug zum Aufbau und Beweis dieser unvermeidbaren Menge ist die “Entladungsmethode” (Discharging Method), die von Heinrich Heesch verfeinert wurde. Die Entladungsmethode ist eine geradezu magische Technik zum Beweis von Struktursätzen in der Graphentheorie und nutzt das Konzept der elektrischen Ladung aus dem Elektromagnetismus als Analogie.

Der mathematische Prozess der Entladungsmethode lautet wie folgt:

1. $$ch(v) = 6 - \deg(v)$$

   Aufgrund der aus der Eulerschen Formel abgeleiteten Gleichung $\sum_{v} (6 - \deg(v)) = 12$ beträgt die Summe der Anfangsladungen des gesamten Graphen exakt 12 (ein positiver Wert). Hier hat ein Knoten vom Grad 5 die Ladung $+1$, ein Knoten vom Grad 6 die Ladung $0$ und Knoten vom Grad 7 oder höher eine negative Ladung. (Da wir annehmen können, dass in einem minimalen Gegenbeispiel keine Knoten vom Grad 4 oder weniger existieren, betrachten wir 5 als Minimalgrad).

2. Definition der Entladungsregeln (Discharging Rules): Als Nächstes definieren wir Regeln, um Ladungen zwischen benachbarten Knoten zu verschieben. Die Grundidee ist, “Ladung von Knoten mit positiver Ladung (d. h. Knoten vom Grad 5) zu Knoten mit negativer Ladung (Knoten mit hohem Grad ab 7) fließen zu lassen (zu entladen)”. Beispielsweise werden Dutzende oder Hunderte detaillierter Regeln aufgestellt, wie “Wenn ein Knoten $v$ vom Grad 5 an einen Knoten $u$ vom Grad 7 angrenzt, übertrage eine Ladung von $\frac{1}{5}$ von $v$ nach $u$”.

3. $$ \sum_{v \in V} ch'(v) = 12 > 0 $$

   ($ch'(v)$ ist die Ladung des Knotens $v$ nach der Verschiebung) Dass die Gesamtsumme positiv ist, bedeutet, “dass auch nach der Ladungsverschiebung mindestens ein Knoten mit positiver Ladung existieren muss”.

   Hier analysieren wir die Endladung $ch'(v)$ jedes Knotens basierend auf seiner lokalen Struktur (dem Muster der Grade dieses Knotens und seiner Nachbarknoten). Wenn wir beweisen können, dass “ein Knoten, der eine bestimmte Konfiguration nicht aufweist, unter den festgelegten Entladungsregeln immer eine Endladung von null oder weniger haben wird”, dann bedeutet eine positive Endladung, dass diese “bestimmte Konfiguration” notwendigerweise irgendwo im Graphen existieren muss. Auf diese Weise entsteht die “unvermeidbare Menge”, indem alle Muster von lokalen Konfigurationen, die zu einer positiven Endladung führen können, erschöpfend aufgelistet werden.

Heesch war davon überzeugt, dass durch die Anwendung dieser Entladungsmethode eine unvermeidbare Menge aus einer endlichen Anzahl (wahrscheinlich Tausenden) von reduziblen Konfigurationen konstruiert werden könnte. Die Rechenkomplexität zur Bestimmung, ob eine bestimmte Konfiguration “reduzibel” ist, explodiert jedoch exponentiell in Bezug auf die Länge der Grenze. Eine manuelle Überprüfung der Reduzibilität von Tausenden von Konfigurationen war für Menschen selbst in einem ganzen Leben unmöglich.

Kapitel 4: 1976, der computergestützte Verifikationsalgorithmus von Appel und Haken

Definition von D-Reduzibilität und C-Reduzibilität

In den 1970er Jahren starteten Kenneth Appel und Wolfgang Haken von der University of Illinois ein historisches Projekt, das Heeschs Entladungsmethode mit der Rechenleistung von Computern verschmolz.

Die rechenintensivste Aufgabe, die sie in Angriff nahmen, war die “Reduzibilitätsprüfung” von Konfigurationen. Es gibt hauptsächlich zwei Arten von Reduzibilität:

• D-Reduzibilität (D-reducibility / Direct reducibility): Wenn für alle möglichen 4-Färbungsmuster der die Konfiguration umgebenden ringförmigen Grenze (Ring) gezeigt werden kann, dass sich diese auch in das Innere der Konfiguration fortsetzen lassen, oder durch Umkehren der Kempe-Ketten der Grenzfarben in ein nach innen fortsetzbares Muster umgewandelt werden können. Wenn dies bestätigt wird, kann sofort gesagt werden, dass die Konfiguration nicht im minimalen Gegenbeispiel enthalten ist.
• C-Reduzibilität (C-reducibility / Contracting reducibility): Eine Methode, bei der, wenn Muster existieren, die bei der D-Reduzibilitätsprüfung durchfallen, ein kleinerer Graph betrachtet wird, in dem ein Teil der Konfiguration “kontrahiert” (mehrere Knoten werden zu einem verschmolzen) ist. Wenn dieser kontrahierte Graph 4-färbbar ist, zeigt dies, dass der ursprüngliche Graph ebenfalls 4-färbbar ist.

Algorithmus zur Bestimmung der Färbbarkeit der Ringgrenze

Dem Computer (IBM 360) wurde die Ausführung des Algorithmus zur Prüfung der D- und C-Reduzibilität für eine enorme Anzahl von Konfigurationskandidaten anvertraut.

Angenommen, eine Konfiguration $C$ hat einen Grenzring $R$ (der Länge $k$). Es gibt maximal $4^k$ Kombinationen, um die Knoten auf dem Ring mit 4 Farben zu färben, was selbst unter Berücksichtigung von Symmetrien eine enorme Zahl ist. Bei einer Ringlänge von $k=14$ müssen beispielsweise etwa 200.000 Grenzchromatizitätsvaliditäten überprüft werden. Der Algorithmus läuft in folgenden Schritten ab:

1. Generiere die Menge aller gültigen 4-Färbungsmuster für den Grenzring $R$.
2. Teste alle möglichen Möglichkeiten, das Innere der Konfiguration $C$ tatsächlich mit 4 Farben zu färben, und zeichne auf, mit welchen Grenzmustern sie konsistent sind (nach innen erweiterbar).
3. Für Grenzmuster, die nicht nach innen erweiterbar sind, simuliere Umkehrungen von Kempe-Ketten. Wenn ein Muster durch Umkehrung in ein Muster überführt werden kann, das bereits als “nach innen erweiterbar” bekannt ist, wird dieses anfängliche Muster ebenfalls als “gelöst” markiert.
4. Wiederhole diese Suche nach Umkehrungsübergängen. Wenn alle Grenzmuster gelöst werden können, wird bestimmt, dass die Konfiguration $C$ “D-reduzibel” ist.

Da die Rechenzeit bei größeren Grenzlängen explodiert, beschränkten Appel und Haken die Konfigurationen auf eine maximale Ringlänge von 14 und passten die Entladungsregeln zum Aufbau einer unvermeidbaren Menge rigoros an. Dieser Anpassungsprozess selbst war eine kontinuierliche gigantische Versuch-und-Irrtum-Schleife zwischen Mensch und Computer. Ein interaktiver Prozess – “der Mensch korrigiert die Entladungsregeln, der Computer spuckt Kandidaten für unvermeidbare Mengen aus, testet die Reduzibilität, der Mensch betrachtet die fehlgeschlagenen Konfigurationen und korrigiert die Regeln erneut” – wurde mehrere Jahre lang fortgesetzt.

1200 Stunden Berechnung und “Q.E.D.”

1976 entdeckten sie schließlich eine unvermeidbare Menge bestehend aus 1.936 Konfigurationen, die aus fein abgestimmten Entladungsregeln abgeleitet wurde. Und nachdem sie den Großrechner der University of Illinois über 1200 Stunden laufen ließen, bestätigte der Computer, dass alle diese 1.936 Konfigurationen entweder D-reduzibel oder C-reduzibel sind.

Sie schrieben kurz in der Zusammenfassung ihres Papiers: “Every planar map is four colorable.”

Der Poststempel des Fachbereichs Mathematik der University of Illinois erhielt stolz den Aufdruck “FOUR COLORS SUFFICE” (4 Farben reichen aus). Dies war ein monumentales Ereignis in der Geschichte der Mathematik, bei dem erstmals ein Computer einen zentralen deduktiven Schritt im Beweis eines Theorems übernahm.

Kapitel 5: Erschütterung der mathematischen Welt und die Philosophie des “Beweises”

Die Ankündigung von Appel und Haken löste in der mathematischen Welt weniger Freude als vielmehr tiefe Verwirrung und heftige Debatten aus.

Ist ein für den Menschen unlesbarer Beweis Mathematik?

In der von der griechischen Antike geprägten mathematischen Tradition war ein “Beweis” etwas, bei dem menschliche Mathematiker logische Schritte nacheinander nachvollziehen, ihre Richtigkeit aus tiefstem Herzen verstehen und akzeptieren konnten. Man glaubte, dass der Beweisprozess eine tiefe Einsicht darüber, “warum der Satz gilt”, und die Schönheit der Struktur in sich barg.

Der Beweis des Vier-Farben-Satzes war jedoch von anderer Art. Das Papier enthielt nur eine Liste der 1.936 Konfigurationen und eine Beschreibung des Computeralgorithmus. Die tatsächliche Aufzeichnung (Trace) der Reduzibilitätsprüfungen war so riesig, dass es schwierig war, sie auch nur auf Papier zu drucken. Für noch so geniale Mathematiker war es unmöglich, die Berechnungen ihr ganzes Leben lang manuell nachzuvollziehen und sicherzustellen, dass keine logischen Mängel vorliegen.

Es entstand eine beispiellose Situation: “Um zu glauben, dass der Beweis korrekt ist, muss man glauben, dass die Hardware des Computers nicht versagt hat und dass das von Appel und Haken in Assemblersprache geschriebene Programm keine Fehler enthält.”

Der Wissenschaftsphilosoph Thomas Tymoczko kritisierte, dass dieser Beweis die Mathematik von der apriorischen Suche nach Wahrheit zu etwas Empirischem und Experimentellem wie der Physik degradiert habe. Die Definition der Handlung des “Beweisens” selbst befand sich in einer epistemologischen Krise.

Gegenargumente und Vereinfachung durch RSST

Appel und Haken entgegneten auf die Kritik: “Nur schöne Beweise sind keine Mathematik. Es gibt von Natur aus komplexe Probleme, die riesige Fallunterscheidungen erfordern, und wenn diese die Grenzen des menschlichen Gehirns überschreiten, ist die Zuhilfenahme von Maschinen eine unvermeidliche Evolution.”

Um diesen Schleier zu lüften, versuchten viele Mathematiker, den Beweis zu vereinfachen und neu zu überprüfen. Im Jahr 1997 veröffentlichten Neil Robertson, Daniel P. Sanders, Paul Seymour und Robin Thomas (allgemein bekannt als RSST) einen neuen Beweis, der die Entladungsmethode systematischer und für den Menschen leichter überprüfbar machte und die Größe der unvermeidbaren Menge von 1.936 auf 633 Konfigurationen reduzierte. Es war ein raffinierter Algorithmus, dessen Berechnung in nur wenigen Stunden abgeschlossen war.

Es bleibt jedoch dabei, dass dies immer noch von der “computergestützten Reduzibilitätsberechnung” abhängt. Ein “schöner Beweis mit Papier und Stift”, den die menschliche Intuition vollständig erfassen kann, wurde noch nicht gefunden (und viele Graphentheoretiker glauben, dass ein solcher Beweis prinzipiell nicht existieren wird).

Kapitel 6: Georges Gonthiers vollständiger formaler Beweis mit Coq

Wie kann man mathematisch vollständig die Angst beseitigen, dass “das Programm Fehler enthalten könnte”? Die ultimative Antwort darauf ist die vollständige Formalisierung (Formalization) unter Verwendung eines “Beweisassistenten” (Proof Assistant).

Im Jahr 2005 gelang es Georges Gonthier vom französischen Nationalen Institut für Forschung in Informatik und Automatik (INRIA) und Microsoft Research zusammen mit Benjamin Werner, den Beweis des Vier-Farben-Satzes mithilfe des Beweisassistenten “Coq” von Grund auf vollständig zu formalisieren.

Formalisierung von hyperplanaren Karten (Hypermap) und kombinatorischer Topologie

Coq ist ein System, das von mathematischen Axiomen ausgeht und Beweise gemäß einem strengen System logischer Regeln (Calculus of Inductive Constructions) beschreibt und maschinell überprüft.

Gonthiers größte Errungenschaft bestand darin, das intuitive und geometrische Objekt eines planaren Graphen in eine vollständige algebraische und kombinatorische Struktur zu übersetzen, die von einem Computer verarbeitet werden kann. Er definierte eine Datenstruktur namens “Hypermap” (hyperplanare Karte), um die Beziehungen zwischen Knoten, Kanten und Flächen in einem Graphen auszudrücken. Dies ist eine Methode, Graphen als Mengen von “Darts” (Halbkanten) und als Permutationsgruppen über diese darzustellen. Dadurch wurden topologische Theoreme wie die Eulersche Formel und der Jordansche Kurvensatz vollständig als formale Logik aus Gruppentheorie und endlichen Mengen formalisiert.

Beweis der Korrektheit des Beweisprogramms selbst

Ferner warf Gonthier die “in C-Sprache geschriebenen Verifikationsprogramme” weg, die von Appel-Haken und RSST verwendet wurden, und implementierte den Algorithmus zur Bestimmung der Reduzibilität selbst unter Verwendung der internen Sprache von Coq (Gallina). Und dann bewies er mathematisch in Coq die Korrektheit des Algorithmus selbst: “Wenn dieser Bestimmungsalgorithmus ‘True’ ausgibt, ist diese Konfiguration wirklich reduzibel.”

Dies hat die Zuverlässigkeit des Beweises entscheidend verändert. Man muss sich keine Sorgen mehr über “Fehler im Algorithmus” machen. Solange der als Kernstück von Coq fungierende Logikprüfungs-Kernel (ein extrem einfacher, ausgereifter Code von einigen hundert Zeilen, implementiert mithilfe von De-Bruijn-Indizes usw.) die logischen Inferenzregeln korrekt verarbeitet, ist mathematisch garantiert, dass der riesige Beweisbaum, den Gonthier konstruiert hat, absolut korrekt ist.

Dies ist ein neuer Höhepunkt für “Beweise” in der Mathematik. Es ist eine Evolution vom “Beweis, den ein Mensch liest und versteht (Informal Proof)” hin zum “formalen Beweis (Formal Proof), bei dem eine Maschine logische Vollständigkeit garantiert”. Der Vier-Farben-Satz wurde das erste nichttriviale große Theorem in der Geschichte, das dieses Höchstmaß an Strenge erreichte.

Kapitel 7: Das 4-Farben-Problem planarer Graphen und das Paradoxon der NP-Vollständigkeit

Lassen Sie uns zum Schluss den Vier-Farben-Satz aus der Perspektive der rechnerischen Komplexitätstheorie (Computational Complexity Theory) betrachten. Hier gibt es ein höchst faszinierendes, geradezu paradoxes Phänomen.

Das Färbungsproblem in allgemeinen Graphen (das Problem zu bestimmen, ob ein gegebener Graph mit $k$ Farben gefärbt werden kann) ist eines der berühmtesten “NP-vollständigen” (NP-complete) Probleme in der Informatik. Insbesondere ist bewiesen, dass das “3-Färbungsproblem in planaren Graphen” (Planar 3-Colorability) NP-vollständig ist. Das bedeutet, dass man annimmt, dass es keinen Algorithmus gibt, der in Polynomialzeit entscheidet, ob ein planarer Graph mit 3 Farben gefärbt werden kann, es sei denn, $\text{P} = \text{NP}$.

Wie sieht es also mit dem “4-Färbungsproblem in planaren Graphen” (Planar 4-Colorability) aus? Intuitiv könnte man denken, dass, wenn 3 Farben NP-vollständig sind, 4 Farben ebenso schwierig (NP-vollständig) sein müssten.

Überraschenderweise ist die Berechnungskomplexität des 4-Färbungsproblems in planaren Graphen (Entscheidungsproblem) $O(1)$, was bedeutet “konstante Zeit (trivial)”. Weil der Vier-Farben-Satz garantiert, dass “alle planaren Graphen mit 4 Farben gefärbt werden können”, gibt der Algorithmus einfach immer “Ja” aus, ohne sich den Eingabegraphen überhaupt anzusehen, und hat stets zu 100% recht. Dies ist ein wunderschönes Beispiel dafür, wie die mächtige Existenzgarantie eines Theorems die Komplexität eines Entscheidungsproblems auf ein absolutes Minimum reduziert.

Dies betrifft jedoch nur das Entscheidungsproblem (Decision Problem), “ob es gefärbt werden kann”. Einen Färbungsalgorithmus (Search Problem) zu konstruieren, “wie man es tatsächlich mit 4 Farben färbt”, ist eine ganz andere Geschichte. Wenn man das Beweisverfahren von Appel-Haken oder RSST als Algorithmus implementiert, erhält man einen Algorithmus, der für einen gegebenen planaren Graphen mit $N$ Knoten tatsächlich eine 4-Färbung finden kann. Es wurde gezeigt, dass ein auf dem RSST-Beweis basierender Algorithmus eine 4-Färbung in Polynomialzeit mit einer Worst-Case-Komplexität von $O(N^2)$ ausgibt.

Mit anderen Worten: Während der Versuch, einen planaren Graphen mit 3 Farben zu färben, eine Zeit erfordern könnte, die der Lebensdauer des Universums entspricht (NP-vollständig), führt die Zugabe der vierten Farbe dank der mathematischen Struktur hinter dem Vier-Farben-Satz zur Existenz eines schnellen (nämlich in $O(N^2)$) Algorithmus. Es ist eine zutiefst mysteriöse und faszinierende Tatsache an der Schnittstelle von Mathematik und Informatik.

Fazit: Das Vermächtnis des Vier-Farben-Satzes

Das einfache Kartenfärbungsproblem eines englischen jungen Mannes aus dem Jahr 1852 begann als bloßes Rätsel. Aber es eröffnete im Laufe von mehr als einem Jahrhundert ein riesiges neues mathematisches Feld namens Graphentheorie, entwickelte die Algorithmentheorie weiter und konfrontierte die Menschheit schließlich mit den grundlegenden philosophischen Fragen: “Können Computer mathematische Beweise erbringen?” und “Was ist mathematische Wahrheit?”.

Die Geschichte des Vier-Farben-Satzes ist eine Geschichte der intensiven Schnittmenge zwischen den Grenzen der menschlichen Intuition und den Möglichkeiten einer neuen logischen Maschine. Heute werden andere massive und schwierige Probleme wie die Kepler-Vermutung (2014, Flyspeck-Projekt von Thomas Hales) und der Satz von Feit-Thompson ebenfalls vollständig durch formale Verifikation unter Verwendung von Beweisassistenten bewiesen.

Wenn wir heute eine Karte beiläufig mit vier Farben kolorieren, verbergen sich darin Schicht um Schicht die Ästhetik von Eulers Polyedern, Kempes genialer Rückschlag, Heawoods strenge Widerlegung, die Mathematik von Heeschs Entladung, die Spuren von Tausenden von Stunden blinkender Supercomputer-Berechnungen und die Logik von Coqs hyperplanaren Karten. Der Vier-Farben-Satz wird zweifellos als bestes Fallbeispiel dafür in Erinnerung bleiben, wie die Mathematik sich über die Grenzen des menschlichen Denkens hinaus ausdehnt.