نشرت شركة Google DeepMind ورقة بحثية في 24 مايو تصف حلقة عمل ذكية تعتمد على نماذج اللغات الكبيرة وتُسمى LLM-Lean، وقد تمكنت هذه الحلقة من حل 9 مسائل من أصل 353 مسألة مفتوحة ضمن مشكلة إيردوس — بعضها ظل بلا حل لأكثر من 50 عامًا — كما أثبتت صحة 44 فرضية من أصل 492 فرضية مفتوحة في قاعدة بيانات OEIS، وكل ذلك بتكلفة لا تتجاوز بضع مئات من الدولارات لكل مسألة. يجمع النظام، الذي وُصِف بالتفصيل في الرابط arxiv.org/abs/2605.22763، بين نموذج لغوي كبير لتوليد البراهين ومترجم Lean للتحقق الشكلي، الذي يتولى التحقق الميكانيكي من كل خطوة منطقية؛ ولا يتم أي مراجعة بشرية إلا بعد تأكيد Lean لصحة البرهان. وقد تمكن هذا النظام أيضًا من حل مسألة عمرها 15 عامًا في مجال الهندسة الجبرية، بالإضافة إلى اكتشاف معلمة خوارزمية جديدة في نظرية التحسين.
ومن أهم النتائج التي توصلت إليها الورقة البحثية أن وكيلًا بسيطًا يقوم بالتبديل بين توليد النصوص عبر نموذج لغوي كبير وتلقي ملاحظات من المترجم قد نجح في حل جميع المسائل التسع المتعلقة بمشكلة إيردوس؛ بينما تجاوزه النظام الكامل الذي يستخدم البحث التطوري والتعلم المعزز فقط في التعامل مع أصعب المسائل، مما يشير إلى أن تحسين النماذج الأساسية قد يكون أكثر أهمية من تعقيد الهيكل العام للنظام. وأظهر تحليل الإخفاقات أن الذكاء الاصطناعي كان يختلق في كثير من الأحيان مقدمات رياضية غير صحيحة ويخفي صعوبات أساسية عبر إعادة صياغتها كمقدمات مساعدة؛ وقد تمكن مترجم Lean من كشف هذه الأخطاء تلقائيًا، وهو ما لا يمكن للأساليب التقليدية في إثبات البراهين القيام به. وحتى الآن، تتركز النجاحات في مجالات التركيبيات ونظرية الأعداد والتحسين، حيث تكون مكتبة Lean الرياضية (Mathlib) أكثر نضجًا؛ أما المسائل التي تتطلب تطوير نظريات جديدة فلا تزال بعيدة المنال.
وأشار غاري ماركوس إلى أن هذا النهج يندرج تحت فئة الذكاء الاصطناعي العصبي-الرمزي، ووصفه بأنه “أكثر دقة وتحليلًا كميًا” مقارنةً بجهود OpenAI في إثبات البراهين بشكل غير رسمي، مما أثار تساؤلات حول ما إذا كانت OpenAI قد أسرعت في إعلاناتها علمًا بأن نتائج DeepMind كانت وشيكة. وفي المقابل، لاحظ نيت سواريس أن وسائل الإعلام الرئيسية تجاهلت هذه القصة رغم ضخامتها، مُعزياً ذلك إلى حالة “التخدّر المجتمعي” تجاه التطورات الكبرى في مجال الذكاء الاصطناعي. وقد حصد المنشور 2.6 مليون مشاهدة خلال 24 ساعة فقط.