OpenAI Math ist ein von FineEnvs im Jahr 2026 veröffentlichtes Datenset für den Beweis mathematischer Theoreme, das OpenAIs mathematische Ergebnisse in Lean-Formalisierungsumgebungen für Theorembeweise aufbereitet. Es zielt darauf ab, Agenten streng verifizierbare Aufgaben zur formalen Beweisführung mathematischer Theoreme bereitzustellen.

Das Datenset umfasst 369 End-to-End verifizierte Harbor-Task-Umgebungen. Diese basieren auf 405 Ergebnissen aus dem OpenAI-Projekt openai/math, die als Lean-Theoremaussagen formalisiert wurden, und decken 214 Ergebnisfamilien sowie 17 mathematische Fachgebiete ab.

Das Datenset nutzt einen experimentellen Verifizierungsfilter, der nur solche Aufgaben aufnimmt, bei denen die ursprünglichen Beweise von OpenAI die Verifizierung in der jeweiligen Umgebung bestehen. Agenten müssen in einer vorkonfigurierten Sandbox-Umgebung mit Lean 4 und Mathlib die mit sorry markierten Beweisplatzhalter ausfüllen, um den vollständigen Beweis der ursprünglichen Theoreme abzuschließen.

Nach Abschluss der Aufgabe überprüft der Verifizierer die Beweisergebnisse in einer separaten Sandbox: Die Theoremaussage muss exakt mit der Originalversion übereinstimmen, es dürfen keine unvollständigen sorry-Platzhalter vorhanden sein, es dürfen ausschließlich die Standard-Axiome von Lean verwendet werden, und der Beweis muss die Lean-Kernverifizierung bestehen. Bei erfolgreicher Verifizierung wird eine Belohnung von 1 vergeben, andernfalls eine Belohnung von 0.

Jede Aufgabe ist standardmäßig mit 4 CPU-Kernen, 8 GB RAM und 10 GB Speicherplatz konfiguriert. Das Zeitlimit für die Ausführung beträgt 4 Stunden.

Zusammensetzung des Datensets

• Verzeichnis tasks: Für jede verifizierte Frage gibt es eine Harbor-Aufgabe, die die Aufgabenbeschreibung, die Lean-Theoremaussage, das Sandbox-Image-Rezept, den Verifizierer und einen Referenz-Solver enthält.
• registry.json: Harbor-Registrierungseintrag [email protected].
• manifest.parquet: Eine Zeile pro Aufgabe mit Feldern wie Fachgebiet, Ergebnisfamilie, Theoremname, Größe des Referenzbeweises und oracle result.
• Verzeichnis generator: Code zum Erstellen der Sandbox-Images und zur erneuten Generierung der Aufgaben aus openai/math.
• LICENSE, NOTICE und LICENSE-openai-math: Lizenz- und Herkunftsangaben.