Am 21. Oktober teilte Microsoft Research mit, dass Xinzhi Zhang und Zhao Song die Kannan–Lovász–Simonovits-Vermutung bewiesen hätten, ein 1995 formuliertes mathematisches Problem. In der Ankündigung von Microsoft Research erklärt das Unternehmen, das Ergebnis sei aus einem von Menschen gesteuerten Agenten-Workflow hervorgegangen und nicht aus einem vollständig autonomen Modelldurchlauf.
Microsoft zufolge untersuchten KI-Systeme mehr als 100 mögliche Ansätze, während die Forschenden entschieden, welche Wege sie weiterverfolgen, schwache Ansätze verwerfen und die verbleibende Mathematik prüfen. Das Unternehmen erklärt zudem, dass ungesteuerte Versuche mit mehreren führenden Modellen und einem annähernd gleichen gesamten Token-Budget das Problem nicht lösten.
Laut dem Beitrag wurden die Tools nicht nur zur Ideengenerierung eingesetzt, sondern auch für Herleitungen, das Verfassen der Arbeit und interne Prüfungen des Beweises. Microsoft ergänzt, dass bereits eine Formalisierung in Lean 4 veröffentlicht wurde; nach der abschließenden Prüfung sei eine kürzere, maschinell verifizierte Version geplant.
Die Arbeit sollte weiterhin als wichtiges Preprint-Ergebnis gelesen werden, nicht als endgültiger Meilenstein für Lehrbücher. Unabhängige Berichte zufolge veröffentlichten andere Gruppen innerhalb weniger Tage parallele Beweise, was das Vertrauen erhöht. Ein Journal-Review hat die Arbeit jedoch noch nicht durchlaufen.