# OpenAI Mathematik-Beweise: Was belegt ist und was offen bleibt > OpenAI hat am 6. Oktober 2026 Ergebnisse eines nicht öffentlichen internen Modells zu offenen Mathematikproblemen auf GitHub veröffentlicht, teils mit Lean-Formalisierung. Alle Angaben stammen vom Hersteller; unabhängig begutachtet sind die nicht formalisierten Ergebnisse bisher nicht. Einen Tag später zog OpenAI laut Dr. Web drei Manuskripte zurück. Veröffentlicht: 11.10.2026 · Kategorie: Künstliche Intelligenz · Adresse: https://www.heisenberg-it.de/blog/openai-mathematik-beweise-einordnung ## Das Wichtigste in Kürze - OpenAI veröffentlichte am 6. Oktober 2026 Mathematikergebnisse eines internen, nicht öffentlichen Modells, samt Lean-Formalisierungen und Angaben zum Rechenaufwand. - Dr. Web nennt 719 Manuskripte zu 372 Problemfamilien, Hardwareluxx 722 Manuskripte; für 300 der 719 Hauptergebnisse liegt laut Dr. Web ein Lean-Beweis vor. - Lean bestätigt die formale Korrektheit eines Beweises, aber nicht Relevanz, Originalität oder automatisch die exakte Passung zum Problem. - Am 7. Oktober zog OpenAI drei Manuskripte zurück und überarbeitete 14, so Dr. Web. - Beim Navier-Stokes-Problem bestreiten Mathematiker, dass das wichtigste Problem gelöst ist; das Clay-Institut führt es als aktiv. ## Was hat OpenAI am 6. Oktober 2026 veröffentlicht? OpenAI hat Ergebnisse eines internen Frontier-Modells zu offenen Mathematikproblemen publiziert [1][2]. Das Modell ist nicht öffentlich zugänglich [1]. Die Ergebnisse liegen in einem GitHub-Repository, mit Vorgaben zur Überarbeitung und zu Quellenangaben [1]. Das Material umfasst laut OpenAI: - Lean-Formalisierungen vieler Beweise, weitere sollen folgen [1], - zehn Zusammenfassungen des Modell-Reasonings, also seiner Denkschritte [1], - Schätzungen zum Rechenaufwand [1], - Statistiken zur Zahl der versuchten Probleme [1]. OpenAI prüft nach eigenen Angaben weiterhin Alternativen zu GitHub, nämlich von der Fachgemeinschaft betriebene Plattformen [1]. Die Veröffentlichung wurde mit der Advisory Group on Mathematics and AI (AGMAI) am Institute for Advanced Study abgestimmt [1][3]. > **Achtung:** Alle Angaben dieser Veröffentlichung sind Herstellerangaben. Sie sind kein Nachweis, dass die Ergebnisse stimmen. Stand: Oktober 2026. ## Wie viele Ergebnisse sind es, und wie viele sind in Lean geprüft? Die Berichte nennen unterschiedliche Zahlen, eine verlässliche Gesamtzahl gibt es derzeit nicht. Dr. Web spricht von 719 Manuskripten zu 372 Problemfamilien, Hardwareluxx von 722 Manuskripten. Die Zahlen sind Herstellerangaben, wie Fachmedien sie wiedergeben. Welche Angabe zu den Manuskripten stimmt, ist ungeklärt. | Angabe | Wert | Beleg | |---|---|---| | Manuskripte | 719 | Dr. Web [4] | | Manuskripte | 722 | Hardwareluxx [5] | | Problemfamilien | 372 | Dr. Web [4] | | Probleme laut Meldung | 372 | WinFuture [6] | | Vorgelegte Aufgaben | rund 4.000 | Hardwareluxx, Dr. Web [5][4] | | Brauchbare Lösungen | etwa ein Zehntel der Aufgaben | Hardwareluxx [5] | | Lean-Beweise | 300 für 719 Hauptergebnisse | Dr. Web [4] | Die Zahlen lassen sich so lesen: Aus rund 4.000 Aufgaben entstanden Manuskripte zu 372 Problemfamilien. Für weniger als die Hälfte der Hauptergebnisse liegt ein Lean-Beweis vor. Der Rest ist nicht maschinell geprüft. ## Was bestätigt Lean, und was nicht? Lean bestätigt, dass ein Beweis formal fehlerfrei ist. Mehr nicht. > **Definition:** Lean ist eine Programmiersprache und ein Beweisassistent, mit dem ein Computer mathematische Beweise prüft [1]. Die Übersetzung eines Beweises in Lean heißt Formalisierung. Laut WinFuture prüft Lean nur die formale Korrektheit, nicht Relevanz oder Originalität [6]. Ein Lean-Beweis zeigt außerdem nur, dass die formalisierte Aussage stimmt. Ob sie das Problem exakt so abbildet, wie es gestellt wurde, ist eine eigene Frage. Lassen Sie das im Einzelfall von Fachleuten prüfen. > **Beispiel:** Angenommen, ein Text besteht die Rechtschreibprüfung ohne Fehler. Dann ist er noch nicht inhaltlich richtig und beantwortet vielleicht nicht die gestellte Frage. Ähnlich verhält es sich mit einem Lean-Beweis. Für die nicht formalisierten Ergebnisse gilt: OpenAI räumt laut Berichten ein, dass sie Fehler enthalten könnten [4][7]. Eine unabhängige Prüfung liegt dafür nicht vor. ## Warum hat OpenAI Arbeiten zurückgezogen? Am 7. Oktober zog OpenAI drei Manuskripte zurück und überarbeitete 14 weitere, berichtet Dr. Web [4]. Auslöser war ein Vorzeichenfehler in der Arbeit über Weil-Klassen auf abelschen Varietäten der Dimension acht [4]. Betroffen ist auch ein Beweis der rationalen Hodge-Vermutung für Produkte von K3-Flächen [4]. Die archivierten Fassungen bleiben mit Hinweis abrufbar [4]. Der genaue Inhalt der Rückzüge und Revisionen ist bisher nur durch diesen einen Bericht belegt. Das zeigt dennoch, dass auch veröffentlichte Ergebnisse Fehler enthalten können. Ob weitere Korrekturen folgen, ist offen. ## Was empfiehlt die AGMAI, und wie passt die Veröffentlichung dazu? Die AGMAI hat am 29. September 2026 Empfehlungen zur verantwortungsvollen Veröffentlichung KI-generierter Mathematik vorgelegt. Sie stützen sich auf über 600 Rückmeldungen aus der Fachgemeinschaft [3]. Zentrale Punkte: - Die AGMAI lehnt es ab, dass Labs fortgeschrittene Mathematikprobleme an unzugänglichen proprietären Modellen testen [3]. - Von Menschen verstandene Arbeiten sollen als Preprint, im Peer-Review und in Vorträgen veröffentlicht werden [3]. - Bei noch nicht verstandenen Ergebnissen sollen die Labs selbst die Literatur nach verwandten Ideen durchsuchen und diese zitieren. Die Beweise sollen sie im Stil klassischer Fachartikel aufbereiten lassen [3]. - Labs sollen das menschliche Verständnis fördern, auch finanziell. Es soll aber gemeinschaftlich und nicht vom Lab gesteuert entstehen [3]. OpenAI beruft sich auf die AGMAI und deren Empfehlungen [1]. Zugleich stammen die Ergebnisse von einem nicht öffentlichen Modell und liegen auf GitHub statt im Peer-Review. Wie gut das zu den Empfehlungen passt, bleibt umstritten. ## Warum kritisieren Mathematiker das Vorgehen? Die Kritik richtet sich auf drei Punkte: das unveröffentlichte Modell, GitHub statt Peer-Review und die schiere Masse der Resultate. Die Fachwelt reagiert laut Berichten skeptisch [7][6]. Laut The Decoder warnen 25 Fields-Medaillen-Träger, die Massenproduktion könne „fruchtbaren Boden zerstören“ [8]. Gemeint ist: Wenige Fachleute können so viele Resultate kaum prüfen und einordnen. OpenAI will künftig Konferenzen finanziell unterstützen [9][8]. ## Hat OpenAI das Navier-Stokes-Problem gelöst? OpenAI behauptet es, doch das ist umstritten und nicht anerkannt. Die Navier-Stokes-Gleichungen beschreiben die Strömung von Flüssigkeiten. Das Existenz-und-Glattheits-Problem gehört zu den Millennium-Preisproblemen des Clay Mathematics Institute, jedes ist mit einer Million US-Dollar dotiert [10][11]. Nach OpenAIs Seite vom 8. September 2026 gibt es einen analytischen Beweis samt Lean-Formalisierung. Danach kann ein anfangs ruhendes, glattes Fluid mit glatter äußerer Kraft und endlicher Energie in endlicher Zeit eine Singularität entwickeln. Das entspreche den Aussagen „C“ und „D“ der Clay-Formulierung [11]. OpenAI will das Preisgeld nicht beanspruchen [11]. Die Einordnung fällt unterschiedlich aus: - Laut Scientific American löst das Ergebnis die Clay-Formulierung („C“ mit äußerer Kraft) eindeutig. Mathematiker wie Silvestre sagen dagegen, das wichtigste Problem sei ungelöst. Drei Mathematiker zeigten, dass OpenAIs Methode nicht auf das volle Problem erweiterbar ist [12]. - Das Clay-Institut führt das Problem im September 2026 weiter als „aktiv“ [13]. - Parallel lösten Alpöge (Anthropic) und Buckmaster (NYU) laut OpenAI das erzwungene Euler-Problem [11]. Euler-Regularität betrifft Gleichungen ohne Viskosität, also ohne Zähigkeit der Flüssigkeit [11]. - Buckmaster sagt, er habe OpenAIs Beweis nicht gesehen und wisse nicht, ob seine Daten genutzt wurden [10]. Die Aussagen zu Priorität und Vorgehen stammen von Beteiligten und sind unabhängig nicht belegt. ## Wie groß war der Rechenaufwand? Im Durchschnitt entsprach der Aufwand laut OpenAI etwa drei Stunden ChatGPT-Pro-Denkzeit pro Ergebnis [1]. Für Navier-Stokes nennt OpenAI deutlich mehr [11]: - Das Training des Modells begann am 28. August, die Lösung kam am 5. September nach etwa 88 Stunden. - Die Lean-Verifikation dauerte weitere 17 Stunden mit GPT-6 Astra. - Das Multiagentensystem, also viele zusammenarbeitende KI-Instanzen, hatte etwa 10.000 gleichzeitige Agenten. - Verbraucht wurden etwa 130 Milliarden Output-Tokens und 2,7 Millionen Nachrichten. Alle Werte sind Herstellerangaben. Ob sich der Aufwand mit anderen Modellen vergleichen lässt, geben sie nicht her. ## Was bleibt offen? Offen sind vor allem diese Punkte: - Sind die nicht formalisierten Ergebnisse korrekt? Eine unabhängige Prüfung fehlt [4]. - Wie viele Manuskripte es genau sind (719 oder 722) und wie viele Problemfamilien (372) dazugehören [5][4]. - Wie das Modell heißt und ob es veröffentlicht wird [1]. - Ob die Lean-Aussagen die Probleme exakt wie gestellt abbilden [6]. - Ob das Clay-Institut das Navier-Stokes-Ergebnis anerkennt [13][11]. ## Was heißt das für Leserinnen und Leser? Die Antwort unterscheidet sich je nach Interesse: - **KI-Interessierte und Unternehmen:** Behandeln Sie die Meldung als Herstellerangabe über ein Modell, das niemand außerhalb von OpenAI nutzen kann [1]. Eine Aussage über die Leistung verfügbarer Produkte folgt daraus nicht. - **Mathematik- und Wissenschaftsinteressierte:** Trennen Sie Lean-geprüfte Beweise von nicht formalisierten. Die Lean-Dateien liegen im Repository [1]. - **Entwickler:** Lean-Formalisierungen und Reasoning-Zusammenfassungen sind öffentlich einsehbar [1]. Das Modell selbst ist es nicht. ## Fazit: Wie sollte man die Meldung lesen? Die Veröffentlichung ist eine Herstellerangabe mit teilweiser formaler Prüfung. Der Rückzug von Arbeiten und die abweichenden Zahlen zeigen, dass vieles ungeklärt ist. Belastbar werden die Ergebnisse erst durch unabhängige Begutachtung, wie sie die AGMAI-Empfehlungen vorsehen [3]. ## Häufige Fragen ### Wie heißt das Modell hinter den Ergebnissen? Ein Produktname ist nicht bekannt. OpenAI spricht von einem internen Frontier-Modell, das nicht öffentlich zugänglich ist [1]. Nur für die Lean-Verifikation beim Navier-Stokes-Ergebnis nennt OpenAI GPT-6 Astra [11]. Ob und wann das Modell veröffentlicht wird, ist offen. Auf die Ergebnisse haben Sie deshalb nur über das Repository Zugriff, nicht über das Modell. ### Bekommt OpenAI das Preisgeld von einer Million US-Dollar? Nach heutigem Stand nein. OpenAI will das Preisgeld ausdrücklich nicht beanspruchen [11]. Außerdem führt das Clay-Institut das Navier-Stokes-Problem im September 2026 weiter als aktiv [13]. Ob es das Ergebnis offiziell anerkennt, ist offen. Mathematiker bestreiten zudem, dass das wichtigste Problem gelöst ist [12]. ### Was ist ein Beweisassistent wie Lean? Ein Beweisassistent ist eine Software, mit der ein Computer mathematische Beweise Schritt für Schritt prüft. Lean ist eine Programmiersprache und ein solcher Beweisassistent [1]. Er bestätigt die formale Korrektheit, nicht aber Relevanz oder Originalität eines Ergebnisses [6]. Ob die formalisierte Aussage das Problem exakt abbildet, muss gesondert beurteilt werden. ### Werden die Ergebnisse in Fachzeitschriften veröffentlicht? Das ist bisher offen. Die Ergebnisse liegen auf GitHub, OpenAI prüft Plattformen der Fachgemeinschaft als Alternative [1]. Die AGMAI empfiehlt für von Menschen verstandene Arbeiten Preprint, Peer-Review und Vorträge [3]. OpenAI will künftig Konferenzen finanziell unterstützen [9][8]. Eine Zusage für bestimmte Zeitschriften ist nicht bekannt. ### Ist das Modell öffentlich nutzbar? Nein. Es handelt sich um ein internes, nicht öffentlich zugängliches Modell [1]. Öffentlich einsehbar sind die Ergebnisse im GitHub-Repository, darunter Lean-Formalisierungen, zehn Zusammenfassungen des Reasonings, Schätzungen zum Rechenaufwand und Statistiken zu den versuchten Problemen [1]. Ob das Modell später veröffentlicht wird, ist nicht bekannt. ## Quellen 1. [KI-Fortschritte in der Mathematik teilen](https://openai.com/de-DE/index/sharing-ai-progress-in-mathematics/) – OpenAI, 2026-10-06 2. [Sharing AI progress in mathematics](https://openai.com/index/sharing-ai-progress-in-mathematics/) – OpenAI, 2026-10-06 3. [Responsible Release of AI-Generated Mathematics (general-sep29)](https://agmai.org/general-sep29/) – AGMAI, 2026-09-29 4. [OpenAI zieht drei mathematische Ergebnisse zurück](https://www.drweb.de/openai-mathematik-beweise-zurueckgezogen/) – Dr. Web 5. [Probleme aus der Mathematik: OpenAI veröffentlicht hunderte KI-generierte Lösungen](https://www.hardwareluxx.de/index.php/news/software/anwendungsprogramme/70545-probleme-aus-der-mathematik-openai-veroeffentlicht-hunderte-ki-generierte-loesungen.html) – Hardwareluxx 6. [Mathematiker sauer: OpenAI mit KI-Lösungen für 372 Mathe-Probleme](https://winfuture.de/news,161792.html) – WinFuture 7. [Hunderte ungelöste Mathe-Probleme geknackt? OpenAIs Coup lässt Forscher kalt](https://www.webnachrichten.de/wirtschaft/ki-loest-mathe-probleme-openai-erntet-skepsis-der-wissenschaft-zr-94529318.html) – webnachrichten.de 8. [OpenAI veröffentlicht hunderte KI-generierte Mathe-Beweise auf GitHub](https://the-decoder.de/openai-veroeffentlicht-hunderte-ki-generierte-mathe-beweise-auf-github/) – The Decoder 9. [OpenAI auf GitHub: KI soll hunderte offene Mathe-Probleme gelöst haben](https://t3n.de/news/openai-ki-mathe-beweise-github-1766978/) – t3n 10. [OpenAI claims to have solved the 90-year-old Navier-Stokes math problem in 88 hours](https://www.cnbc.com/2026/09/09/openai-navier-stokes-math-problem-solved.html) – CNBC, 2026-09-09 11. [On the Navier–Stokes Millennium Prize Problem](https://openai.com/index/navier-stokes-solution/) – OpenAI, 2026-09-08 12. [Did OpenAI solve the wrong Navier-Stokes problem?](https://www.scientificamerican.com/article/did-openai-solve-the-wrong-navier-stokes-problem/) – Scientific American 13. [Navier–Stokes existence and smoothness](https://en.wikipedia.org/wiki/Navier%E2%80%93Stokes_existence_and_smoothness) – Wikipedia, 2026-09 Mit KI-Unterstützung recherchiert und geschrieben, fachlich geprüft von Hannes Ftuni am 11.10.2026. Herausgeber: Heisenberg IT GmbH, Bochum.