كشفت غوغل ديب مايند عن إنجاز علمي غير مسبوق بعد نجاح نظامها الذكي AlphaProof Nexus بحل 9 من أصل 353 مسألة رياضية مفتوحة من مجموعة مسائل أَردوش المشهورة، من بينها مسألتان ظلتا دون حل منذ 56 عاماً. تمثل النتائج، التي نُشرت في مخدّم الطباعة الأولية arXiv بتاريخ 21 أيار/مايو 2026، خطوة نوعية تجاه توظيف الذكاء الاصطناعي كشريك فعّال للباحثين الرياضيين، لا مجرد أداة محاكاة.
نهج تحقيق متشدد مبني على لين
الابتكار الجوهري يقوم على دمج قدرات النماذج اللغوية الكبيرة القائمة على Gemini 3.1 Pro مع نظام التحقق الشكلي Lean، وهو مساعد برهان رياضي يفحص صحة كل خطوة منطقية آلياً. تولى النظام توليد محاولات البرهان بصورة مستقلة، يليها تصحيح ذاتي مباشر عبر مترجم Lean الذي يرفض أي استنتاج غير مدعوم أو يحتوي على ثغرات منطقية. تضمن هذه الآلية التحققية عدم تسرب ما يُعرف بـ"الهلوسات" - أخطاء المنطق الشائعة لدى أنظمة الذكاء الاصطناعي - إلى النتائج النهائية.
اتبع العميل استراتيجية تكرارية بحتة: توليد محاولة برهان، فحصها شكلياً، تحليل الفشل، إجراء تحسينات، واستكشاف مسارات استدلال متعددة بصورة متزامنة. نُفّذت العمليات عبر شبكة عُملاء فرعيين مستقلين (subagents) يتبادلون الحلول الواعدة ويتخلون عن الطُّرُق المسدودة بوساطة خوارزميات تطورية. حُددت حدود العمل بـ3000 دورة (iterations)؛ تُوقف المحاولة تلقائياً إن تجاوزت هذا السقف دون تقدم ملموس.
حل مسائل مستعصية بتكلفة محدودة
حسب التقديرات المنشورة، بلغت التكلفة الحسابية لكل مسألة مُحلّة بضع مئات الدولارات فقط. غير أن هذا الرقم يُخفي استثماراً حسابياً ضخماً: اختبر العميل الكامل جميع المسائل الـ353 المشكّلة رسمياً من كتالوغ أَردوش، وامتد البحث الاستكشافي ساعات طويلة. استهلك نظام AlphaProof المساعد نحو 27.5 ساعة TPU بتكلفة 60 دولاراً لكل مسألة على معالجات v6e TPU.
من أبرز النتائج حل المسألة رقم 12(i) المطروحة سنة 1970، والتي تطلّبت بناء مجموعة لانهائية تحقّق شرطاً تقييدياً صارماً لقابلية القسمة وشرط كثافة تراكمية. ابتكر العميل برهاناً يجمع نظرية الباقي الصينية ومجموعات تتجنّب التسلسلات الحسابية الثلاثية. كذلك، حُلّت المسألة رقم 125 المفتوحة منذ 1996، عبر حجة ترقيق استقرائية تستغل التقارب الديوفانتي بين القاعدتين 3 و4.
البراهين تفوق الأعداد الأولية والهندسة الجبرية
بالتوازي، برهن النظام صحة 44 من 492 تخميناً مفتوحاً مأخوذاً من الموسوعة الإلكترونية للمتتاليات الصحيحة (OEIS). شمل البرهان حزمة من مجالات رياضية متنوعة: حلّ سؤالاً عمره 15 عاماً حول دوال هيلبرت بالهندسة الجبرية، وحسّن حداً مفتوحاً بالأمثلية المحدّبة باكتشاف جدولة معاملات خوارزمية جديدة لم تكن معروفة سابقاً. يُستخدم العميل حالياً ضمن مشاريع بحثية نشطة بمجالات التوليفات، البصريات الكمومية، نظرية الرسوم البيانية، والهندسة الجبرية.
بمراجعة دقيقة للأداء، تبين أن العميل البسيط (basic agent) - المُحرر بتبادل بسيط بين التوليد اللغوي والتحقق بلين - أعاد إنتاج جميع النجاحات الـ9 ذاتها، لكنه استهلك تكلفة أعلى بكثير على المسائل الأصعب. يفسر الباحثون هذا التباين بتقدم قدرات النماذج اللغوية الكبيرة بشكل لافت خلال العام الماضي، وقوة التغذية الراجعة الصادرة مباشرة من مُترجم البرمجة.
تحديات ثابتة ومستقبل واعد
رغم النتائج المُبهرة، بقي 97.5% من مسائل أَردوش دون حل. أظهر تحليل الإخفاقات أن العملاء غالباً ما يخفون صعوبة المسألة الجوهرية ضمن ليمات مساعدة تُعيد صياغة المشكلة بشكل هامشي، أو يقترحون ليمات "مثبتة بالأدبيات" تبيّن عند الفحص أنها هلوسات. حتى مع التحذير الصريح، استمر هذا السلوك، ما يُبرز أهمية التحقق الشكلي الشامل.
أشارت التجارب إلى عجز نماذج أصغر مثل Gemini 3.0 Flash عن حل أي مسألة، كما فشل نظام AlphaProof بذاته عند تشغيله بوضعية البحث الشجري المستقل. قاد ذلك الفريق إلى استنتاج أن التفاعل التكراري بين قدرات التوليد والتحقق المُشدَّد هو المفتاح الحاسم للنجاح، وليس فقط قوة النموذج الأحادي.
وفقاً لتصريح ديميس حاسابيس، الرئيس التنفيذي لديب مايند، لبودكاست Big Technology، يظل النظام بعيداً كل البعد عن ما يُسمى الذكاء الاصطناعي العام (AGI)، رغم الإنجازات الرياضية المُلفتة. عكست تعليقات الرياضيين المتعاونين مع الفريق نظرة متوازنة: استفادوا من المحاولات الجزئية للعميل حتى عند فشله، إذ وفّرت لهم فهماً أعمق للبنية المنطقية للمسائل، وساعدتهم على اكتشاف صياغات رسمية خاطئة (misformalizations) بكفاءة عالية.
جميع البراهين الشكلية منشورة بمستودع GitHub الرسمي، مع توفير بعض البراهين بلغة طبيعية مُبسّطة لتسهيل المراجعة الإنسانية. سُجّلت النتائج رسمياً على ويكي تيرانس تاو الخاص بمساهمات الذكاء الاصطناعي بمسائل أَردوش، ما يعكس اعترافاً مهنياً بجدية العمل وصرامته.