722 Beweise einer KI: Was sich schon prüfen lässt

In der Nacht vom 6. auf den 7. Oktober, in Spanien bereits in den frühen Morgenstunden, lud OpenAI 722 mathematische Manuskripte auf GitHub hoch. Geschrieben hat sie ein internes Modell, das das Unternehmen weder veröffentlicht noch benannt hat, und sie sind in 372 „Familien“ gruppiert: Jede vereint ein Hauptergebnis mit seinen Varianten und Folgerungen. OpenAI erklärt, dass es seine Modelle an ungelösten Forschungsproblemen evaluiert und die Ergebnisse veröffentlicht hat, die ein ausreichendes Maß an Relevanz erreichten.

Am 21. September hatte das Unternehmen erklärt, sein Modell habe „mehr als hundert“ offene Probleme gelöst, ohne eines davon zu zeigen. Jetzt hat es sie gezeigt, und es sind mehr. Darunter sind Behauptungen, die, sollten sie sich bestätigen, seit Jahrzehnten offene Fragen beantworten würden: wie sich die Primzahlen verteilen, wo die Grenzen von Optimierungsalgorithmen liegen oder warum ein Magnet ein Magnet bleibt.

Lance Fortnow, ein Veteran der theoretischen Informatik, schrieb am Tag darauf, sein Fach sei in 24 Stunden weiter vorangekommen als in den drei Jahrzehnten davor zusammen. Im selben Beitrag fügte er hinzu, dass nichts davon bisher verifiziert ist.

Dieser Vorbehalt ist die Frage dieses Artikels: Was bedeutet es, dass diese Ergebnisse „geprüft“ sind? Diesmal kann eine Maschine einen Teil davon überprüfen, was bei keiner früheren Ankündigung der Fall war. Doch diese Prüfung hat mehrere Ebenen, und der größte Teil der Arbeit steht noch aus.

Was genau im Repository liegt

Laut README des Repositorys erhielt das Modell rund 4.000 Probleme, und jedes Ergebnis verbrauchte im Schnitt so viel Rechenleistung wie drei Stunden Nachdenken von ChatGPT Pro. Wie es diese Probleme ausgewählt hat, erklärt das Unternehmen nicht, doch ein Verhältnis lässt sich ablesen: Aus rund 4.000 Versuchen gingen 372 Familien hervor. Wie Fortnow anmerkt, löste das Modell weniger als 10 % dessen, was ihm vorgelegt wurde.

Fast alles entstand mit demselben automatischen Verfahren. Das README nennt zwei Ausnahmen, ohne sie näher zu erläutern: einen Bereich der Riemannschen Zetafunktion, in dem es keine Nullstellen gibt, und die Hodge-Vermutung für eine bestimmte Familie geometrischer Objekte. Es sind ausgerechnet die beiden Ergebnisse, die Millennium-Problemen am nächsten kommen. Einer der Texte zur Zetafunktion wurde zudem von Menschen bearbeitet, um ihn lesbar zu machen.

Das Repository enthält:

• die Artikel als PDF mit ihren Quelldateien;
• zehn gekürzte Zusammenfassungen der Überlegungen, denen das Modell folgte;
• eine Bibliothek formaler Beweise in Lean, auf die wir gleich eingehen;
• und die Zusage, die Versionsgeschichte zu bewahren: Korrekturen werden als neue Versionen veröffentlicht, ohne die früheren zu löschen.

Das README selbst warnt: „Some of the unformalized results could have issues“. Einige der nicht formalisierten Ergebnisse könnten Probleme aufweisen.

Der Beitrag zur Ankündigung hebt kein konkretes Ergebnis hervor. Die Liste der „großen Ergebnisse“, die in diesen Tagen kursiert, ist eine Auswahl der Presse und der Mathematiker selbst. Wir haben vier ausgewählt, an denen sich die Tragweite des Behaupteten ablesen lässt.

Vier Ergebnisse, um zu verstehen, was auf dem Spiel steht

Die Primzahlen und die Zetafunktion

Die Primzahlen scheinen sich regellos zu verteilen, folgen aber einem durchschnittlichen Gesetz, das 1896 bewiesen wurde: Bis zu einer Zahl x gibt es ungefähr x/ln x Primzahlen. Interessant ist die Frage, wie weit die tatsächliche Anzahl von diesem Gesetz abweicht. Und die Antwort hängt davon ab, wo die Nullstellen der Riemannschen Zetafunktion liegen, also die Punkte, an denen diese Funktion den Wert null annimmt.

Die Riemannsche Vermutung, 1859 formuliert und eines der sieben Millennium-Probleme, besagt, dass alle diese Nullstellen auf einer bestimmten Geraden liegen, der mit Realteil 1/2. Ist sie wahr, ist der Fehler beim Zählen der Primzahlen der kleinstmögliche. Bis heute wusste man nur, dass es genau am Rand, bei Realteil 1, keine Nullstellen gibt, und ebenso wenig in einem Streifen, der nach oben hin immer schmaler wird. Niemand hatte beweisen können, dass es einen nullstellenfreien Streifen fester Breite gibt. Diese abgeschwächte Version ist als Quasi-Riemann-Hypothese bekannt.

OpenAI behauptet, sie bewiesen zu haben: Es gibt keine Nullstellen mit Realteil größer als 7/8. Das ist nicht die Riemannsche Vermutung, die bis 1/2 reichen muss, aber es wäre der erste Fortschritt dieser Art, seit die Frage gestellt wurde. Ein anderes Manuskript derselben Familie schließt zudem die sogenannten Siegel-Nullstellen aus, eine hypothetische Anomalie, wegen der viele Sätze über Primzahlen von Konstanten abhängen, die niemand berechnen kann. Ein weiteres Manuskript beweist auf anderem Weg einen etwas kleineren Bereich, ab 11/12. Es ist der Text, den Menschen bearbeitet haben.

Die Grenzen von Optimierungsalgorithmen

Viele praktische Probleme sind zu schwierig, um sie in großem Maßstab exakt zu lösen. Ein Beispiel ist, ein Netz so in zwei Gruppen zu teilen, dass möglichst viele Verbindungen durchtrennt werden (Max-Cut). Ein anderes ist, die kleinste Zahl von Knoten zu wählen, die alle Verbindungen berühren (Vertex Cover). Für solche Fälle nutzen wir Algorithmen, die eine Näherungslösung mit garantierter Qualität liefern. Der Algorithmus für Max-Cut etwa garantiert mindestens 87,8 % des Optimums.

Seit 2002 sagt die Unique-Games-Vermutung (Unique Games Conjecture) von Subhash Khot voraus, dass es in vertretbarer Zeit nicht besser geht. Ist sie wahr, wären viele der Näherungsalgorithmen, die wir bereits nutzen, die bestmöglichen, es sei denn, P = NP. OpenAI behauptet, die Vermutung bewiesen zu haben. In einem separaten Ergebnis behauptet es außerdem, ohne sich auf sie zu stützen, zu beweisen, dass es NP-schwer ist, diese Garantien für Max-Cut und Vertex Cover zu verbessern, also so schwer wie die härtesten Probleme ihrer Klasse.

Dahinter steht auch eine menschliche Geschichte. Laut Quanta Magazine kamen am 11. September Gerüchte auf, OpenAI habe den Beweis. Dor Minzer (MIT) und zwei Studierende arbeiteten seit sieben Jahren an einer Variante des Problems und hatten sie im April gelöst. Drei Tage nach den Gerüchten veröffentlichten sie 95 Seiten mit einem Hinweis auf der ersten: Der Text sei mathematisch vollständig, habe aber noch nicht die Form, in der sie ihn teilen wollten. „There is a lot of value in failing and knowing why you failed“, sagte Minzer dem Magazin: Zu scheitern und zu verstehen, warum, hat großen Wert.

Warum ein Magnet ein Magnet bleibt

In einem Magneten richten sich die winzigen magnetischen Momente der Atome, die Spins, gleich aus. Die Quantenphysik beschreibt dieses Verhalten mit dem Heisenberg-Modell, und jeder Physiker geht davon aus, dass das Material in drei Dimensionen bei niedriger Temperatur seine Magnetisierung behält. Das streng zu beweisen, war etwas anderes. Die klassische Version des Modells und der quantenmechanische antiferromagnetische Fall, in dem benachbarte Spins in entgegengesetzte Richtungen zeigen, wurden vor Jahrzehnten gelöst. Doch die Technik, die in diesen Fällen funktionierte, versagt beim gewöhnlichen Quantenmagneten, und Elliott Lieb nahm ihn 1999 als „Problem A“ in eine Liste offener Probleme der mathematischen Physik auf.

OpenAI behauptet, ihn für alle Dimensionen ab drei bewiesen zu haben. Es ist ein gutes Beispiel für eine Art von Ergebnis, die oft unbemerkt bleibt: Es ändert nicht, was wir über die Welt glauben, aber es verwandelt eine physikalische Gewissheit in ein Theorem.

Eine klassische Frage mit einer unerwarteten Antwort

Aus einer „freien Gruppe“, der Menge aller Wörter, die sich mit zwei Buchstaben und ihren Inversen schreiben lassen, oder mit dreien, konstruiert man ein Objekt der Analysis, einen sogenannten Von-Neumann-Faktor. Diese Objekte tauchen in den grundlegenden Arbeiten von Murray und von Neumann auf, und die Frage, die Richard Kadison zugeschrieben wird, lautet, ob sich das Objekt daran erinnert, mit wie vielen Buchstaben man begonnen hat. Sie gilt als das bekannteste offene Problem ihres Gebiets, und ein Großteil der Forschung zielte darauf, zu beweisen, dass die Objekte verschieden sind.

OpenAI behauptet das Gegenteil: Mit zwei oder mit drei Buchstaben erhält man dasselbe Objekt. Bestätigt sich das, wäre es eines jener Ergebnisse, die ein ganzes Fach zwingen, seine Intuition zu überdenken. Zudem veranschaulicht es gut das Problem, um das es im nächsten Abschnitt geht.

Der Rest des Katalogs

Diese vier sind eine Auswahl. Die Tabelle führt weitere Ergebnisse ersten Ranges auf und zeigt, ob sie einen formalen Beweis in Lean haben:

Quelle: Katalog des Repositorys und Katalog der Formalisierungen, abgerufen am 7. Oktober 2026. Beschreibungen von Codin vereinfacht.

„Geprüft“ kann drei verschiedene Dinge bedeuten

Das Neue an dieser Veröffentlichung gegenüber den früheren ist Lean. Lean ist eine Sprache, in der man einen Beweis so detailliert aufschreibt, dass ein Programm ihn Schritt für Schritt überprüfen kann, ohne jemandem vertrauen zu müssen. Es stützt sich auf Mathlib, eine gemeinschaftliche Bibliothek bereits geprüfter Definitionen und Sätze. Dass ein Beweis in Lean „kompiliert“, bedeutet, dass jeder Schritt aus den vorherigen folgt.

Wenn es heißt, ein Ergebnis sei geprüft, lohnt es sich jedoch, drei Fragen auseinanderzuhalten.

Erstens: Ist der formale Beweis korrekt?

Das klärt Lean, und es lässt sich außerhalb von OpenAI wiederholen. Das Repository enthält Challenges für Comparator, ein Werkzeug, das einen Beweis nur akzeptiert, wenn er genau die Referenzaussage beweist und ausschließlich die Standardaxiome verwendet. Wenige Stunden nach der Veröffentlichung haben mehrere Personen außerhalb von OpenAI den Beweis für den Bereich ab 7/8 auf ihren Rechnern erneut kompiliert, mit korrektem Ergebnis.

Das Repository enthält mehr als 120.000 Lean-Dateien, doch diese Bibliothek deckt nur einen kleinen Teil des Katalogs ab: Bei 162 der 722 Manuskripte ist das Hauptergebnis formalisiert.

Zweitens: Sagt die formale Aussage, was wir glauben?

Lean garantiert, dass der Beweis die Aussage beweist, die ihm vorgegeben wurde. Es garantiert nicht, dass diese Aussage das bedeutet, was im Artikel steht. Diese Ebene hängt am stärksten von Menschen ab, und ihre Schwierigkeit variiert stark von Ergebnis zu Ergebnis.

Im besten Fall ist die Aussage so kurz, dass sie jeder mit etwas Vorbildung lesen kann:

theorem riemannZeta_ne_zero_of_seven_eighths_lt_re
    {s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0 := by
  sorry

Ist die Definition die der Gemeinschaft und passt die Aussage in zwei Zeilen, ist das Vertrauen, das Lean gibt, sehr hoch. Deshalb ist der nullstellenfreie Bereich ab 7/8 heute das am besten geprüfte Ergebnis des Katalogs.

Bei den Faktoren freier Gruppen liegt der Fall anders. Mathlib kennt diese Objekte noch nicht, daher definiert die Comparator-Challenge sie von Grund auf, mit Definitionen, die ebenfalls OpenAI geschrieben hat. Bei Unique Games ist es ähnlich: Die Aussage stützt sich auf Tausende Zeichen eigener Kodierungen. Ein perfekter Beweis zu einer leicht falschen Definition beweist etwas anderes. Jemand mit Fachkenntnis muss diese Definitionen lesen und bestätigen, dass sie das eigentliche Problem erfassen.

Der Katalog der Formalisierungen macht es in zwei Feldern deutlich: Auch die Lean-Beweise hat ein KI-Agent geschrieben (automation: agent), und ihre Überprüfung ist als ausstehend vermerkt (review: unchecked).

Drittens: Was haben wir verstanden?

Selbst wenn die Aussage gut formalisiert ist, deckt Lean meist nur den Hauptsatz ab. Bei der Quasi-Riemann-Hypothese weist die Dokumentation selbst darauf hin, dass die Anwendungen aus dem Artikel nicht enthalten sind. Genau diese Anwendungen interessieren jemanden, der auf Primzahlen spezialisiert ist.

Die übrigen 560 Manuskripte hängen heute von ihrem Text in natürlicher Sprache und vom internen Urteil von OpenAI ab. Darunter ist die Hodge-Vermutung, eines der beiden Ergebnisse, die nicht dem automatischen Verfahren folgten, und eines ohne Formalisierung.

Und dann bleibt, was kein Programm prüft: welche Idee jeden Beweis trägt, ob er neue Wege eröffnet und was sich im Fachgebiet ändert. Über diese Verschiebung haben wir bereits in Wenn Beweisen nicht mehr der Engpass ist geschrieben. Diese Veröffentlichung macht sie greifbar: Die Maschine hat die erste Ebene stark erleichtert, und die menschliche Arbeit konzentriert sich auf die beiden anderen.

Was die Mathematiker gefordert haben und was gekommen ist

Am 21. September stellte OpenAI eine unabhängige Beratungsgruppe aus neun Mathematikerinnen und Mathematikern vor, AGMAI, angesiedelt am Institute for Advanced Study in Princeton. Am 29. September, eine Woche vor der Veröffentlichung, veröffentlichte die Gruppe ihre Empfehlungen, gestützt auf mehr als 600 Rückmeldungen aus der Gemeinschaft. Sie begannen mit einer Bitte: dass die Labore aufhören, proprietäre Modelle an fortgeschrittenen mathematischen Problemen zu erproben. Hier der Vergleich zwischen dem, was gefordert wurde, und dem, was gekommen ist:

Quellen: Empfehlungen von AGMAI vom 29. September, Ankündigung von OpenAI und README des Repositorys. Vergleich von Codin erstellt.

Ohne das Modell und die Prompts kann niemand nachvollziehen, wie jedes Ergebnis zustande kam. Das hindert nicht daran, einen Beweis zu prüfen, der für sich allein trägt oder nicht. Es verhindert aber, zu wissen, wie stark die Auswahl der Probleme ins Gewicht fiel, was erfolglos versucht wurde oder ob die beiden Ausnahmen Hilfe erhielten, die der Rest nicht bekam.

Ebenfalls am 6. Oktober veröffentlichte AGMAI eine Erklärung, die man ganz lesen sollte. Darin heißt es, die beratende Rolle der Gruppe sei weder als Bewertung der Tragweite dieser Ergebnisse noch als Billigung des Verfahrens zu verstehen. Es sei Sache der Gemeinschaft, zu beurteilen, inwieweit ihre Empfehlungen befolgt wurden. Und sie fasst es so zusammen: „This release is the beginning, not the completion, of the process“. Die Veröffentlichung ist der Anfang des Prozesses, diese Ergebnisse zu verstehen und aufzunehmen, nicht sein Abschluss.

Wie die Gemeinschaft es in den ersten Stunden aufgenommen hat

Stand 7. Oktober hatte keine Fachperson eine Begutachtung eines konkreten Ergebnisses veröffentlicht, und kein Fehler war bestätigt. Was es gibt, sind Positionen dazu, wie die Ankündigung zu lesen ist.

Andrew Sutherland (MIT) forderte in Scientific American, als nicht verifiziert zu behandeln, was sich nicht reproduzieren lässt: „We should ask for receipts“. Daniel Litt (Universität Toronto) antwortete im selben Artikel mit dem gegenteiligen Argument. Wenn wir die Antworten kennen wollen, ergibt es keinen Sinn, das Unternehmen zu bitten, sie geheim zu halten, und er glaubt, dass es gut für die Mathematik sein wird. Mark Braverman (Princeton) sagte Quanta, Mathematik per Pressemitteilung sei „nicht sehr gesund“, räumte aber ein, dass ein solcher Beweis neue Forschungslinien eröffnen kann.

Unterdessen hat sich die Verifikation außerhalb von OpenAI zu organisieren begonnen. Neben den erneuten Lean-Kompilierungen hat ein gemeinschaftlicher Katalog offener Probleme Hunderte Ergebnisse importiert, jedes mit demselben Warnhinweis: Noch hat es niemand aus der unabhängigen Mathematik geprüft. Mehrere sind dort bereits als umstritten markiert, wegen möglicher Konflikte mit früher veröffentlichten Ergebnissen.

Der Grundton hat zwei Seiten. Es gibt Staunen über die Größenordnung, selbst unter den Kritikern. Und es gibt Müdigkeit: Nach der Kontroverse um die Urheberschaft von Navier–Stokes und dem Brief der Fields-Medaillenträger richtet sich die Kritik nicht mehr nur gegen das, was diese Systeme sagen. Sie richtet sich auch darauf, wer das Tempo bestimmt und wie veröffentlicht wird.

Ein grüner Test beweist nur, was der Test fragt

Am 29. September vertraten wir die Ansicht, wer hundert Fortschritte ankündigt, solle jeden mit genügend Informationen versehen, um ihn zu prüfen und darauf aufzubauen. Diese Veröffentlichung liefert deutlich mehr als die vorherige. Es gibt vollständige Manuskripte, eine formale Bibliothek, die jeder ausführen kann, und eine Versionsgeschichte. Es wäre unfair, das nicht anzuerkennen. Doch es fehlt weiterhin, was es erlauben würde, den Prozess zu reproduzieren, und es bleibt unklar, wer die Arbeit der Überprüfung bezahlt.

In der Software kennen wir die Unterscheidung gut, die dieser Fall sichtbar macht. Dass die Tests bestehen, beweist nicht, dass das Programm das Richtige tut: Es beweist, dass es tut, was die Tests prüfen. Ist die Spezifikation falsch geschrieben, kann der Code sie perfekt erfüllen und trotzdem nutzlos sein. Lean hat die Korrektheit eines Beweises in etwas verwandelt, das einem automatischen Test ähnelt, schnell und zuverlässig. Die Frage hat sich zur Spezifikation verschoben: ob die formale Aussage das Problem ist, das uns wichtig ist, und was uns der Beweis lehrt, außer dass die Aussage wahr ist.

Deshalb ist die Zahl, die man in den kommenden Monaten verfolgen sollte, nicht 722. Drei andere werden mehr aussagen:

• Wie viele formale Aussagen jemand aus dem Fachgebiet prüft, angefangen bei denen, die sich auf eigene Definitionen stützen.
• Wie viele Ergebnisse ersten Ranges eine Begutachtung durch Fachleute erhalten, vor allem die ohne Lean, wie Hodge.
• Wie viele Korrekturen die Versionsgeschichte verzeichnet. Ein Repository dieser Größe ohne Fehler wäre verdächtiger als eines mit Fehlern.

Wachsen diese Zahlen, wird diese Veröffentlichung dazu gedient haben, dass die Gemeinschaft echte Ergebnisse aufnimmt. Wachsen sie nicht, haben wir Hunderte Sätze, von denen wir nur wissen, dass eine Maschine sie für wahr erklärt.

Quellen

• OpenAI: „Sharing AI progress in mathematics“, 6. Oktober 2026.
• Repository openai/math: README, Katalog der Manuskripte, Katalog der Formalisierungen, Umfang der Formalisierung der Quasi-Riemann-Hypothese und Comparator-Challenge. Commit adc7f124, abgerufen am 7. Oktober 2026.
• AGMAI: Empfehlungen vom 29. September 2026 und Erklärung vom 6. Oktober.
• Lance Fortnow: „Open No More“, 7. Oktober 2026.
• Quanta Magazine: Wettlauf um die Unique-Games-Vermutung, 7. Oktober 2026.
• Scientific American: Reaktionen von Sutherland und Litt, 6. Oktober 2026.
• Elliott Lieb: „Problem A“, Liste offener Probleme der mathematischen Physik, 1999.
• Unabhängige erneute Kompilierungen des Bereichs ab 7/8: Zhang-Liao/quasi-riemann und davegoldblatt/openai-zeta-proof-check. Sie prüfen den formalen Beweis, nicht den Artikel.
• Gemeinschaftlicher Katalog vibemathed: Import der Ergebnisse von OpenAI.

Redaktioneller Hinweis: Wir haben keines der Ergebnisse geprüft. Die mathematischen Beschreibungen sind für Leserinnen und Leser ohne Fachkenntnis vereinfacht und geben wieder, was OpenAI behauptet, keinen Konsens der Gemeinschaft.