Ein am 19. Oktober 2026 veröffentlichter Bericht über Gespräche mit den Mathematikern Richard Borcherds und Robin Huang von der University of California, Berkeley, macht ihre unterschiedlichen Einschätzungen zu KI deutlich. Borcherds hält es für möglich, dass KI menschliche Mathematiker in wenigen Jahren überflüssig machen könnte, wenn die Entwicklung so weitergeht. Huang bezweifelt den derzeitigen Nutzen von KI für die mathematische Forschung und sorgt sich um die Folgen für die Fachgemeinschaft.
Die technische Kritik an OpenAIs Navier–Stokes-Behauptung betrifft eine andere Frage: Eine am 6. Oktober veröffentlichte Analyse findet Abweichungen zwischen ausgewählten Passagen des schriftlichen Beweises und seiner Lean-Formalisierung. Die Autoren erklären ausdrücklich, dass sie damit nicht behaupten, der natürlichsprachliche Beweis sei falsch.
Zwei Sichtweisen auf KI in der Mathematik
Der Bericht von The Daily Californian stellt die Einschätzungen von Borcherds und Huang gegenüber, nicht einen Konsens unter Mathematikern. Borcherds sieht KI auf dem Weg, menschliche Forscher zu übertreffen. Huang äußert Zweifel am aktuellen Nutzen für die Forschung und stellt infrage, ob die bestehenden Anreize und Normen in der Mathematik zu den Spannungen rund um KI beitragen.
Was OpenAI behauptet
OpenAI erklärte am 8. September, sein Ergebnis betreffe eine dreidimensionale inkompressible Flüssigkeit, die unter einer glatten äußeren Kraft in endlicher Zeit eine Singularität entwickelt. Die Flüssigkeit starte dabei in Ruhe und ihre Energie bleibe endlich. OpenAI zufolge erfüllt das Ergebnis die Aussagen C und D der Formulierung des Clay Mathematics Institute.
Für diese Arbeit setzte OpenAI nach eigenen Angaben rund 10.000 Agenten gleichzeitig ein. Sie erzeugten etwa 2,7 Millionen Nachrichten und rund 130 Milliarden Ausgabetoken. Die Agenten hätten das Ergebnis nach ungefähr 88 Stunden erreicht; die anschließende Lean-Formalisierung und Prüfung hätten weitere 17 Stunden gedauert. NeoTeo berichtete bereits über OpenAIs mathematische Ergebnisse aus einem internen Modell.
Wo Text und Lean-Fassung auseinanderlaufen
A. Bastounis, F. Circelli und A. C. Hansen vergleichen in ihrer Analyse eine Abschätzung in OpenAIs schriftlichem Beweis mit der entsprechenden Aussage in der Lean-Fassung. Beim Lemma 8.6 enthält die Eingabeschranke der Textfassung vier zusätzliche Ableitungen; die angeführte Lean-Abschätzung enthält fünf.
| Fassung der Abschätzung | Zusätzliche Ableitungen in der Eingabeschranke |
| Schriftlicher Beweis | 4 |
| Angeführte Lean-Fassung | 5 |
Die Autoren nennen außerdem Unterschiede bei einer Abschätzung des Druckflusses. Die Textfassung verwendet einen Term mit B_R, während die Lean-Abschätzung zusätzlich von A_R abhängt. Da sich die Ausdrücke auch an weiteren Stellen unterscheiden, halten die Autoren beide Abschätzungen für schwer vergleichbar.
Was eine Lean-Prüfung aussagt
Lean ist ein Beweisassistent, der formal codierte mathematische Aussagen und Beweisschritte nach den Regeln des Systems prüft. Eine erfolgreiche Prüfung betrifft die Aussage, die tatsächlich codiert wurde. Sie belegt für sich allein nicht, dass diese Codierung den Inhalt des schriftlichen Arguments genau wiedergibt. Die Analyse von Bastounis, Circelli und Hansen richtet sich auf diese Übereinstimmung zwischen ausgewählten Textpassagen und ihrer Formalisierung.
