Markdown-Ausgabe

AI-translated from English; not yet reviewed by a fluent editor.

# OpenAIs Mathematik-Repository: Manuskripte, Versionen und Lean-Beweise

> OpenAIs Sammlung umfasst 722 Manuskripte in 372 Familien. Ein genauer Blick auf eine Lean-Beweiskonfiguration zeigt, wie sich Versionen, Umfang und Prüfanforderungen untersuchen lassen.

By BIG CHANGE Editorial

Published: 2026-10-07T04:13:00.689Z
Updated: 2026-10-07T04:13:00.689Z
Canonical: https://bigchange.ai/blog/openai-math-repository-manuscripts-formal-proofs

![Charcoal concept illustration of one reader holding loose manuscript folios, seen from behind, beside a second stack with an orange tab.](https://bigchange.ai/api/media/file/openai-math-manuscript-reading-hero-v1.png)
AI-generated conceptual illustration by BIG CHANGE.

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](https://openai.com/index/sharing-ai-progress-in-mathematics/) 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](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/CONTENTS.md) 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](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/README.md) 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](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/formalization.yaml) 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`](https://github.com/openai/math/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](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/overview.pdf), 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](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Quasi-Riemann-Hypothesis-September-30-2026/README.md) 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](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/003.md) 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](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/README.md) verwendet Familie 003 als Beispiel. Comparator vergleicht einen vorgeschlagenen Lean-Beweis mit einer festgelegten Challenge. Die [JSON-Konfiguration](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/QuasiRiemannHypothesis.json) 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](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/QuasiRiemannHypothesis.lean) 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](https://github.com/leanprover/comparator#readme).

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](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/lean-toolchain). Das [Lake-Manifest](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/lake-manifest.json) 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:

```sh
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](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/README.md) 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](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/), 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](https://openai.com/index/sharing-ai-progress-in-mathematics/), [Darstellung der Generierung](https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/README.md#how-the-results-were-produced).

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. Oktober](https://openai.com/index/sharing-ai-progress-in-mathematics/)Belegt 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 Repository](https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a)Enthä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-Validierungsleitfaden](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/)Erläutert Bedeutung und Grenzen der Beweisprüfung. Wir nutzten Referenzversion 4.35.0-rc3; das OpenAI-Projekt pinnt Lean 4.34.1.
- [Comparator-Dokumentation](https://github.com/leanprover/comparator#readme)Beschreibt Challenge- und Lösungsdateien, Umgebungsanforderungen und bedingte Garantien. Sie meldet kein Verifikationsergebnis für diese Sammlung.
- [Curtis Pykes Review bei Kingy.ai](https://kingy.ai/blog/openai-math-722-manuscripts-results-proofs-compute-costs/)Bietet 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 Mathematik](https://bigchange.ai/blog/ai-mathematics-unit-distance-navier-stokes)Behandelt die Entwicklung von Mai bis September. Dieser Artikel untersucht die Artefaktstruktur der neuen Sammlung und den Prüfprozess.

## Sources

- [OpenAIs Ankündigung vom 6. Oktober](https://openai.com/index/sharing-ai-progress-in-mathematics/) — Belegt Veröffentlichungsdatum, internen Modellstatus, geplante Ergänzungen und die Compute-Schätzung des Unternehmens. Es ist der Bericht des Entwicklers über die eigene Arbeit.
- [OpenAIs festgelegtes Mathematik-Repository](https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a) — Enthält Katalog, Manuskriptdateien und untersuchte Beweiskonfigurationen. Die Zahlen stammen aus dem vollständigen Inventar und der Manuskriptkarte; ausgewählte formale Dateien wurden ohne Ausführung gelesen. Zur Einordnung haben wir den LaTeX-Quelltext der Übersicht geprüft.
- [Lean-Validierungsleitfaden](https://lean-lang.org/doc/reference/4.35.0-rc3/ValidatingProofs/) — Erläutert Bedeutung und Grenzen der Beweisprüfung. Wir nutzten Referenzversion 4.35.0-rc3; das OpenAI-Projekt pinnt Lean 4.34.1.
- [Comparator-Dokumentation](https://github.com/leanprover/comparator#readme) — Beschreibt Challenge- und Lösungsdateien, Umgebungsanforderungen und bedingte Garantien. Sie meldet kein Verifikationsergebnis für diese Sammlung.
- [Curtis Pykes Review bei Kingy.ai](https://kingy.ai/blog/openai-math-722-manuscripts-results-proofs-compute-costs/) — Unabhängige statische Prüfung der Veröffentlichung. Sie hält fest, dass keine unabhängige Lean-Ausführung stattfand; wir betrachten sie nicht als Reproduktion einer Beweisprüfung.
- [Früherer BIG-CHANGE-Bericht zu KI und Mathematik](https://bigchange.ai/blog/ai-mathematics-unit-distance-navier-stokes) — Behandelt den Zeitraum von Mai bis September. Dieser Artikel untersucht Struktur und Prüfprozess der neuen Sammlung.