Mathematiker beweisen mit KI-Agenten die 31 Jahre alte KLS-Vermutung. Modelle allein schafften es mit denselben Tokens nicht

Microsoft Research hat am 21. Oktober bekanntgegeben, dass sein Forscher Xinzhi Zhang und Koautor Zhao Song die KLS-Vermutung aus dem Jahr 1995 bewiesen haben. Für die Mathematik ist damit ein 31 Jahre altes Problem gelöst. Für KI-Teams ist es eine ungewöhnlich genaue Beschreibung dessen, was Agenten bei solcher Arbeit tun und was Menschen.

Ein gerader Schnitt reicht in jeder Dimension

Die Vermutung von Kannan, Lovász und Simonovits betrifft eine breite Klasse hochdimensionaler Wahrscheinlichkeitsverteilungen, die sogenannten log-konkaven Verteilungen. Sie fragt, ob der beste gerade Schnitt durch eine solche Form fast so gut ist wie der beste Schnitt beliebiger Form. Die Vermutung besagt, dass der Unterschied durch eine Konstante begrenzt ist, die nicht von der Zahl der Dimensionen abhängt. Darauf beruht auch die Theorie der Irrfahrten, mit denen Algorithmen aus Verteilungen Stichproben ziehen.

Das beste bekannte Ergebnis vom Juli 2026 ließ noch zu, dass die Schranke mit der Dimension langsam wächst. Die Autoren schärften es zunächst nach und gingen mit KI-Agenten mehr als 100 mögliche Ansätze durch, oft mit langen Rechnungen mit Tensoren höherer Ordnung. Daraus entstand ein neues Kriterium. Die Fassung des Papers vom 1. Oktober wendete es wiederholt an und drückte die Abhängigkeit von der Dimension auf den iterierten Logarithmus. Die Fassung vom 4. Oktober wiederholte das ganze Verfahren, zeigte, dass sich die kleinen Fehler nicht unbegrenzt aufsummieren, und schloss den Beweis ab. Laut Blog stammt die Idee für diesen Schritt aus früheren Arbeiten der Autoren zu schnellen Algorithmen für lineare Optimierung.

Andere haben das Ergebnis bereits bestätigt. Am selben Tag veröffentlichte eine eigenständige Expertengruppe einen eigenen vollständigen Beweis und nannte die erste Fassung des Microsoft-Papers „den entscheidenden Schritt“. Ein dritter Beweis vom selben Tag stützt sich auf eine eng verwandte Idee. Danach erschien eine Formalisierung in Lean 4, die das Kriterium aus der ersten Fassung mit weiterer Forschung verbindet.

Der Kontrollversuch ohne Menschen ist für KI-Teams wichtiger als der Beweis selbst

Der Blog beschreibt die Arbeitsteilung genau. KI-Werkzeuge probierten Varianten aus, führten detaillierte Herleitungen durch, halfen beim Schreiben des Manuskripts und machten interne Beweisprüfungen. Die Menschen gaben die Richtung vor, wählten vielversprechende Ideen aus, fügten sie zum endgültigen Argument zusammen und prüften den Beweis. Die Agenten liefen parallel, und nach jeder Runde strich der Forscher Sackgassen und gab das beste Zwischenergebnis in die nächste Runde. Etwa hundert solcher Pfade gab es.

Am wertvollsten ist der Kontrollversuch. Die Autoren versuchten mehrfach, dasselbe Problem mit mehreren führenden Modellen ohne Anleitung und mit ungefähr demselben Token-Budget zu lösen. Das Ziel erreichten sie nicht. Für Unternehmen, die hoffen, Forschung durch einen einzigen großen Modelllauf zu ersetzen, ist das eine nützliche Warnung. Gewirkt hat hier die Kombination aus Suche und menschlichem Urteil, das die Agenten laufend von falschen Wegen abbrachte.

Für die Mathematik ist die Wirkung unmittelbar. Viele Sätze, die bisher nur unter der Annahme galten, dass KLS stimmt, gelten jetzt ohne Bedingung. Das stärkt die Grundlagen der konvexen Geometrie, der Wahrscheinlichkeitstheorie und der theoretischen Informatik.

Der Kontrollversuch ist bisher nur ein Satz in einem Blogbeitrag

Microsoft hat nicht offengelegt, welche Modelle im Kontrollversuch liefen, wie viele Versuche es gab und wie viele Tokens verbraucht wurden. Die Aussage, dass die Arbeit ohne Menschen scheiterte, ist deshalb vorerst eine Schilderung der Autoren selbst und keine Messung, die andere wiederholen können. Dasselbe gilt für die „mehr als 100 Ansätze“, die ihren eigenen Prozess beschreiben.

Auch die formale Prüfung hat zwei Ebenen. Die veröffentlichte Formalisierung in Lean 4 verbindet das Kriterium aus der ersten Fassung mit anderer Forschung und ist damit keine maschinelle Prüfung genau dieses Beweises. Die Autoren haben einen verkürzten, in Lean geprüften Beweis, wollen ihn aber erst nach der abschließenden Durchsicht veröffentlichen. Das Ergebnis selbst liefert zudem keinen neuen Sampling-Algorithmus. Es ändert vor allem, was sich über die bestehenden beweisen lässt.

Ein veröffentlichter Lean-Beweis und Details zum Kontrolllauf entscheiden über die Stärke des Arguments

Für Mathematiker zählt vor allem der verkürzte, in Lean geprüfte Beweis und seine Annahme im Peer Review. Drei unabhängige Beweise am selben Tag sind ein starkes Signal, doch erst das Review gibt dem Ergebnis sein endgültiges Gewicht.

Für die KI-Welt ist wichtiger, ob Microsoft die Daten des Kontrollversuchs veröffentlicht: die Modelle, die Zahl der Läufe und den Token-Verbrauch. Erst dann lässt sich ehrlich beziffern, wie viel Arbeit der Mensch leistete, der die Sackgassen strich. Und es zeigt sich, ob eine von Menschen beschnittene Suche auch bei anderen offenen Problemen funktioniert oder nur hier.

Liliths Urteil

Hundert Agenten suchten einen Weg, während ein Mathematiker nach jeder Runde die Sackgassen durchstrich. Die Modelle ohne ihn bekamen dasselbe Token-Budget und fanden keinen Beweis, was jeder Manager zweimal lesen sollte, der Forschung einem einzigen großen Lauf überlassen will.