EINE KI KNACKT EIN FÄRBUNGSRÄTSEL

Man nehme ein Netz aus Punkten, die durch Linien verbunden sind – Mathematiker nennen das einen Graphen. Nun färbe man die Punkte so, dass zwei durch eine Linie verbundene Punkte nie dieselbe Farbe haben. Die kleinste Zahl von Farben, die dafür reicht, ist die chromatische Zahl des Graphen. Ein berühmter Sonderfall ist der Vierfarbensatz, bewiesen 1977, dessen Titel alles sagt: „Every planar map is four colorable” (Jede ebene Landkarte ist mit vier Farben färbbar).

Hadwigers Wette von 1943

1943 schlug Hadwiger eine umfassende Regel für alle Graphen vor. Man verkleinere einen Graphen, indem man Punkte oder Linien löscht und zwei verbundene Punkte zu einem verschmilzt. Das Ergebnis heißt Minor. Hadwiger betrachtete den größten vollständigen Graphen – einen Cluster, in dem jeder Punkt mit jedem anderen verbunden ist –, den man auf diese Weise erhalten kann, und vermutete, dass die Zahl der benötigten Farben nie die Größe dieses Clusters übersteigt.

Die Arbeit nennt dies „eines der ältesten und grundlegendsten Probleme der Graphentheorie”. Bewiesen ist es nur für kleine Fälle: bis zu Clustern der Größe fünf, wo es sich als äquivalent zum Vierfarbensatz oder auf ihn zurückführbar erweist. Ab sechs ist es offen.

Annäherung, ein Logarithmus nach dem anderen

Da die exakte Aussage sich widersetzt, versuchten Forscher, die Zahl der Farben durch eine Funktion der Clustergröße zu beschränken, die so langsam wie möglich wächst. Die Arbeit zeichnet die Fortschritte nach. Jahrzehntelang wuchs die beste Schranke etwas schneller als proportional – um einen Faktor mit der Quadratwurzel eines Logarithmus. Vor einigen Jahren durchbrachen Norin, Postle und Song diese Barriere. Delcourt und Postle verbesserten sie dann weiter und zeigten vor allem, dass es genügt, sich mit recht kleinen Graphen zu befassen. Liu und Luo drückten den Zusatzfaktor bis auf einen dreifachen Logarithmus herunter.

Der natürliche Endpunkt ist die lineare Hadwiger-Vermutung: Ein festes Vielfaches der Clustergröße reicht immer. Genau das beanspruchen nun Sergey Norin von der McGill University in Montreal und Raphael Steiner von der ETH Zürich bewiesen zu haben.

Die Rolle der Maschine

Die Autoren sind deutlich: Der Beweis wurde von GPT-6 Astra, einem OpenAI-Modell, nach ihren Anweisungen gefunden. Zuerst baten sie es, den Fall sehr dichter Graphen zu beweisen, den sie für das fehlende Teilstück hielten. Es gelang, schreiben sie, „nach nur ein paar Stunden und etwas Ermutigung”. Gebeten, eine Abhängigkeit explizit zu machen, deckte es Graphen bis zu einer bestimmten Größe ab – aber nicht ganz den benötigten Bereich. Dann baten sie es um eine originelle Idee, um die Lücke zu schließen, woraus der „Bootstrap”-Schritt des endgültigen Beweises entstand. Fast keine der eigenen konkreten Beweisideen der Autoren hat überlebt, sagen sie, bis auf einen Vorschlag zu Kontraktionen.

Der Text stammt von Menschen. Ein weiteres OpenAI-Modell half beim Korrekturlesen und bei der Bibliografie. Die Autoren berichten, dass OpenAIs Codex eine formale, maschinell prüfbare Version des gesamten Beweises im Beweisassistenten Lean erstellt hat, die online zusammen mit einem frühen, von KI geschriebenen Entwurf veröffentlicht wurde. Sie übernehmen die volle Verantwortung für die Mathematik.

Im Inneren des Beweises

Das Argument hat zwei Hälften:

1. Kleine Graphen, wenige Farben. Für Graphen, die nicht viel größer als die Clustergrenze sind, zeigen die Autoren, dass etwa das Vierfache der Clustergröße genügt. Ausgangspunkt ist ein Ergebnis von Reed und Seymour aus dem Jahr 1998: Eine gelockerte, „fraktionale” Form der Färbung gehorcht der linearen Regel bereits mit dem Faktor zwei. Die neue Arbeit macht aus fraktionalen Färbungen echte, indem sie dem Graphen einige zusätzliche Linien hinzufügt und in einer Hilfsstruktur riesige Paarungen (Matchings) findet.
2. Ein Bootstrap. Ein zweites Argument erweitert den Bereich der abgedeckten Graphengrößen bei jedem Schritt um einen Faktor vier Drittel im Exponenten, auf Kosten einer größeren Konstante. Zehn Schritte bringen den Bereich von einem Drittel auf etwa 5,92, über die von der Delcourt-Postle-Reduktion geforderte Schwelle von 5 hinaus. Diese Hälfte nutzt einen alten Trick von Gyárfás, der laut den Autoren noch nie auf dieses Problem angewandt worden war.

Die Autoren beschreiben den Beweis als aus bekannten Werkzeugen gebaut – „in der konvexen Hülle bestehender Ergebnisse enthalten”, aber nicht an einem offensichtlichen Rand davon.

Was offen bleibt

Die Konstante ist gewaltig: Eine grobe Schätzung ergibt etwa 10¹⁰⁰. Die Autoren sehen Spielraum, sie unter 10¹⁰ zu drücken, glauben aber, dass etwa 100 zu erreichen neue Ideen erfordern würde. Hadwigers exakte Vermutung bleibt unberührt: „Wir sind unentschieden”, schreiben sie. Die Arbeit ist ein Preprint; 41 Seiten neuer Mathematik müssen sich nun der Prüfung durch andere Fachleute stellen.