Null Entschuldigungen, ein großes Sternchen: Einblick in OpenAIs zehn maschinengeprüfte Beweise
Überblick über die Kolumne
Am 1. August 2026 veröffentlichte OpenAI ein Manuskript, das vor zwei Jahren wie Fiktion geklungen hätte: Ein unveröffentlichter interner Build des nächsten Modells, Codename Astra, erzeugte vollständig maschinengeprüfte Lean-4-Beweise für zehn Probleme, die seit einem Jahrzehnt oder länger ungelöst waren – in Gruppentheorie, Operatoralgebren, Kugelpackung, Schaltkreiskomplexität und Ramsey-Theorie. Das 249-seitige Dokument wird mit einem GitHub-Repository mit Beweiszertifikaten unter Apache-2.0-Lizenz ausgeliefert, und das Detail, das alle wiederholen, ist, dass die Zahl der „sorry" im Lean-Code null beträgt – das heißt, kein Schritt blieb als unbewiesener Platzhalter stehen, keine Lücke wurde mit einer Annahme übertüncht. Jede Zeile wurde von einem Beweisassistenten geprüft, dem Ruf, Hype-Zyklen oder die Autorenschaft des Papiers egal sind.
Was tatsächlich gelöst wurde
Das wichtigste Ergebnis ist eine explizite Konstruktion einer nicht-sofischen Gruppe, womit eine Frage beantwortet wird, die Michail Gromow stellte, als er Sofizität 1999 definierte. Allein dieser Punkt wäre für einen menschlichen Mathematiker ein karrierebestimmendes Ergebnis. Daneben steht ein Gegenbeispiel zu Connes‘ Starrheitsvermutung über Gruppen-von-Neumann-Algebren – ein Teilgebiet, in dem Fortschritt historisch in Jahrzehnten gemessen wurde, nicht in Monaten. Das Manuskript berichtet außerdem über verbesserte asymptotische obere Schranken für Kugelpackungen in hohen Dimensionen – ein Problem mit einem seltsamen öffentlichen Profil, da die Fälle in acht und vierundzwanzig Dimensionen durch Maryna Viazovska‘s gefeierte Arbeit berühmt wurden, während die allgemeinen hochdimensionalen Asymptotiken vergleichsweise unglamourös und hartnäckig geblieben sind. Abgerundet werden die zehn durch weitere Ergebnisse in Schaltkreiskomplexität und Ramsey-Theorie, zwei Bereichen, in denen kombinatorische Explosion computergestützte Suche historisch entweder unpraktikabel oder, wenn sie funktionierte, wenig überzeugend gemacht hat.
Was diese Liste von der üblichen „KI löst Matheproblem"-Presseschleife unterscheidet, ist die Verifikationsebene. Lean benotet nicht nach Kurve. Ein Lean-geprüfter Beweis kompiliert entweder gegen die formale Aussage oder nicht, und es gibt keinen Gutachter, den man bezirzen muss, keinen Betreuer, den man beruhigen muss, kein Komitee, das man zufriedenstellen muss. Das ist eine wesentlich andere Behauptung als „das Modell hat eine Beweisskizze erzeugt, die Experten plausibel fanden“, was näher an dem liegt, was frühere KI-Mathe-Ankündigungen tatsächlich waren.
Die gespaltene Rezeption
Die Reaktionen arbeitender Mathematikerinnen und Mathematiker sind wirklich geteilt, und zwar nicht entlang der Linien, die man bei einer typischen KI-Hype-Geschichte erwarten würde. Timothy Gowers, der eine Fields-Medaille und eine lange Spur von Skepsis gegenüber übertriebenen KI-Behauptungen hat, sagte, er würde einen der zehn Beweise ohne Zögern für eine Top-Zeitschrift empfehlen – eine echte Bestätigung von jemandem, der solche Dinge nicht leichtfertig vergibt. Thomas Bloom, der den Erdos-Probleme-Katalog an der Universität Manchester kuratiert und daher so gut wie jeder weiß, was „ungelöst“ in der Praxis bedeutet, nannte die Ergebnisse „große Neuigkeiten“.
Aber die Begeisterung ist nicht einhellig, und die Skepsis sollte man ernst nehmen, statt sie als reflexartiges Gatekeeping abzutun. Steven Miller von der Yeshiva University hat OpenAI beschuldigt, für diese Ergebnisse effektiv auf seine eigene veröffentlichte Forschung ohne Quellenangabe zurückgegriffen zu haben – eine Beschwerde, die anders wirkt als generische „KI hat meine Inhalte gefressen“-Klagen, weil sie aus der spezifischen mathematischen Gemeinschaft kommt, deren jahrzehntelang veröffentlichte Lemmata und Techniken genau das Trainingssubstrat sind, das ein solches Modell bräuchte. Und das Timing ist nicht neutral: Die Leidener Erklärung, inzwischen von der Internationalen Mathematischen Union unterstützt, hat bereits ein Zeichen gesetzt und davor gewarnt, dass KI-Unternehmen veröffentlichte mathematische Forschung ohne Zustimmung nutzen, Peer Review umgehen und Druck auf die Normen von Zuschreibung und Beweis ausüben, auf denen das Feld seit sehr langer Zeit beruht. Diese Ankündigung kommt genau in die Mitte dieses Arguments, nicht davor.
Die 2.000-Dollar-Frage
OpenAIs eigene Rahmung setzt stark auf Kosten: etwa 2.000 Dollar an Rechenleistung zu aktuellen API-Preisen, um zehn Beweise zu erzeugen, deren Lösung der mathematischen Gemeinschaft kollektiv über hundert Personenjahre nicht gelungen ist. Das ist eine auffällige Zahl, und sie soll auffällig sein. Aber die Zahl deckt nur die erfolgreichen Läufe ab – sie sagt nichts darüber, wie viele Versuche nicht funktioniert haben, wie viele Kandidatenbeweise erzeugt und verworfen wurden oder wie viel Rechenleistung in Probleme geflossen ist, die nie ins Manuskript geschafft haben. Kritiker haben schnell darauf hingewiesen, dass 2.000 Dollar damit eher Publikationskosten sind als Entdeckungskosten. Das entspricht einem Unternehmen, das nur seine profitablen Geschäfte meldet: wahr, so weit es reicht, aber nicht die Zahl, die man bräuchte, wenn man die tatsächliche Ökonomie des Prozesses abschätzen wollte.
Es gibt auch eine Reproduzierbarkeits-Falte, die in der Aufregung leicht übersehen wird. Niemand außerhalb von OpenAI kann Astra ausführen – es ist ein unveröffentlichter interner Build, kein ausgeliefertes Produkt. Die Beweise selbst sind also unabhängig prüfbar, weil Lean offen und die Zertifikate öffentlich sind. Aber der Prozess, der sie erzeugt hat, ist für niemand anderen unabhängig wiederholbar. Das ist eine ungewöhnliche erkenntnistheoretische Position: völlige Transparenz auf der Ebene des Outputs, völlige Undurchsichtigkeit auf der Ebene der Methode. Es lohnt sich, bei dieser Unterscheidung zu verweilen, denn „verifiziert“ und „reproduzierbar“ erfüllen hier unterschiedliche Aufgaben, und sie gleichzusetzen ist genau der Weg, wie aus einer korrekten Pressemitteilung eine aufgeblähte öffentliche Erzählung wird.
Bemerkenswert ist auch, was diese Ankündigung nicht behauptet. Frühere OpenAI-Mathe-Ankündigungen kamen manchmal mit pauschalen Behauptungen über externe Begutachtung oder Expertenvalidierung; diese hier macht diesen Schritt nicht. Die Befürwortungen – Gowers, Bloom – wirken eher wie individuelle Reaktionen denn wie ein orchestrierter Begutachtungsprozess, und OpenAI scheint sich auf Leans formale Verifikation zu stützen, um die Glaubwürdigkeitsarbeit zu leisten. Das ist argumentativ ehrlicher, aber es bedeutet auch, dass die informelle Prüfung der Gemeinschaft – die Art, die normalerweise durch Seminare, Gutachtenberichte und jahrelange Versuche, ein Ergebnis zu widerlegen, geschieht – für den mathematischen Gehalt noch nicht stattgefunden hat, obwohl die formale Logik ihre Prüfung bereits bestanden hat.
Dies im Kontext der restlichen Woche lesen
Nichts davon geschah im luftleeren Raum. In denselben Tagen senkte OpenAI die Preise für GPT-5.6 „Luna“ um etwa 80 % auf 0,20 Dollar pro Million Eingabe-Token, und ChatGPT überschritt Berichten zufolge etwa eine Milliarde wöchentlich aktive Nutzer. Die Transparenz- und Kennzeichnungspflichten des EU-KI-Gesetzes traten ebenfalls am 2. August in Kraft. Setzt man diese Puzzleteile neben die Mathe-Ankündigung, wird ein Muster sichtbar: Ein Unternehmen, das gleichzeitig bei Preis und Umfang seines Verbraucherprodukts rast und versucht, eine Flagge auf dem schwierigsten möglichen Terrain zu pflanzen – der reinen Mathematik –, wo „Halluzination“ nicht nur eine Belästigung, sondern ein Kategorienfehler ist, weil ein falscher Beweis schlicht nicht kompiliert.
Genau deshalb ist das Lean-Verifikationsdetail wichtiger als die 2.000-Dollar-Zahl oder der Nutzerzahlen-Meilenstein. Preiskämpfe und Nutzungszahlen sind Geschäftskennzahlen, die in beide Richtungen gedreht werden können. Eine „sorry“-Zahl von null in einem formalen Beweisprüfer ist nicht in gleicher Weise drehbar – sie ist entweder wahr oder das Repository kompiliert nicht. Die interessante Spannung ist, dass diese härteste, am besten verifizierbare Behauptung auch diejenige ist, die mit der geringsten Reproduzierbarkeit ankommt, eingehüllt in die umstrittensten Zuschreibungsfragen, genau in dem Moment, in dem sich die mathematische Gemeinschaft um die Leidener Erklärung organisiert, um dagegenzuhalten, wie KI-Labore veröffentlichte Forschung nutzen. Ob Astra einen echten Phasenwechsel in der mathematischen Entdeckung darstellt oder eine sehr gut ausgewählte Highlight-Reel aus einem viel größeren und chaotischeren Suchprozess, ist eine Frage, die das nächste Jahr der Prüfung beantworten muss – nicht dieses eine Manuskript.