Zahlen, bitte! Als der Computer den Vier-Farben-Satz bewies

Nach der Veröffentlichung von mehr als 370 „Resultatfamilien“ durch OpenAI stellen bekannte Mathematiker die Sinnfrage: Wie weit ist KI-gestützte Mathematik noch Mathematik? Was ist von einem Beweis zu halten, der von einem LLM geführt wurde und schwer verständlich ist?

In dieser Rubrik stellen wir immer dienstags verblüffende, beeindruckende, informative und witzige Zahlen aus den Bereichen IT, Wissenschaft, Kunst, Wirtschaft, Politik und natürlich der Mathematik vor.

• Alle Artikel zu "Zahlen, bitte!"

Diese Fragen sind nicht neu. Vor 50 Jahren veröffentlichten Wolfgang Haken und Kenneth Appel ihren Beweis für das Vierfarben-Theorem. Es besagt, dass vier Farben ausreichen, eine beliebige Landkarte so zu färben, dass keine Länder mit gemeinsamen Grenzen die gleiche Farbe haben. Den Beweis hatten IBM-Großrechner vom Typ 360-75, 370-158 und 370-168   in 1200 Stunden Rechenzeit durchgeführt. Auch für die Prüfung des Beweises wurde ein unabhängiges Computerprogramm genutzt.

Vier Jahre Arbeit am Theorem

An ihrem Beweis des Vierfarben-Theorems hatten die beiden Mathematiker von der Universität von Illinois in Urbana-Champaign vier Jahre lang gearbeitet. Sie setzten eine Beweisführung fort, die eine lange Tradition hatte. Denn das Vierfarben-Theorem geht auf eine Vermutung zurück, die der Mathematiker Francis Guthrie 1852 aufstellte, als er eine Karte der englischen Grafschaften färben wollte. 1878 stellte der Mathematiker Arthur Cayley die Vermutung in einer Sitzung der London Mathematical Society vor.

An ihr nahm der Rechtsanwalt Alfred Kempe teil, der ein Jahr später einen Beweis ablieferte. Wie Haken und Appel in ihrem Aufsatz zum Vierfarben-Theorem ausführten, nahm Kempe das Gegenteil der Vermutung und zeigte, dass sie in einem Widerspruch endete. Es dauerte elf Jahre, bis dieser Beweis widerlegt wurde, doch Kempes Ansatz, die sogenannte Theorie der Kempe-Ketten, gab den folgenden Mathematikern die Richtung vor.

Im Jahr 1922 bewiesen Mathematiker, dass jede Landkarte mit 25 oder weniger Ländern mit vier Farben koloriert werden kann. Zehn Jahre später war man mit dem Beweis bei 96 Ländern angelangt -- und legte die Vermutung beiseite, als der Unvollständigkeitssatz von Kurt Gödel die Mathematik erschütterte. Wayne interessiert es eigentlich, ob vier, sechs oder zwei Farben nötig sind?

Deutscher Wissenschaftler mit Idee zum Theorem-Programm

1936 begann der Mathematiker Heinrich Heesch sich mit dem Vierfarben-Theorem zu beschäftigen. Seine Weigerung, dem Nationalsozialistischen Deutschen Dozentenbund beizutreten, hatte seine Universitätslaufbahn beendet und so beschäftigte er sich als Privatmann mit der Zahl möglicher Karten und Knoten, die untersucht werden mussten. Er schätzte sie auf rund 10.000 Konfigurationen. Nach dem Krieg hielt er Vorträge zu diesem Thema und entwickelte als Professor an der Technischen Hochschule Hannover mit dem Mathematiker Karl Dürre die Idee zu einem Computerprogramm, das die möglichen Kombinationen prüft.

Heesch reiste mehrfach in die USA, da die zu der Zeit in Deutschland verfügbaren Computer für sein Vorhaben nicht leistungsfähig genug waren, und arbeitete dort mit den Mathematikern Wolfgang Haken und Yoshio Shimamoto zusammen. Letzterer publizierte 1971 einen Ansatz mit einem Computerprogramm, das allerdings fehlerhaft war.

Der Beweis, den Haken und Appel 1976 schließlich vorstellten, war komplex. 1482 Konfigurationen mussten von einem Computer durchgerechnet werden, wofür im Schnitt weniger als eine Stunde Rechenzeit pro Konfiguration nötig war. Die Gutachter, die vor der Veröffentlichung den Beweis prüfen sollten, griffen selbst zum Computer. „Als wir unsere Arbeit über den Beweis beim Illinois Journal of Mathematics einreichten, überprüften die Gutachter das Entladungs-Verfahren anhand unserer vollständigen Unterlagen, während sie die Berechnungen zur Reduzierbarkeit [der zu untersuchenden 1482 Konfigurationen] durch den Einsatz eines unabhängigen Computerprogramms verifizierten“, so Haken und Appel in ihrem Rückblick.

Viel Kritik an computergestützter Beweisführung

Auf die erste Veröffentlichung des Beweises folgte ein Sturm der Entrüstung. „Die computergestützten Tricksereien von Appel und Haken in den Bereich der Mathematik aufzunehmen, würde uns nur intellektuell unbefriedigt zurücklassen“, so Daniel Cohen vom Hunter College in New York. „Das ist kein Beweis, das ist nicht einmal der Ansatz eines Beweises. Es ist der lächerlichste Fall von ‚Des Kaisers neue Kleider‘, der jemals in der Geschichte der Mathematik aufgetaucht ist und diese in Misskredit gebracht hat“, donnerte George Spencer-Brown von der Universität Cambridge. „Gott würde nicht zulassen, dass der Satz durch eine derart schreckliche Methode bewiesen wird!“, so der Kombinatoriker Herbert Wilf von der Universität von Pennsylvania.

Andere Kritiken waren „EDV-technischer“ Natur, wie das seinerzeit genannt wurde: Was ist, wenn der Compiler oder das Betriebssystem eines Computers fehlerhaft sind, wenn sie den Beweis durchrechnen? Auch außerhalb der Zunft gab es harsche Reaktionen. Die Wissenschaftsredaktion der New York Times weigerte sich, einen Text über den Beweis zu veröffentlichen. Im Journal of Philosophy schrieb der Philosoph Thomas Tymoczko: „Kein Mathematiker hat einen Beweis für das Vierfarbenproblem gesehen, und ebenso wenig hat jemand einen Beweis dafür gesehen, dass es überhaupt einen Beweis dafür gibt.

Zudem ist es höchst unwahrscheinlich, dass jemals ein Mathematiker einen Beweis für das Vierfarbenproblem zu Gesicht bekommen wird.“ Auf seine Weise brachte Tymoczko den Problemfall auf den Punkt: Ein formal schlüssiger Beweis, den Menschen nicht überblicken können, lässt sich Schritt für Schritt nicht auf seine logische Folgerichtigkeit prüfen.

Der heftige Widerstand führte dazu, dass Haken und Appel 1989 ein Buch mit einer ausführlicheren Beweisführung veröffentlichten, das auch die zuvor nur auf Mikrofiche erschienenen Ergänzungen enthielt. In seinem Buch „Four Colours Suffice“ berichtet der Mathematikhistoriker Robin Wilson davon, dass die Ablehnung oder Akzeptanz des Beweises ziemlich genau eine Frage des Alters war. Mathematiker unter 40 akzeptierten die computerisierte Lösung des Vierfarben-Theorems, die über 40 lehnten sie ab. Eine große Ausnahme von dieser Regel war der 1917 geborene britische Kryptologe und Mathematiker Bill Tutte, der selbst einen Ansatz zum Vierfarben-Theorem vorgelegt hatte.

Er dichtete 1976 zur Feier des Beweises: „Wolfgang Haken Smote the Kraken One! Two! Three! Four! Quoth he: The monster is no more.“

Computertechnik als Beweisassistent

Weitsichtig fügte Tutte hinzu, dass die anderen Mathematiker, die an dem Problem gearbeitet hatten, sich verzweifelt die Haare raufen und sich die Frage stellen dürften: „Was sollen wir bloß jetzt tun?“ Seine Antwort: „Bleibe guten Mutes! Du kannst weiter forschen. Du kannst dich mit den Vermutungen von Hajós und Hadwiger befassen.“ Man kann hinzufügen, dass das Monster später auch mit anderen Methoden gezähmt wurde. 1996 vereinfachten Neil Robertson, Daniel Sanders, Paul Seymour und Robin Thomas den Beweis auf 633 Konfigurationen. Im Jahr 2005 schloss Georges Gonthier eine vollständige Formalisierung des Beweises im Beweisassistenten Coq ab. Der schrieb: „Die übrigen rund 60.000 Zeilen des Beweises lassen sich zwar zur Gewinnung von Erkenntnissen oder sogar zur Unterhaltung lesen, müssen aber nicht auf ihre Korrektheit hin überprüft werden. Das ist die Aufgabe des Beweisassistenten Coq – eine Aufgabe für Computer.“

Mit der Veröffentlichung von hunderten KI-generierten Lösungen durch OpenAI stellt sich die Frage auf einem neuen Niveau. In einem langen Artikel beschreibt die New York Times, wie Terence Tao, 2006 mit der Fields-Medaille ausgezeichnet, vom begeisterten Nutzer der KI zum scharfen Kritiker des Vorgehens von OpenAI wurde und nun seine Doktoranden in Treffen betreut, die laut Tao zunehmend Therapiesitzungen gleichen. Ein Bericht von Harvard-Mathematikern empfiehlt, Doktorgrade künftig weniger nach dem Text der Dissertation und stärker nach einer gründlichen mündlichen Verteidigung zu vergeben.

Ähnlich wie Bill Tutte vor fast 50 Jahren bleibt Tao tapfer optimistisch und guten Mutes, weil es viele offene Probleme an den Grenzen der Mathematik gibt. „Dies ist eine Zeit für Kreativität, und ich hoffe sehr, dass die Studierenden sich dieser Herausforderung stellen. Sie haben nicht darum gebeten. Doch ich glaube, viele von ihnen werden uns überraschen.“ Schließen wir mit einem weiteren Gedicht von Tutte:

„The Four Colour Theorem is the tip of the iceberg,
the thin end of the wedge
and the first cuckoo of spring.“