OpenAIs Mathematikveröffentlichung vom 6. Oktober stellt eine öffentliche Sammlung mit 722 Manuskripten bereit, die in 372 Ergebnisfamilien gegliedert sind. Eine Familie kann mehrere Arbeiten umfassen, während ein formaler Beweis eine engere Aussage abdecken kann als das zugehörige Manuskript. Wer einer Arbeit im Repository bis zu ihrer Beweiskonfiguration folgt, erkennt, welche Aussage zur Prüfung ausgewählt wurde.

BIG CHANGE hat am 7. Oktober das vollständige Dateiinventar des Repositorys, den Katalog und ausgewählte Beweisartefakte untersucht. Dies ist eine dokumentarische und statische Artefaktanalyse; wir haben weder die Lean-Bibliothek kompiliert noch einen Beweisprüfer ausgeführt oder die Mathematik begutachtet. OpenAIs Ankündigung beschreibt eine fortlaufend wachsende Veröffentlichung und kündigt weitere Formalisierungen an.

Die große Veränderung

  • Was sich geändert hat:Forschende können nun Hunderte KI-generierte Manuskripte über einen gemeinsamen öffentlichen Katalog bis zu unterstützenden Dateien und bei einigen Ergebnissen bis zu formalen Aussagen und vorgeschlagenen Beweisimplementierungen verfolgen.
  • Warum das wichtig ist:Mathematikerinnen und Mathematiker, die ein Ergebnis verwenden möchten, können die tatsächlich zur Prüfung ausgewählte Aussage, ihre Annahmen und ihren Bezug zur Arbeit untersuchen. Die Struktur des Repositorys hilft zu erkennen, wo ein engeres formales Ergebnis endet und eine weitergehende mathematische Prüfung beginnt.
  • Worauf es ankommt:OpenAI plant weitere Formalisierungen und will Revisionen aufbewahren. Für alle, die diese Arbeit zitieren oder darauf aufbauen, sind solche Aktualisierungen relevant: Eine Prüfung sollte die untersuchte Version und den Satz benennen.

Manuskripte und Familien getrennt zählen

Unser Inventar fand 722 unmittelbare Manuskriptverzeichnisse unter preprints/; jedes enthält ein PDF. Unter reasoning_traces/ lagen weitere 10 PDFs. Die Manuskriptkarte enthält 372 Einträge eigenständiger Familien und Links zu 722 Manuskripten.

Diese Zahlen beschreiben unterschiedliche Objekte:

Artefakt

Was Lesende untersuchen können

Ergebnisfamilie

Eine Gruppe verwandter Arbeiten, etwa mit ergänzenden Argumenten, Folgerungen oder alternativen Beweisen.

Manuskript

Ein einzelnes mathematisches Dokument mit eigenen Quelldateien und Zitationsangaben.

Zusammenfassung der Überlegungen

Eine gekürzte Darstellung der Überlegungen des Modells zu einem ausgewählten Ergebnis.

Lean-Artefakt

Formale Definitionen, Aussagen und vorgeschlagene Beweise mit Links und Konfigurationen, die festlegen, was geprüft werden soll.

Die README des Repositorys erklärt diese Kategorien und warnt vor dem uneinheitlichen Verifikationsstand. Für einige Ergebnisse gibt es keine Lean-Formalisierung; laut OpenAI kann nicht formalisiertes Material Probleme enthalten. Der Formalisierungskatalog vermerkt den Umfang als "Partial progress" und den Prüfstatus als unchecked. Das sind Veröffentlichungsmetadaten, kein von BIG CHANGE ausgeführtes Prüfergebnis.

Die öffentlichen Dateien lassen sich ohne OpenAI-Konto lesen. In der Ankündigung wird das erzeugende Modell als intern bezeichnet; OpenAI arbeite daran, es zu veröffentlichen. Der Zugang zu diesen Dokumenten belegt daher keinen Zugang zu diesem Modell.

Version festhalten, bevor Sie einem Beweis folgen

Der hier verwendete Repository-Snapshot entspricht Commit adc7f1241b42e322a6451854ab7e4b4c146bf78a vom 6. Oktober 2026 um 21:58:50 UTC. Links mit dieser Kennung bewahren den untersuchten Snapshot; Links mit main folgen dem veränderlichen Standardbranch. OpenAIs README verspricht, frühere Veröffentlichungen bei Korrekturen oder Revisionen aufzubewahren.

Beginnen Sie mit der Übersicht, die Familien nach mathematischen Themen ordnet. Nutzen Sie dann die Manuskriptkarte, um eine bestimmte Arbeit aufzurufen. Notieren Sie ihr Verzeichnis, den Repository-Commit und die angegebene Zitation. Das Manuskriptdatum kann vom Veröffentlichungsdatum der öffentlichen Sammlung abweichen.

Familie 003 enthält eine Arbeit mit der Behauptung eines nullstellenfreien Bereichs rechts von 7/8, einen alternativen Beweis für einen Bereich rechts von 11/12 und eine separate Arbeit zu Landau-Siegel-Nullstellen. Das Verzeichnis der ersten Arbeit ist auf den 30. September datiert und enthält eine BibTeX-Zitation. Die konkrete Arbeit zu benennen, hält diese Aussagen auseinander.

Die Lean-Umfangsseite beschreibt, welche Aussagen die Formalisierung abdeckt, nennt Ausschlüsse und weist auf ausgelassene spätere Anwendungen in der Arbeit hin. Sie verlinkt separate Prüfaussagen zum Zeta-Ergebnis, zu Dirichlet- und Hecke-L-Funktionen sowie zu einer einheitlichen Lücke zwischen reellen Nullstellen. Die Prüfung einer ausgewählten Aussage steht nicht automatisch für alle Punkte dieser Seite.

Der ausgewählten Aussage bis zu ihrer Konfiguration folgen

OpenAIs Comparator-Anleitung verwendet Familie 003 als Beispiel. Comparator vergleicht einen vorgeschlagenen Lean-Beweis mit einer festgelegten Challenge. Die JSON-Konfiguration des Beispiels wählt einen Satz aus: die Nullstellenfreiheit der Riemannschen Zetafunktion, wenn der Realteil ihres Arguments größer als 7/8 ist.

Die Konfiguration verweist auf ein Challenge-Modul und ein separates Lösungsmodul. Sie erlaubt die Standardaxiome propext , Quot.sound und Classical.choice und setzt enable_nanoda auf false . Nanoda ist ein unabhängiger Prüfer, den Comparator verwenden kann; in der bereitgestellten Konfiguration ist er deaktiviert.

Die Challenge-Datei enthält sorry , Leans Platzhalter für einen unvollständigen Beweis. Er hat hier eine konkrete Funktion: Er liefert die abzugleichende Aussage. Comparators Dokumentation erlaubt einen Platzhalter in der Challenge und verlangt einen ordentlichen Beweis in der Lösung. Dass sorry allein in dieser Challenge vorkommt, sagt nichts darüber aus, ob die separate Lösung besteht. Comparators Dokumentation.

Für eine dokumentierte lokale Prüfung braucht man diese Konfiguration, ihre Challenge- und Lösungsmodule sowie deren Abhängigkeiten. Das Repository pinnt Lean 4.34.1. Das Lake-Manifest verzeichnet Abhängigkeitsrevisionen, darunter Mathlib auf Revision d13f23b723b8a846827a245b89c10fc7d3f11612.

OpenAI verlangt, dass comparator , landrun und lean4export im Suchpfad für ausführbare Dateien liegen, und dokumentiert diese Befehle anschließend aus dem Verzeichnis lean/ heraus:

Terminal
lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.json

Das sind Anweisungen des Herausgebers, keine von uns ausgeführten Befehle. Die Versionen der drei externen Werkzeuge sind nicht festgelegt. Comparators aktuelle Dokumentation verlangt eine kompatible Version von lean4export und beschreibt Sandbox-Voraussetzungen sowie die Bedingungen, unter denen ein Erfolg eine Übereinstimmung mit der Challenge, die Nutzung zulässiger Axiome und die Annahme durch den Kernel belegt. Ein reproduzierbarer Bericht sollte die installierten Werkzeugversionen und die tatsächliche Ausgabe zusammen mit dem Repository-Commit festhalten.

Die README der Lean-Bibliothek empfiehlt, kleine Teile dieser großen Bibliothek zu kompilieren. Sie dokumentiert auch Linux-Beschränkungen beim Memory-Mapping, die einen vollständigen Build verhindern können. Wir haben weder lokale Laufzeit noch Hardwarekosten dieses Beispiels gemessen.

Eine erfolgreiche Prüfung im angegebenen Umfang lesen

Der Lean-Validierungsleitfaden, bei der Abfrage in Version 4.35.0-rc3, unterscheidet die Annahme eines formalen Beweises von der Auslegung der Bedeutung des Satzes. Diese Dokumentationsversion ist getrennt von der im Repository festgelegten Toolchain.

Eine erfolgreiche einfache Prüfung bedeutet, dass der Kernel die formale Aussage unter den Definitionen, Imports und Axiomen akzeptiert hat. Abhängigkeiten können weiterhin unvollständige Beweise enthalten. Lean dokumentiert #print axioms zum Anzeigen verwendeter Axiome, darunter sorryAx für einen unvollständigen Beweis in der Abhängigkeitskette.

Strengere Prüfungen führen gespeicherte Beweise erneut aus oder vergleichen eine Lösung mit einer separat festgelegten Aussage. Auch sie hängen von der Prüfumgebung und der korrekten Darstellung der beabsichtigten Bedeutung ab. Deshalb gehören die konkrete Challenge, zulässige Axiome und Einstellungen externer Prüfer in einen Verifikationsbericht. Weder die Annahme durch den Kernel noch eine Übereinstimmung mit der Challenge belegt die Annahme durch eine Fachzeitschrift oder die Formalisierung jeder Aussage eines Manuskripts.

Die Compute-Angabe beschreibt die Generierung

OpenAI zufolge entsprach der Rechenaufwand pro Ergebnis im Durchschnitt etwa drei Stunden Denkzeit mit ChatGPT Pro. Laut README wurden bei der Evaluation rund 4.000 Probleme gestellt, die Ausgaben anschließend gruppiert und nach Bedeutung ausgewählt. Auch Ausnahmen vom üblichen Verfahren werden genannt. Das sind Unternehmensangaben zur Generierung; sie beziffern weder die Lean-Prüfung durch Lesende noch eine Gesamtrechnung in Dollar. Veröffentlichungsankündigung, Darstellung der Generierung.

Für Familie 003 benennt diese Untersuchung eine konkrete Zeta-Aussage, die vorgeschlagene Lösung und die vom Prüfer zugelassenen Axiome. Sie stellt auch fest, dass Nanoda im bereitgestellten Beispiel deaktiviert bleibt. Ob die konfigurierte Prüfung gelingt, lässt sich nur durch einen dokumentierten Lauf feststellen.

Quellen und weiterführende Lektüre

  • OpenAIs Ankündigung vom 6. OktoberBelegt Veröffentlichungsdatum, internen Modellstatus, geplante Ergänzungen und die Compute-Schätzung des Unternehmens. Es ist die Darstellung des Entwicklers über die eigene Arbeit.
  • Festgelegtes RepositoryEnthält den Katalog, Manuskriptdateien und Beweiskonfigurationen, die wir untersucht haben. Die Zahlen stammen aus dem vollständigen Inventar und der Manuskriptkarte; ausgewählte formale Dateien wurden ohne Ausführung gelesen. Zur Einordnung der Struktur haben wir den LaTeX-Quelltext der Übersicht geprüft.
  • Lean-ValidierungsleitfadenErläutert Bedeutung und Grenzen der Beweisprüfung. Wir nutzten Referenzversion 4.35.0-rc3; das OpenAI-Projekt pinnt Lean 4.34.1.
  • Comparator-DokumentationBeschreibt Challenge- und Lösungsdateien, Umgebungsanforderungen und bedingte Garantien. Sie meldet kein Verifikationsergebnis für diese Sammlung.
  • Curtis Pykes Review bei Kingy.aiBietet eine unabhängige statische Prüfung der Veröffentlichung. Sie sagt ausdrücklich, dass Lean nicht unabhängig ausgeführt wurde; wir betrachten sie nicht als Reproduktion einer Beweisprüfung.
  • Früherer BIG-CHANGE-Bericht zu KI und MathematikBehandelt die Entwicklung von Mai bis September. Dieser Artikel untersucht die Artefaktstruktur der neuen Sammlung und den Prüfprozess.