OpenAI Math est un ensemble de données de preuve de théorèmes mathématiques publié par FineEnvs en 2026, qui organise les résultats mathématiques d'OpenAI en environnements de preuve de théorèmes formalisés en Lean, visant à fournir aux agents des tâches de preuve de théorèmes mathématiques formels pouvant être strictement vérifiés.

Cet ensemble de données contient 369 environnements de tâches Harbor vérifiés de bout en bout, issus de 405 résultats formalisés en énoncés de théorèmes Lean dans le projet openai/math d'OpenAI, couvrant 214 familles de résultats et 17 domaines mathématiques.

L'ensemble de données adopte un mécanisme de sélection par vérification expérimentale, n'incluant que les tâches pour lesquelles les preuves originales d'OpenAI réussissent la vérification dans les environnements correspondants. Les agents doivent compléter les espaces réservés de preuve marqués par sorry dans des environnements bac à sable préconfigurés avec Lean 4 et Mathlib, afin de réaliser la preuve complète des théorèmes originaux.

Une fois la tâche terminée, le vérificateur contrôle les résultats de la preuve dans un bac à sable indépendant : l'énoncé du théorème doit être identique à la version originale, aucun sorry ne doit rester inachevé, seuls les axiomes standards de Lean doivent être utilisés, et la preuve doit passer la vérification par le noyau Lean. Une vérification réussie attribue une récompense de 1, sinon la récompense est de 0.

Chaque tâche est configurée par défaut avec 4 cœurs CPU, 8 Go de mémoire, 10 Go d'espace disque, et une limite d'exécution de 4 heures.

Composition de l'ensemble de données

• Répertoire tasks : chaque problème vérifié correspond à une tâche Harbor, contenant la description de la tâche, l'énoncé du théorème Lean, la recette de l'image du bac à sable, le vérificateur et le solveur de référence.
• registry.json : entrée du registre Harbor [email protected].
• manifest.parquet : une ligne par tâche, avec des champs incluant le domaine, la famille de résultats, le nom du théorème, la taille de la preuve de référence et le résultat oracle.
• Répertoire generator : code nécessaire pour construire les images de bac à sable et régénérer les tâches à partir de openai/math.
• LICENSE, NOTICE et LICENSE-openai-math : informations sur les licences et les attributions.