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 ausgefü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 370-158 und 370-168 in 1200 Stunden Rechenzeit durchgeführt. Auch für die Prüfung des Beweises wurde ein (anderer) Computer genutzt.
Die Länder der Welt eingeteilt in vier Farben: Eingefärbt gemäß dem Vier-Farben-Satz.
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.
Der südafrikanische Mathematiker und Botaniker Francis Guthrie (* 22. Januar 1831 in London; † 19. Oktober 1899 in Claremont, Kapstadt) kam 1852 bei Kartierungsarbeiten zu der Vermutung des Vier-Farben-Satzes.
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 Deutschen Dozentenbund der Nationalsozialisten 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 Programmierer 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 ansässigen 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 veröffentlichten, war komplex. 1482 Konfigurationen mussten von einem Computer durchgerechnet werden, wofür 6400 Minuten Rechenzeit pro Konfiguration veranschlagt wurden. 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. „Wenn diese computergestützten Tricksereien von Appel und Haken in den Kanon der Mathematik aufgenommen werden, ist das eine intellektuelle Bankrotterklärung“, 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 [PDF]: 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 dürften und sich die Frage stellen: „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 Jahre 2008 überprüfte der Beweisassistent Coq den Beweis für Georges Gonthier. 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 (Fields-Preisträger 2006) vom anfänglichen Nutzer der KI zum Skeptiker 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.“
