OpenAI Math هي مجموعة بيانات لإثبات النظريات الرياضية، أصدرتها FineEnvs في عام 2026، تنظم نتائج OpenAI الرياضية كبيئة لإثبات النظريات الشكلية باستخدام Lean، بهدف توفير مهام لإثبات النظريات الرياضية الشكلية قابلة للتحقق بدقة للوكلاء الذكيين.

تحتوي هذه المجموعة على 369 بيئة مهمة Harbor تم التحقق منها بشكل متكامل، مستمدة من 405 نتائج في مشروع OpenAI openai/math تم تحويلها إلى صيغ نظرية Lean، وتغطي 214 عائلة من النتائج و17 مجالاً رياضياً.

تعتمد المجموعة آلية تجريبية للتحقق والاختيار، حيث تُدرج فقط المهام التي تنجح فيها البراهين الأصلية من OpenAI في اجتياز التحقق ضمن البيئة المقابلة. يحتاج الوكيل الذكي إلى إكمال البراهين في بيئة معزولة مُهيأة مسبقاً باستخدام Lean 4 و Mathlib، من خلال استبدال العناصر النائبة للبرهان المُميّزة بـ sorry لإكمال البرهان الكامل للنظرية الأصلية.

بعد إكمال المهمة، يقوم التحقق بفحص نتائج البرهان في بيئة معزولة منفصلة: يجب أن يتطابق بيان النظرية تماماً مع النسخة الأصلية، وألا توجد عناصر نائبة غير مكتملة من نوع sorry، وأن يستخدم البرهان البديهيات القياسية لـ Lean فقط، وأن يجتاز التحقق عبر نواة Lean. يحصل الوكيل على مكافأة 1 عند النجاح في التحقق، و 0 في الحالات الأخرى.

يتم تكوين كل مهمة افتراضياً بـ 4 نوى من وحدة المعالجة المركزية، و 8 جيجابايت من الذاكرة، و 10 جيجابايت من مساحة القرص، مع حد زمني للتنفيذ يبلغ 4 ساعات.

تكوين مجموعة البيانات

• مجلد tasks: كل مسألة نجحت في التحقق تقابل مهمة Harbor واحدة، وتتضمن وصف المهمة، وبيان نظرية Lean، ووصفة صورة البيئة المعزولة، وأداة التحقق، والحل المرجعي.
• registry.json: مدخل سجل Harbor [email protected].
• manifest.parquet: صف واحد لكل مهمة، يشمل الحقول المجال، وعائلة النتائج، واسم النظرية، وحجم البرهان المرجعي، ونتيجة oracle.
• مجلد generator: الكود اللازم لبناء صور البيئة المعزولة وإعادة توليد المهام من openai/math.
• ملفات LICENSE و NOTICE و LICENSE-openai-math: معلومات الترخيص والنسبة.