OpenAI veröffentlicht 722 Mathe-Manuskripte mit in Lean prüfbaren Beweisen
Ein internes Modell soll offene Probleme gelöst haben, und die Beweise lassen sich maschinell nachprüfen statt nur glauben.
OpenAI hat am 6. Oktober 2026 722 Mathematik-Manuskripte veröffentlicht, deren Beweise sich im Beweisassistenten Lean prüfen lassen. Verfasst hat sie ein internes Modell des Unternehmens, und sie betreffen Probleme, die bisher als offen galten. Neben OpenAI selbst berichten The Verge und heise online über die Veröffentlichung.
Was bekannt ist
Die Manuskripte stammen laut OpenAI von einem internen Modell. Einen Produktnamen oder eine Version nennt die Ankündigung im Titel der Story nicht.
Die Lösungen beziehen sich auf einen Bestand von mehreren Tausend Problemen. Für etwa ein Zehntel davon liegen nun Lösungen vor. Für den weitaus größeren Teil gibt es weiterhin keine.
Laut The Verge hat OpenAI das Material über GitHub zugänglich gemacht. Damit sind die Texte und Beweise nicht nur beschrieben, sondern abrufbar.
heise online spricht von Hunderten weiteren KI-generierten Lösungen. Die Formulierung macht deutlich, dass es nicht die erste Veröffentlichung dieser Art ist, sondern eine Fortsetzung.
Der zentrale Punkt ist die Form der Beweise. Sie lassen sich in Lean prüfen. Lean ist ein Beweisassistent: Ein Programm kontrolliert jeden einzelnen Schritt eines Beweises gegen formale Regeln. Läuft die Prüfung durch, ist der Beweis für die formal formulierte Aussage korrekt, gleichgültig, ob ihn ein Mensch oder eine Maschine geschrieben hat.
Einordnung
Meldungen, ein Sprachmodell habe ein mathematisches Problem gelöst, haben ein Grundproblem: Sie lassen sich schwer überprüfen. Ein Beweis in natürlicher Sprache muss von Fachleuten Zeile für Zeile gelesen werden, und das kostet bei Hunderten Manuskripten Monate.
Mit einer Lean-Prüfung verschiebt sich diese Last. Wer den Ergebnissen nicht traut, muss nicht dem Unternehmen glauben, sondern kann den Beweis selbst durch den Prüfer laufen lassen. Genau das trennt die Veröffentlichung von einer bloßen Leistungsbehauptung.
Gleichzeitig rückt der Anteil die große Zahl zurecht. 722 Manuskripte wirken umfangreich, decken aber nur etwa ein Zehntel des Problembestands ab. Das Modell löst also nicht beliebige offene Fragen, sondern einen kleinen Ausschnitt einer großen Sammlung.
Für die Mathematik ist das dennoch relevant. Formal geprüfte Beweise lassen sich weiterverwenden, als Bausteine für andere Arbeiten oder als Material, an dem sich Fachleute orientieren können.
Was offen ist
Die Quellen nennen weder den Namen des internen Modells noch, ob es öffentlich zugänglich werden soll. Unklar ist außerdem, ob alle 722 Manuskripte vollständig in Lean formalisiert sind und ob unabhängige Mathematikerinnen und Mathematiker die Ergebnisse bereits begutachtet haben. Eine Lean-Prüfung belegt zudem nur, dass der Beweis zur formalen Aussage passt, nicht, dass diese Aussage das ursprüngliche Problem korrekt abbildet.
Termine
-
- Oktober 2026: OpenAI veröffentlicht die 722 Mathematik-Manuskripte
