قدّمت شركة أوبن إيه آي عائلة نماذجها الكبرى القادمة في الأول من أوت 2026، لا عبر جدول قياسات أداء بل عبر عشر مسائل بحثية محلولة. فقد أنتجت نسخة داخلية غير مُتاحة للجمهور من النموذج — واسمه Astra — حلولاً أصلية لعشر مسائل مفتوحة في الرياضيات وعلوم الحاسوب النظرية، لم تشهد أيّ منها تقدّماً في نتيجتها الأساسية منذ عقد على الأقل. ونُشر كل حل مصحوباً بصياغة صورية بلغة Lean 4 على GitHub، إضافة إلى شرح لمسار استدلال النموذج.
وأبرز هذه النتائج هو أول بناء صريح لزمرة غير سوفية (non-sofic group)، وهو ما يحسم سؤالاً طرحه ميخائيل غروموف سنة 1999 حول ما إذا كانت كل زمرة معدودة قابلة للتقريب بتبديلات منتهية. وكتب الباحث في أوبن إيه آي سيباستيان بوبيك عند الإعلان على منصة إكس: "نعم، الزمر غير السوفية موجودة"، واصفاً النتيجة بأنها "واحدة من نتائج جميلة كثيرة أثبتها Astra، نموذجنا الكبير القادم".
أبرز النقاط
- عشر نتائج تغطي نظرية الزمر، وجبريات فون نويمان، والهندسة عالية الأبعاد، ونظرية الترميز، وتعقيد الدارات الحسابية، والتعقيد الكمومي، وتعمية الشبكات، والتوافقيات القصوى.
- كل برهان مصاغ صورياً بلغة Lean 4 ومنشور على GitHub، بحيث يمكن لبرنامج التحقق من كل خطوة منطقية بدل الاعتماد على ثقة القارئ في كاتبها.
- نحو ألفي دولار ككلفة إجمالية للرموز وفق تسعيرة واجهة Sol، أي ما يقارب مئتي دولار لكل مسألة ظلّت مفتوحة عقداً.
- مخطوطة من 249 صفحة ترافق الإصدار، مع شرح لسلسلة الاستدلال في كل نتيجة على حدة.
- Astra غير متاح. لا تسعير ولا قياسات أداء ولا موعد إطلاق، ولم يُحسم بعد ما إذا كان سيصدر باسم GPT-6 أو كإصدار فرعي.
التفاصيل
تتّسم النتائج العشر بتنوّع غير معتاد في إعلان واحد. فإلى جانب الزمرة غير السوفية، قدّم Astra دحضاً لحدسية الصلابة لدى ألان كون في نظرية جبريات فون نويمان، وبرهاناً لحدسية إيرهارت حول الحجم في كل الأبعاد، وأول تحسين للحدّ الأعلى العام لتكديس الكرات في الأبعاد العالية منذ سنة 1978 — وهو حدّ بات الآن مطابقاً لعتبة كون-إلكيس.
أما بقية النتائج فتميل إلى التعقيد والتوافقيات: حدود محسّنة أُسّياً لأحجام الشيفرات الثنائية والكروية، وحدود دنيا جديدة لدارات حسابية تحسب الدائم (permanent)، ومبرهنة تكرار متوازٍ أُسّية لكل لعبة منتهية بلاعبين متشابكين، وصعوبة تقريب بعامل كثير الحدود لمسألة أقرب متجه. كما سقطت ثلاث من مسائل إيردوش هي 146 و180 و183، والأخيرة حدّ أدنى فوق أُسّي لأعداد رامزي المثلثية متعددة الألوان.
وتوضّح أوبن إيه آي توزيع الأدوار صراحة: Astra هو من ولّد الحجج الرياضية الأساسية وصاغها صورياً، بينما تولّى باحثون بشر إعداد المخطوطات للنشر. وتقول الشركة إن نسبة تأليف هذه الحجج إلى البشر ستكون تشويهاً لكيفية إنتاجها فعلياً — وهو موقف لافت في ظل الجدل القائم حول نسبة الأعمال في الرياضيات المدعومة بالذكاء الاصطناعي.
الأثر
شهادات Lean هي ما يفصل هذا الإعلان عمّا سبقه من إعلانات الذكاء الاصطناعي في الرياضيات. فنمط الفشل المعتاد في مثل هذه الادّعاءات هو سلسلة استدلال تبدو معقولة لكنها تتجاوز بصمت الخطوة الوحيدة التي كانت مهمة فعلاً؛ ونواة Lean لا تقبل التجاوز. وبإمكان أي شخص استنساخ المستودع وإعادة التحقق من البراهين دون الحاجة إلى تصديق وصف أوبن إيه آي لها.
ورقم الكلفة يتحمّل عبئاً كبيراً في التغطية الإعلامية، وهو يستحق التدقيق. فمبلغ الألفي دولار تقريباً يغطي التشغيلات الناجحة فقط. وقد أقرّ الباحث في أوبن إيه آي نعوم براون بأن الفريق حاول مسائل كبرى أخرى دون نجاح، قائلاً: "للأسف، لا مسائل من جوائز الألفية (بعد)". وأشار أيضاً إلى أن الإنفاق على كل مسألة كان منخفضاً، ما يعني أن مزيداً من الحوسبة وقت الاختبار قد يدفع النتائج أبعد. لكن ما لا يكشفه الإعلان هو المقام: كم مسألة جُرّبت، وكم تشغيلة فشلت، وكم بلغت الفاتورة التجريبية الكاملة.
بالنسبة إلى الباحثين العاملين، التحوّل يتعلق بموقع عنق الزجاجة أكثر مما يتعلق بالمبرهنات العشر ذاتها. فأعداد رامزي لا تُطعم أحداً، وإن كانت نتيجة صعوبة مسألة أقرب متجه تمسّ أسس التعمية ما بعد الكمومية القائمة على الشبكات. التغيّر الأهم هو أن توليد برهان مرشّح لمسألة ظلّت مفتوحة عقداً صار له سعر معلن، وأن التحقق منه أصبح المهارة الأندر.
الخلفية
يأتي الإعلان في فترة متوتّرة أصلاً. ففي جويلية ساعد نموذج Claude Fable 5 من أنثروبيك في إنتاج مثال مضاد لحدسية جاكوبي، وهي مسألة عمرها 87 سنة، في الأبعاد الثالثة فما فوق — وهي نتيجة نشرها الرياضي ليفنت ألبوغه على إكس ثم صاغها مجتمع كيفن بوزارد صورياً بلغة Lean. ووصف توماس بلوم، الرياضي في مانشستر الذي يشرف على قاعدة بيانات مسائل إيردوش، إصدار Astra بأنه "خبر كبير"، وأكبر من نتائج سابقة هذه السنة.
كما اعترض بلوم على تأطير الأمر بوصفه استبدالاً للرياضيين، مشيراً إلى أن هذه الأنظمة تستند إلى أكثر من قرن من النظريات التي بناها رياضيون، وأنها دُرّبت على كل ما كتبه الرياضيون. وفي جوان 2026 نشرت مجموعة دولية "إعلان لايدن حول الذكاء الاصطناعي والرياضيات"، بمصادقة الاتحاد الرياضي الدولي، ووقّعه خلال يوم واحد أكثر من ألف باحث، بينهم تيرنس تاو وبيتر شولتسه وكيفن بوزارد وسكوت آرونسون. واعتراض الإعلان ليس على الذكاء الاصطناعي بل على التدريب دون موافقة، وتجاوز التحقق، وإغفال نسبة الأعمال إلى أصحابها — ويحذّر تحديداً من أن التقييم العلمي يتضرّر حين تُبلَّغ النتائج عبر بيانات صحفية ومدوّنات بدل الأوراق البحثية.
ما التالي
يبقى Astra غير مُطلق، ولم تنشر أوبن إيه آي أي قياسات أداء أو نافذة إطلاق. والأسئلة المفتوحة هي: هل تصمد النتائج العشر أمام مراجعة الأقران، وكيف تبدو نسبة الإخفاق غير المعلنة، وهل يتعمّم هذا النهج على ما هو أبعد من المسائل القابلة للتحقق الآلي؟ فالتحقق الصوري يعمل بسلاسة مع المبرهنات، لكن معظم الادّعاءات العلمية لا تأتي مصحوبة بنواة قادرة على رفضها.
المصدر: OpenAI