OpenAI تنشر 722 ورقة رياضيات من نموذج داخلي، و162 منها فقط ببرهان يتحقق منه الحاسوب
المغزى: الرقم المهم ليس عدد الأوراق بل نسبة ما تحقق منه الحاسوب، نحو 22%، والباقي يظل دعوى تنتظر مراجعة بشرية باعتراف الشركة نفسها.
نشرت OpenAI، في 6 أكتوبر 2026، مستودعًا عامًا على GitHub يضم 722 ورقة رياضيات مرتبة في 372 عائلة، أنتجها نموذج داخلي لم يُعلَن عنه. وبحسب ملف README في المستودع، طُرحت على النموذج نحو 4,000 مسألة، واستهلكت كل نتيجة في المتوسط ثلاث ساعات من حوسبة التفكير في ChatGPT Pro.
ومن النتائج المعلنة كسر حدّ وضعه Harvey وvan der Hoeven عام 2019 لسرعة ضرب الأعداد الصحيحة.
لكن الرقم الأهم في المستودع هو 162، وهو عدد الأوراق التي لها نتيجة رئيسية مكتوبة بلغة Lean، بحسب ملف الـ formalization الذي يصف نفسه بأنه فهرس للأوراق ذات النتيجة المُفرَّغة. أي نحو 22% من المجموع.
ولغة Lean لغة برهان رياضي. والفرق بين البرهان فيها والورقة العادية أن الحاسوب يدقق كل خطوة، فإما أن يمر البرهان وإما أن يسقط. أما الورقة غير المُفرَّغة في Lean فتبقى دعوى إلى أن يراجعها إنسان.
وتقول OpenAI ذلك بنفسها في ملف README: “بعض النتائج غير المُفرَّغة قد تكون فيها مشكلات”. كما يذكر ملف الـ formalization أن طريقة الإنتاج هي agent، وأن حالة المراجعة unchecked.
وبذلك تظهر في المستودع سلسلة تحقق متدرجة: 4,000 مسألة، ثم 722 ورقة، ثم 162 برهانًا يمر على الآلة. وهي امتداد لمسار بدأ مع إعلان OpenAI عن Astra ونتائجه في Lean، وللنقاش الذي فتحته وثيقة مجتمع الرياضيات عن معايير نشر نتائج الذكاء الاصطناعي.
والفارق يتجاوز الرياضيات. فمخرجات النماذج في العمل البرمجي اليومي لا تملك في الغالب أداة مثل Lean، ولا درجة تحقق معلنة، بل تجربة سريعة ثم ثقة. والسلسلة التي نشرتها OpenAI تبيّن كم يتبقى من الإنتاج حين يُشترط فيه التحقق الآلي.