Axiom: أسراب من وكلاء الذكاء الاصطناعي تحققت حاسوبياً من أطول برهان في الرياضيات — تصنيف الزمر البسيطة المنتهية — خلال 24 يوماً
نشرت الشركة الناشئة صياغة رسمية بلغة Lean من نحو 43.1 مليون سطر لـ«المبرهنة الهائلة»، وأبلغت عن 34 انحرافاً لافتاً عن الأدبيات المنشورة. ولم تُعِد أي مجموعة خارجية بناءها بشكل مستقل بعد.
تقول شركة الذكاء الاصطناعي الناشئة Axiom إنها أنتجت أول برهان كامل يتحقق منه الحاسوب لـتصنيف الزمر البسيطة المنتهية (CFSG) — النتيجة التي تحصي كل «ذرّات» التناظر المنتهي، والتي يمتد برهانها البشري الأصلي على نحو 15,000 صفحة في أكثر من 500 مقالة لنحو 100 رياضي.
كيف أُنجز
بحسب تقرير Axiom في 26 أكتوبر، وجّه مهندسون ورياضيون أسراباً من عشرات وكلاء الذكاء الاصطناعي لمدة 24 يوماً (بدءاً من 1–2 أكتوبر 2026)، فأنتجوا نحو 43.1 مليون سطر من الشيفرة في مساعد البراهين Lean الذي يتحقق من كل خطوة منطقية. اتبع العمل برهان «الجيل الأول»، واعتمد على Mathlib، وقُسّم إلى 108 مراحل ونحو 380 مهمة. ومن بين ما أثبته الوكلاء أن زمرة «الوحش» (Monster) بسيطة.
ما الذي وجدته الآلات
كانت معظم المشكلات المكتشفة في الأدبيات طفيفة (أخطاء مطبعية، أخطاء في الجداول، فرضيات ساقطة)، لكن Axiom تبلّغ عن 34 انحرافاً لافتاً عن السجل المنشور. أكبرها يتعلق بـمبرهنة الزمرة غير المتوازنة: وجد الوكلاء أمثلة مضادة لخطوة في حجة جون والتر لعام 1986، فبنى الفريق مساراً بديلاً، بينها نتيجة جديدة أثبتها نظامه، بعد التشاور مع منظّري الزمر ريتشارد لايونز ورونالد سولومون. وتعد Axiom بنشر قائمة بالأخطاء.
تحفظات
يتحقق Lean من الاستنتاجات، لكن على البشر التأكد من أن الصيغ والتعريفات الرسمية تعبّر فعلاً عن المبرهنة المقصودة. وبحسب تقارير إعلامية حتى 27 أكتوبر، لم تُعِد أي مجموعة خارجية بعدُ بناء البرهان كاملاً بشكل مستقل؛ وقد نشرت Axiom المستودع وملفات البناء لإتاحة ذلك. المعلومات هنا مأخوذة من تقرير الشركة نفسها.