OpenAI hat drei mathematische Manuskripte zurückgezogen, einen Tag nachdem das Unternehmen 719 KI-erzeugte Arbeiten veröffentlicht hatte. Ein einziger Vorzeichenfehler riss zwei darauf aufbauende Beweise mit. Maschinell geprüft sind bisher 42 Prozent der Hauptergebnisse.
drweb.de als bevorzugte Quelle auf Google hinzufügenQualitätsgeprüfte Inhalte direkt in Google News & DiscoverJetzt hinzufügen
„Mehr als 700 Dateien auf einmal zu veröffentlichen, ist keine Demonstration von Gelehrsamkeit, sondern eine Demonstration von Macht“: So kommentiert die Association for Human Mathematics die mathematischen Ergebnisse, die OpenAI am 6. Oktober freigab.[1] Am 7. Oktober zog OpenAI drei davon zurück und überarbeitete 14 weitere.[2]
Das Wichtigste in Kürze
- OpenAI veröffentlichte am 6. Oktober 719 Manuskripte zu 372 Problemfamilien, erzeugt von einem unveröffentlichten internen Modell.
- Einen Tag später zog OpenAI drei Arbeiten zur Hodge-Vermutung zurück, ausgelöst durch einen Vorzeichenfehler.
- Für 300 der 719 Hauptergebnisse liegt ein Beweis im Beweisassistenten Lean vor, die zurückgezogenen Arbeiten gehören nicht dazu.
- Die Association for Human Mathematics ruft Mathematiker auf, die Zusammenarbeit mit OpenAI zu beenden.
Wie kann ein einziger Vorzeichenfehler drei Arbeiten kippen?
In der Arbeit über Weil-Klassen auf abelschen Varietäten der Dimension acht macht ein falsches Vorzeichen ein zentrales Kürzungsargument ungültig. Auf derselben Konstruktion bauten zwei weitere Manuskripte auf, darunter ein Beweis der rationalen Hodge-Vermutung für Produkte von K3-Flächen. OpenAI hat alle drei zurückgezogen, die archivierten Fassungen bleiben mit einem Hinweis auf die Lücke abrufbar.[2]
Die Abhängigkeiten reichen weiter: 14 andere Manuskripte überarbeitete OpenAI mit reparierten Beweisschritten und präziseren Annahmen, 13 zitieren jetzt die korrigierten Fassungen.[2] Softwareentwickler kennen das Muster aus Paketketten, in denen ein Fehler in einer Basisbibliothek bis in jedes abhängige Projekt durchschlägt.
Ein internes Modell erzeugte die Sammlung, nachdem OpenAI ihm rund 4.000 offene Probleme vorgelegt hatte. Im Schnitt steckten in jedem Ergebnis drei Stunden Rechenzeit im Denkmodus von ChatGPT Pro.[3] Bereits im September hatte OpenAI einen Beweis zu den Navier-Stokes-Gleichungen gemeldet, einem der sieben Millennium-Probleme.
Warum schützt der Lean-Beweis nur einen Teil der Ergebnisse?
Der Beweisassistent Lean prüft jeden Schritt eines Beweises maschinell, ein Vorzeichenfehler bliebe dort nicht unentdeckt. Bei 300 von 719 Hauptergebnissen liegt eine solche Formalisierung vor, die Hodge-Arbeiten gehören nicht dazu. OpenAI räumt im Repository selbst ein, dass nicht formalisierte Ergebnisse Fehler enthalten könnten.[3] Unser Hintergrund zur KI in der Mathematik erklärt, warum Beweisassistenten das Erzeugen vom Prüfen trennen.
Peter Scholze von der Universität Bonn bat Ende 2020 die Lean-Gemeinschaft, einen zentralen Satz seiner Arbeit mit Dustin Clausen formal nachzuprüfen. Vollständig verifiziert war der Beweis erst am 14. Juli 2022, nach anderthalb Jahren Gemeinschaftsarbeit.[4] OpenAI legt dagegen 419 Hauptergebnisse ohne maschinelle Prüfung vor.
Wie wirkte der Vorzeichenfehler?
OpenAI veröffentlicht 719 Manuskripte, doch nur 42 Prozent haben einen Maschinenbeweis. Für die Formalisierung eines einzigen Satzes von Clausen und Scholze brauchte die Fachwelt anderthalb Jahre.
Michael Dobler, Herausgeber Dr. Web
Was folgt daraus für Unternehmen, die KI-Ergebnisse nutzen?
Die Association for Human Mathematics ruft Mathematiker auf, die Zusammenarbeit mit OpenAI zu beenden, und verweist auf eine Beratergruppe, die von solchen Tests an internen Modellen abgeraten hatte.[1] Für Unternehmen stellt sich dieselbe Frage im Kleinen: Ein KI-Modell erzeugt Berichte, Verträge und Programmcode schneller, als Fachleute die Ergebnisse prüfen können. Zwei Regeln helfen:
- Prüfquote festlegen: Legen Sie gerne vorab fest, welcher Anteil KI-erzeugter Ergebnisse von Fachleuten oder Werkzeugen geprüft wird, bevor er in Entscheidungen einfließt.
- Abhängigkeiten dokumentieren: Halten Sie fest, welche Arbeiten auf welchen KI-Vorlagen aufbauen. Fällt eine Grundlage weg, finden Sie die betroffenen Folgearbeiten sofort.
Für Programmcode existiert der Maschinenbeweis schon als Werkzeug: Mistral bietet mit Leanstral 1.5 eine offene Beweis-KI an. Vitalik Buterin warnt bereits, dass KI-gestützte Mathematik gängige Verschlüsselung schwächen könnte, weitere Meldungen bündelt die Rubrik Künstliche Intelligenz. Für Ihre Praxis gilt: Ein KI-Ergebnis ist ein Entwurf, bis ein Mensch oder ein Prüfwerkzeug das Ergebnis abgenommen hat.
Quellen
[1] Association for Human Mathematics: AHM Statement on OpenAI’s October 6 Release of Mathematical Documents
[2] OpenAI: openai/math, History (Eintrag vom 7. Oktober 2026)
[3] OpenAI: openai/math, Readme
[4] Lean Community: Completion of the Liquid Tensor Experiment (15. Juli 2022)
Mehr Newshunger?
- Vitalik Buterin warnt vor KI-Angriffen auf die Gitter-Kryptografie, die das BSI empfiehlt
- OpenAI meldet Beweis für ein Millennium-Problem der Mathematik
- GPT-5.6 Sol Ultra legt einen Beweis für die 50 Jahre alte Cycle-Double-Cover-Vermutung vor
- Leanstral 1.5: Mistrals offene KI prüft Code für 3,50 Euro je Aufgabe
- Wie KI in der Mathematik die Grundlagen des Fachs erschüttert
- OpenAI-Modell löst 80 Jahre altes Mathematik-Problem
