// HEISE ONLINE — INTELLIGENZA ARTIFICIALE
Zahlen, bitte! Als der Computer den Vier-Farben-Satz bewies
Die Diskussion um KI-Beweise für mathematische Probleme ist nicht neu. Bereits der erste IT-gestützte Beweis 50 Jahre zuvor zog Forscher-Unmut auf sich.
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.
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.
(Bild: Fibonacci, CC BY-SA 3.0, Bearbeitung: heise medien)
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?
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.