OpenAI veröffentlichte am 6. Oktober mathematische Manuskripte eines internen Modells. Das öffentliche Repository weist auf unterschiedliche Prüfungsstände und mögliche Fehler hin. Das ist weder ein neues Modell für Nutzer noch eine Sammlung von Ergebnissen, die Neudyne fachlich bestätigt hätte.

Für einen Teil der Arbeiten gibt es Formalisierungen in Lean. Sie ermöglichen die computergestützte Prüfung präzise formulierter Aussagen. Damit ist nicht automatisch jede Formulierung im begleitenden Manuskript bestätigt. Eine Bauanleitung für die Bibliothek liegt vor; wir haben die Beweise nicht kompiliert. Wichtiger als die Anzahl der Dateien ist, ob das Prüfartefakt die behauptete Aussage tatsächlich abdeckt.

Die unabhängige Beratungsgruppe AGMAI fordert verständliche Erklärungen und menschliche Verantwortung für mathematische Inhalte. Ihre Konsultation ist deshalb kein Gütesiegel für die Richtigkeit. Ein nützlicheres Bild als die Wundermaschine: Eine Mathematikerin erhält eine neue Idee, findet eine Schwachstelle und entwickelt daraus ein verlässliches Verfahren für weitere Forschung.

Bewähren sich solche Verfahren, könnten sie bei Schranken für Optimierungsalgorithmen oder bei formal geprüften Softwarekomponenten helfen. Das ist unser realistisches Anwendungsszenario, keine nachgewiesene Nutzung dieser Sammlung. Zuerst müssen Voraussetzungen, Beziehungen zur Literatur und der Beweis selbst geprüft werden. Erst danach lässt sich der praktische Wert beurteilen.

Unsere optimistische redaktionelle Schätzung beträgt 4–12 Wochen bis zu ersten veröffentlichten Fachanalysen einzelner Aussagen, sofern passende Spezialisten sich damit befassen. Für die Anerkennung der gesamten Sammlung oder den Einsatz in Produkten lässt sich kein solcher Termin nennen. Spannend ist nicht die Geschwindigkeit der Ankündigung, sondern ob eine Idee auch außerhalb ihres Urhebers einer Prüfung standhält.