OpenAI veröffentlicht 722 Mathe-Manuskripte eines unveröffentlichten Modells
Ein internes KI-Modell von OpenAI hat Hunderte offene Mathematikprobleme bearbeitet. OpenAI stellt 722 Manuskripte in 372 Ergebnisfamilien auf GitHub, viele mit formalen Beweisen in Lean. Mathematikerinnen und Mathematiker reagieren gespalten: Beeindruckende Menge, aber kaum Zeit zum Prüfen.
Hunderte Ergebnisse auf einen Schlag
Am 6. Oktober 2026 hat OpenAI eine große Sammlung neuer mathematischer Resultate veröffentlicht. Sie stammen von einem internen Modell, das noch nicht öffentlich verfügbar ist. Laut Berichten handelt es sich um 722 Manuskripte, die in 372 Ergebnisfamilien gruppiert sind. Insgesamt bekam das Modell rund 4.000 Probleme vorgelegt. Im Schnitt hat es pro Ergebnis etwa drei Stunden Rechenzeit gebraucht, gemessen in ChatGPT-Pro-Nutzung.
Was veröffentlicht wurde
- Ort: ein öffentliches GitHub-Repository mit Regeln für Korrekturen und Zitierungen
- Formale Beweise: Für viele, aber nicht alle Beweise gibt es eine Fassung in Lean. Das ist eine Programmiersprache, mit der ein Computer jeden Beweisschritt automatisch überprüfen kann.
- Bekannte Probleme: Unter anderem geht es um eine nullstellenfreie Zone der Riemannschen Zetafunktion und einen Spezialfall der Hodge-Vermutung. Gelöst sind diese großen Vermutungen damit nicht, es sind Teilergebnisse.
- Transparenz: zehn Zusammenfassungen der Denkwege des Modells sowie Angaben zu Rechenaufwand und Zahl der Versuche
OpenAI kündigt an, Workshops und Konferenzen zu KI-erzeugten Ergebnissen zu finanzieren und das Modell verantwortungsvoll zu veröffentlichen.
Kritik aus der Mathematik
Die Beratungsgruppe für Mathematik und KI am Institute for Advanced Study, die OpenAI vorab konsultiert hat, betont: Ihre Empfehlungen seien keine Bestätigung der Ergebnisse. Die Veröffentlichung sei der Anfang, nicht das Ende der menschlichen Prüfung. Andere Forschende kritisieren, dass so viele Arbeiten auf einmal kaum sorgfältig gegengeprüft sein können. Solange niemand außerhalb von OpenAI das Modell nutzen kann, lassen sich die Ergebnisse auch nicht unabhängig wiederholen.
Einordnung
Hier zeigt sich ein Grundprinzip der Wissenschaft: Ein Ergebnis gilt erst, wenn andere es prüfen können. Formale Beweise in Lean helfen dabei enorm, weil der Computer jeden Schritt kontrolliert. Wo diese Fassung fehlt, müssen Menschen nachrechnen, und das dauert bei 722 Arbeiten sehr lange. Die eigentliche Engstelle ist damit nicht mehr das Finden von Beweisen, sondern das Verstehen und Prüfen.