Nur wenige Wochen nach dem weltweiten Disput um angebliche Beweise für die Navier-Stokes-Gleichungen vollzieht OpenAI eine radikale Kehrtwende in seiner Publikationspolitik. Das Unternehmen hat ein öffentliches GitHub-Repository namens openai/math freigeschaltet, das 722 mathematische Manuskripte in 372 Problemfamilien umfasst. Sämtliche Arbeiten wurden von einem bislang unberührten, internen Frontier-Modell generiert - begleitet von 162 formalisierten Beweisen im computergestützten Beweisassistenten Lean.
Der Schritt markiert eine direkte Reaktion auf den massiven Widerstand der mathematischen Forschungsgemeinschaft. Nachdem 25 führende Mathematiker und Fields-Medaillenträger im September scharfe Transparenzregeln für KI-generierte Forschung gefordert hatten, suchte OpenAI den Schulterschluss mit dem neugegründeten Beirat am Institute for Advanced Study (IAS). Wie das Unternehmen in seinem Blogbeitrag einräumt, folgt die Veröffentlichung auf GitHub direkt den Leitlinien dieses Gremiums, das nach dem Streit um das Navier-Stokes-Problem und der Einberufung des IAS-Beirats ins Leben gerufen wurde.
4.000 Probleme und drei Stunden Rechenzeit pro Durchbruch
Nach Angaben von OpenAI entstand die Sammlung im Rahmen interner Modellevaluationen, nachdem herkömmliche mathematische Benchmarks wie GSM8K oder MATH vollständig saturiert waren. Das Entwicklerteam stellte dem Modell rund 4.000 offene oder anspruchsvolle Forschungsprobleme. Für jedes erfolgreiche Manuskript habe das Modell durchschnittlich die Rechenleistung von etwa drei Stunden ununterbrochener Denkzeit im Modus von ChatGPT Pro beansprucht.
Die Bandbreite der behandelten Disziplinen reicht von der algebraischen Geometrie über die Zahlentheorie bis zur theoretischen Informatik. Zu den herausragenden Ergebnissen zählt Familie 002 mit Fortschritten zur Birch-Swinnerton-Dyer-Vermutung (BSD), einem der sieben renommierten Millennium-Probleme der Mathematik. Das Modell beansprucht hierbei eine vollständige Leitterm-Formel für elliptische Kurven über den rationalen Zahlen bei niedrigem Selmer-Korank. Ebenfalls im Katalog enthalten sind neue Schranken für die Quasi-Riemann-Hypothese (Familie 003), bei der eine nullstellenfreie Region für die Zeta-Funktion hergeleitet wird, sowie Beweise zur Hodge-Vermutung für spezielle abelsche Varietäten (Familie 032).
Das GitHub-Repository im Überblick
Umfang: 722 Manuskripte gegliedert in 372 thematische Familien.
Modell: Unveröffentlichtes internes Frontier-Modell von OpenAI.
Rechenaufwand: Rund drei Stunden Pro-Denkzeit pro akzeptiertem Ergebnis.
Verifikation: 162 Arbeiten verfügen bereits über einen formalen Lean-Code.
Lean als digitaler Notar gegen Halluzinationen
Der entscheidende Unterschied zu früheren Behauptungen liegt in der formalen Verifikation. Frühere KI-Generierungen litten unter dem Problem subtiler logischer Lücken, die menschlichen Prüfern erst nach Tagen mühsamer Lektüre auffielen. Durch die Programmierung in der formalen Beweissprache Lean prüft ein Compiler jeden einzelnen logischen Beweisschritt automatisch auf mathematische Korrektheit ab, ähnlich wie eine Software vor dem Ausführen auf Syntaxfehler geprüft wird.
OpenAI betont jedoch selbst, dass längst nicht alle 722 Manuskripte diesen Goldstandard erfüllen. Nur für einen Teil der Arbeiten liegt bereits ein vollständiger Lean-Code vor. Für die übrigen, rein in mathematischer Fachprosa verfassten Preprints schließt OpenAI Fehler ausdrücklich nicht aus und ruft die wissenschaftliche Gemeinschaft auf, Auffälligkeiten im Repository zu melden. Um diesen Austausch zu strukturieren, stellt das Labor standardisierte Zitations- und Revisionsprotokolle bereit und kündigte an, Workshops sowie Fachkonferenzen finanziell zu fördern.
Wissenschaftliche Begeisterung trifft auf akute Prüfungsnot
In der internationalen Mathematik-Gemeinschaft löst die Veröffentlichung ein geteiltes Echo aus. Einerseits anerkennen Forscher, dass OpenAI mit der Offenlegung des Quellcodes und der Rohdaten den konstruktiven Dialog sucht. Andererseits wirft die schiere Menge an Veröffentlichungen grundlegende Fragen auf: Kaum eine Fakultät verfügt über die personellen Kapazitäten, Hunderte anspruchsvoller Beweise zeitnah manuell nachzurechnen.
Kritiker weisen zudem darauf hin, dass das zugrundeliegende Modell weiterhin unter Verschluss bleibt. Die akademische Welt werde faktisch dazu eingeladen, als unbezahlte Qualitätskontrolle für ein proprietäres System zu fungieren. Dennoch demonstriert der Schritt eindrucksvoll, wie sich die Grenze des maschinellen Schließens verschoben hat: Wo Sprachmodelle vor zwei Jahren noch an einfacher Prozentrechnung scheiterten, dringen spezialisierte Reasoning-Architekturen nun im industriellen Maßstab in das Terrain der Grundlagenforschung vor.
🎯 Was das für die Praxis bedeutet
1. Formale Verifikation wird Industriestandard: Die Kombination aus generativer Hypothesenfindung und maschineller Beweisprüfung in Systemen wie Lean verlässt den akademischen Elfenbeinturm. Für Unternehmen wird dieses Muster zum Vorbild, um KI-Ergebnisse in regulierten Bereichen wie Chipdesign, Smart-Contract-Audits und Leitsoftware mathematisch abzusichern.
2. Test-Time-Compute schlägt Modellgröße: Dass OpenAI im Schnitt drei Stunden Denkzeit pro mathematischem Resultat investierte, unterstreicht den grundlegenden Wandel der Rechenlogik. Statt nur Milliarden für das Vortraining auszugeben, wird gezielte Inferenzzeit zur primären Quelle für logische Tiefe und neuartige Problemlösungen.
3. Druck auf Closed-Source-Forschung wächst: Nach der Navier-Stokes-Kontroverse beweist dieser Fall, dass wissenschaftliche Glaubwürdigkeit ohne reproduzierbare Daten nicht mehr durchsetzbar ist. Unternehmen, die KI-Durchbrüche für sich reklamieren, müssen künftig überprüfbare Artefakte liefern.
