Axiom Math تُحوّل «النظرية الضخمة» إلى 43.1 مليون سطر بلغة Lean خلال 24 يومًا

أعلنت Axiom Math اكتمال التحقق الحاسوبي من نظرية تصنيف الزمر البسيطة المنتهية (CFSG)، التي يسميها علماء الرياضيات «النظرية الضخمة». فقد كتب عشرات وكلاء الذكاء الاصطناعي خلال 24 يومًا نحو 43.1 مليون سطر من الشيفرة بلغة Lean، وصاغوا بها برهانًا يمتد على 15 000 صفحة في أكثر من 500 ورقة علمية. وقد عمل على هذا البرهان نحو 100 عالم على مدى عقود. وتصف Axiom النتيجة بأنها أول برهان كامل لـ CFSG يمكن التحقق منه بالحاسوب. وقد نُشرت الشيفرة والمواد للاطلاع عليها والتحقق منها بصورة مستقلة.

جدول دوري للتماثلات

أبسط طريقة لفهم ما تصنّفه النظرية هي المكعب. يمكن تدويره بـ 24 طريقة بحيث يبدو مطابقًا تمامًا لوضعه الأول. وتشكّل هذه التدويرات زمرة رياضية. وتصف CFSG «اللبنات الأساسية» التي تتكوّن منها جميع زمر التماثل المنتهية. والنتيجة أشبه بجدول دوري للتماثلات، يُستخدم في الجبر ونظرية الأعداد والفيزياء الرياضية.

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

حسابات المشروع: 43 مليون سطر في 24 يومًا

تعطي الأرقام فكرة عن حجم المشروع. فإنتاج 43.1 مليون سطر في 24 يومًا يعني نحو 1.8 مليون سطر يوميًا، أو قرابة 75 ألف سطر في الساعة إذا حُسب العمل على مدار الساعة. ويقابل الصفحة الواحدة من البرهان الورقي نحو 2 900 سطر من الشيفرة الشكلية. والصياغة الشكلية أكثر تفصيلًا من النص الأصلي بعدة رتب من الحجم، لأن علماء الرياضيات يحذفون في أوراقهم الخطوات «البديهية»، بينما لا تسمح Lean بذلك.

وهذا عمل قائم على الوكلاء، لا توليد واحد طويل. فقد أدار عشرات الوكلاء فروعًا متوازية من الصياغة الشكلية، وكان على الشيفرة النهائية أن تلتقي في برهان واحد تقبله نواة التحقق. وهذا التحقق بالنواة هو ما يميّز هذه النتيجة عن المخرجات المعتادة للنماذج اللغوية: فالخطوة الخاطئة لن تمرّ ببساطة.

ماذا وجد الوكلاء أثناء العمل

لم تقتصر الصياغة الشكلية على التأكيد، بل أسفرت أيضًا عن اكتشافات جديدة. وتورد Axiom النتائج التالية:

• نحو 43.1 مليون سطر من شيفرة Lean أنتجها عشرات وكلاء الذكاء الاصطناعي خلال 24 يومًا؛
• 34 تباينًا جوهريًا مع الأعمال الرياضية المنشورة؛
• أمثلة مضادة لبعض الادعاءات الواردة في الأدبيات، مع براهين بديلة لها؛
• نتيجة جديدة في نظرية الزمر، لازمة للمسار المختار للبرهان؛
• في بعض الحالات، أخطاء عُثر عليها في الاستدلالات الأصلية، وحجج رياضية جديدة تصححها؛
• عمل مشترك مع علماء رياضيات، بينهم متخصصون شاركوا في التصنيف الأصلي.

والمشاركة البشرية هنا جوهرية. فحين تصطدم الصياغة الشكلية بتباين مع المنشور، يلزم خبير يميّز الخطأ المطبعي من الثغرة الحقيقية. وقد ساعدت خبرة مؤلفي التصنيف الأصلي على تحديد المواضع التي ينبغي للنسخة الشكلية أن تتبع فيها الأصل، والمواضع التي يلزم فيها مسار مختلف.

ما الذي يمكن الاستفادة منه عمليًا

الاستنتاج الرئيسي للقطاع أن وكلاء يكتبون الشيفرة ويتحققون منها ذاتيًا في بيئة ذات مدقّق صارم قادرون على إنجاز مهام تعجز عنها الجهود اليدوية. فـ Lean هنا بمثابة حَكَم لا يصدّق البشر ولا النموذج بلا دليل. ويمكن تطبيق المخطط نفسه في أي مجال يمكن فيه التحقق من النتيجة آليًا: التحقق من البرمجيات الحرجة، والبروتوكولات، والبنى التشفيرية.

وثمة تنبيه حذر أيضًا. فالتحقق الحاسوبي يضمن صحة البرهان بالنسبة إلى التعريفات والصياغات المكتوبة فقط. لذلك لا تقل أهمية الشيفرة المفتوحة عن النتيجة نفسها: إذ يستطيع علماء الرياضيات قراءة التعريفات والتأكد من أن ما جرت صياغته شكليًا هو المطلوب فعلًا. أما كلفة هذا التشغيل (نفقات الحوسبة والرموز) فلم تذكرها Axiom في إعلانها. وهذا الرقم تحديدًا هو ما سيبيّن هل ستصبح إعادة التحقق الشكلي من النتائج الأساسية أمرًا روتينيًا، أم ستبقى مشروعًا لمرة واحدة.

أما بالنسبة إلى علماء الرياضيات، فالرسالة واضحة. فالأدبيات التي كان لا بد من قبولها ثقةً بسلطة أصحابها صارت تحتمل إعادة تحقق آلية كاملة، وقد ظهر على هذا الطريق بالفعل 34 تباينًا جوهريًا.