تُصدر Axiom Math برهان Lean لتصنيف الزمر، يتألف من 43.1 مليون سطر

قالت Axiom Math في 27 أكتوبر 2026 إنها تُصدر ما تصفه بأنه أول برهان كامل على تصنيف الزمر المنتهية البسيطة جرى التحقق منه حاسوبيًا. وقد أنجزه مهندسون ورياضيون خلال 24 يومًا، عبر توجيه أسراب من عشرات وكلاء الذكاء الاصطناعي الذين كتبوا نحو 43.1 مليون سطر من الشيفرة باستخدام مساعد البراهين Lean.

كتبت الشركة في إعلانها: «نُصدر اليوم أول برهان كامل على تصنيف الزمر المنتهية البسيطة (CFSG) جرى التحقق منه حاسوبيًا». ويحدد هذا التصنيف اللبنات الأساسية للزمر المنتهية، ويمتد البرهان الأصلي على نحو 15,000 صفحة في أكثر من 500 بحث لنحو 100 عالم رياضيات؛ وهو حجم أكسبه لقب المبرهنة الهائلة.

ما الذي أصدرته Axiom

يثبت تصنيف الزمر المنتهية البسيطة أن كل زمرة منتهية بسيطة هي زمرة دورية من رتبة أولية، أو زمرة تبديلات زوجية على خمسة رموز على الأقل، أو واحدة من ست عشرة عائلة لانهائية من زمر لي المنشأة على حقول منتهية، أو واحدة من 26 زمرة متفرقة معزولة بالضبط؛ ويشير الإعلان إلى أن بعض المؤلفين يعدّون زمرة تيتس زمرة سابعة وعشرين. أما أكبر الزمر المتفرقة، وهي زمرة الوحش، فقد أنشأها روبرت غريس عام 1980 باستخدام جبر بُعده 196,884.

امتدت جهود البشر لإثبات المبرهنة عقودًا. ففي عام 1963، أثبت والتر فايت وجون طومسون أن رتبة كل زمرة منتهية بسيطة غير أبيلية زوجية، في بحث من 255 صفحة شغل عددًا كاملًا من مجلة Pacific Journal of Mathematics. وفي عام 1972، وضع دانيال غورينشتاين برنامجًا من ست عشرة خطوة لإكمال التصنيف، وأعلن اكتماله عام 1983؛ لكن حالة الزمر شبه الرقيقة ظلت تعتمد على مخطوطة غير مكتملة لجيفري ميسون، إلى أن نشر مايكل أتشباشر وستيفن سميث معالجة من 1,221 صفحة عام 2004، فاختُتم بذلك ما أصبح يُعرف ببرهان الجيل الأول. ولا يزال برهان أكثر منهجية من الجيل الثاني، بدأه غورينشتاين وريتشارد ليونز وانضم إليهما لاحقًا رونالد سولومون وإينا كابديبوسك، غير مكتمل؛ لذلك صاغت Axiom البرهان من الجيل الأول صياغةً رسمية.

تعرض صفحة المشروع هذه الصياغة الرسمية بوصفها متبعةً لبرهان الجيل الأول، مع تحقق نواة Lean من كل خطوة منطقية، وتذكر أنها تضم 43.1 مليون سطر من Lean، و2.05 مليون تصريح، ومجموعةً تضم 715 بحثًا وكتابًا. وتقول Axiom إن خريطة البرهان التي أعدتها استندت إلى مجلدات الجيل الثاني، وإن الصياغة الرسمية تدمج نحو 1.2 مليون سطر من الشيفرة من مشروع Qiuzhen-CFSG السابق، وتعتمد على Mathlib، الذي تنسب الفضل في إنشائه إلى مئات المساهمين. ويسمي المشروع دين كيورتون وفاسيلي إيلين وبهافيك ميهتا ونيلز فوس مساهمين أساسيين، فيما يتولى ليتونغ هونغ دور الباحث الرئيسي.

يصف مستودع GitHub العام النتيجة بأنها برهان Lean4 خالٍ من استخدام sorry، ومثبت على الإصدار 4.35.0-rc3، ومبني على Mathlib ومشروع TauCeti، ولا يستخدم سوى البديهيات القياسية Classical.choice وpropext وQuot.sound، من دون native_decide. ويقول نص التصنيف الرسمي، المأخوذ من TauCeti: «كل زمرة منتهية بسيطة مماثلة لواحدة من الزمر المنشأة صراحةً في قائمة التصنيف». ويذكر ملف README أن الأمر lake build يتحقق من التطوير بأكمله، وأن تغييرات مفتوحة على أداة البناء Lake وتحسينات يعتزم الفريق المساهمة بها في المشروع الأصلي خفّضت مدة البناء إلى أقل من 24 ساعة؛ وتحمل الشيفرة ترخيص Apache-2.0.

جهد جماعي استمر 24 يومًا

في 1 أكتوبر 2026، فتحت Axiom قناة على Slack لتنسيق المشروع. وقُسّم العمل إلى 108 مراحل رئيسية ونحو 380 مهمة أصغر، استنادًا إلى أعمال سابقة باستخدام Lean وخريطة داخلية للبرهان أُعدت بالاستناد إلى الأدبيات المنشورة. وانطلق السرب الأول في 2 أكتوبر 2026، إذ تولى الوكلاء المراحل الرئيسية عبر مسائل GitHub، وأبلغوا عن إنجازاتهم في Slack. وفككت الوكلاء الرئيسيون البراهين الصعبة وراجعوا العبارات، فيما بحث وكلاء آخرون عن نتائج موجودة أو كتبوا براهين باستخدام Lean؛ وكان بإمكان أي وكيل إحالة المتطلبات السابقة الناقصة إلى وكلاء آخرين، لتُضاف نتائجهم إلى مستودع مشترك.

كشفت المراحل الأولى من التقدم عن نقاط ضعف. فقد أخفت بعض المراحل التي بدت قابلة للإنجاز متطلباتٍ مسبقة هائلة افترضها الوكلاء بدلًا من إثباتها، فحذف الفريق عشرات الآلاف من الأسطر المبنية على تلك الافتراضات قبل أن يبدأ من جديد وفق خطة أكثر متانة. وتعلقت إحدى المراحل المبكرة بمبرهنة دالة المُحدِّد، إذ استند البرهان المقترح إلى افتراضات بنيوية لا تزال بحاجة إلى تبرير. كما أصبحت أوقات البناء عائقًا عندما أخذ الوكلاء ينتجون البراهين بوتيرة أسرع مما يستطيع Lean إعادة التحقق منها. وتقول Axiom إن مهندسيها وزعوا نتائج البناء المخزنة مؤقتًا على العاملين، وأجروا عمليات تحقق مستقلة بالتوازي، ونقلوا الحسابات المنتهية المكلفة إلى شهادات يمكن التحقق منها على نحو مستقل؛ وتقول الشركة إن هذه التغييرات سرّعت التحقق بمراتب قدرية.

في 10 أكتوبر 2026، أعلنت رسالة في القناة أن الوكلاء أثبتوا بساطة زمرة الوحش، بحسب رواية الشركة. كما صاغ الوكلاء رسميًا برهان وجود زمرة الوحش من خلال جبر غريس، ومبرهنةً تحدد الزمر من نوع الوحش بأنها زمرة الوحش. وفي 13 أكتوبر 2026، لم تُنجز سوى مرحلة رئيسية واحدة، فنظم المهندسون جهدًا لإعادة التخطيط قسّموا خلاله المراحل غير المكتملة إلى مبرهنات أصغر محددة بدقة؛ وكان مطلوبًا من كل عملية تقسيم أن توضح كيف تثبت الأجزاء المبرهنة الأصلية، عبر برهان قصير باستخدام Lean.

ثغرات عُثر عليها في البرهان المنشور

أفادت Axiom بأن ترجمة البرهان إلى Lean كشفت مشكلات في الحجج المنشورة. وكان معظمها طفيفًا — أخطاء مطبعية، أو أخطاء في الجداول، أو فروضًا أُسقطت — لكن الشركة أحصت 34 اختلافًا جديرًا بالذكر عن السجل المنشور، وكان أبرزها متعلقًا بمبرهنة الزمر غير المتوازنة، أو UGT.

جاء أحد الأمثلة من مجلدات Aschbacher وSmith عن الزمر شبه النحيفة، حيث أكدت لمّة أن كميتين عدديتين متساويتان. ووجدت الوكلاء مثالًا مضادًا يتعلق بالزمرة SL₂(5)، إذ كانت إحدى الكميتين تساوي 1، في حين أن المساواة المفترضة تقتضي أن تساوي 2. وصحح استبدال المساواة بمتباينة اللمّة، لكن حججًا لاحقة كانت قد اعتمدت على المساواة لاستبعاد حالات معينة، لذلك وسّع الفريق حجة سابقة لتشمل تلك التكوينات.

تساعد مبرهنة UGT على تحديد زمرة كاملة انطلاقًا من معلومات عن زمرها الجزئية: فبحسب ملخص الورقة البحثية المصاحبة، تقتضي الفروض الاستقرائية للتصنيف أن تكون الزمرة البسيطة المحيطة من نوع لي في خاصية فردية أو زمرة تبديلية من درجات معينة، إذا وُجدت فيها زمرة جزئية غير تافهة ذات رتبة فردية، طبيعية في مُمركز عنصر من الرتبة الثانية. وتناولت Axiom المبرهنة بالاستناد إلى دراسة John Walter الصادرة عام 1986، وخلال إضفاء الصيغة الشكلية على تلك الحجة، اكتشف وكلاؤها أمثلة مضادة صريحة لادعاء الإغلاق الذي استندت إليه: إذ كان من الممكن لعملية يُفترض أن تُبقي الزمر البسيطة المرتبطة ضمن عائلة محددة أن تنتج زمرة مستبعدة منها صراحةً.

بحسب ما ترويه الشركة، تبدأ العملية من PSL₂(49)، الذي يكون مُمركز مرافقه الحقلي هو PGL₂(7)، ثم تنتج المكوّن البسيط PSL₂(7)، وهو مستبعد من العائلة لأن 7 عدد أولي من أعداد ميرسين. وتشير Axiom إلى أن الأمثلة المضادة لم تدحض مبرهنة UGT نفسها، ولا حتى نتيجة القضية II.5.9(ii) لدى Walter.

استند الإصلاح إلى نظرية Solomon لعام 1976 بشأن المكوّنات القصوى من الرتبة 2، التي تقول Axiom إنها وفرت الأفكار الأساسية لحجة بديلة أنتجها نظام AxiomProver وأضفى عليها الصيغة الشكلية. وتصف Axiom الخطوة المحورية، الواردة في الورقة بصفتها المبرهنة 2.3 (الحفاظ على القمم البسيطة)، بأنها نتيجة جديدة في نظرية الزمر أثبتها AxiomProver؛ وهي، بالاقتران مع اختزالات Gilman وSolomon ومبرهنات التعرّف لدى Foote وHarris، توفر الصيغة الخاصة بالزمر البسيطة من مبرهنة UGT اللازمة للتصنيف. وبعد إضفاء الصيغة الشكلية على البرهان، توصل علماء الرياضيات في Axiom إلى استدلال أقصر باستخدام أساليب الجيل الأول، سُجّل في الملاحظة 9.5، ويصل إلى النتيجة نفسها من دون المبرهنة 2.3.

ظهرت تلك الورقة، «مبرهنة الزمر غير المتوازنة»، التي أسهم في إعدادها Colin Defant وKen Ono، على خادم المسودات البحثية Hexagon بوصفها الإصدار 1 في 27 أكتوبر 2026، بموجب ترخيص CC BY 4.0؛ ويذكر الموقع الإلكتروني للمشروع أنها تقع في 35 صفحة. وتقول Axiom إنها تعمل مع منظّري الزمر على جمع التصويبات المنشورة في الأدبيات، وستنشرها على صفحة التصويبات الخاصة بالمشروع. واستُشير Lyons وSolomon، اللذان تستند إليهما أسس التصنيف، بشأن إصلاح مبرهنة UGT، وتقول الشركة إنها ستواصل تنظيم التصويبات ومعالجتها بالتعاون مع مجلس استشاري يضمّهما، إلى جانب المستشار الخارجي Dan Nakano. وتعرض Axiom إسهامها على أنه جعل البرهان قابلًا للتحقق آليًا، وتوثيق العوائق التي ظهرت، وتقديم حجج مصاغة شكليًا لمعالجتها، مع تأكيدها أن التصنيف يظل إنجازًا لعلماء الرياضيات الذين اكتشفوا الزمر وطوّروا الحجج.