شركة صينية تفتح شيفرة تحقق أطول برهان رياضي خلال 24 يومًا

بعد تسارع إنتاج الذكاء الاصطناعي للبراهين الرياضية، بما في ذلك دفعات نماذج أوبن إيه آي، أعلنت الشركة الصينية الناشئة أوكسيوم في 27 أكتوبر استكمال الصياغة الرسمية والتحقق الآلي من تصنيف الزمر البسيطة المنتهية، أطول برهان في تاريخ الرياضيات. وحول الفريق البرهان الأصلي، الذي يزيد على خمسة عشر ألف صفحة وموزع في مئات الأوراق بين نحو مئة من الرياضيين، إلى نحو 43.1 مليون سطر بلغة لين في 24 يوما، ثم أتاحه مفتوح المصدر على غيت هب. ويهدف هذا العمل إلى استبدال الاعتماد على الثقة بين الباحثين بتدقيق رياضي يمكن للآلة إعادة تشغيله من البديهيات إلى النتيجة النهائية. انطلق المشروع في 2 أكتوبر واكتمل في 26 منه، بإشراف مهندسين ورياضيين نسقوا عشرات الوكلاء الآلية. واعتمد الفريق على مكتبة لين الرياضية، وعلى نحو 1.2 مليون سطر سابق في مبادرة جامعة تسينغ هوا، وقسم البرهان إلى 108 أهداف رئيسية و380 مهمة فرعية. وشابت البداية صعوبات، منها كتابة أسطر مبنية على فرضيات غير مثبتة استلزمت حذف آلاف الأسطر، كما أبطأ حجم التدقيق المتقدم فاعاد توزيع الأهداف وبناء نظام تخزين مؤقت أعاد استخدام النتائج غير المتغيرة. ونجح الفريق في إثبات وجود الزمرة الوحشية وإثبات بساطتها، وهي خطوة مفصلية في التصنيف. ويحدد تصنيف الزمر البسيطة المنتهية جميع الزمر غير القابلة للتفكيك: زمر الدورات الأولية، والزمر المتناوبة، وستة عشر فصيلة من زمر لي المنتهية الحقل، و26 زمرة متفرقة، أوسعها الزمرة الوحشية الضخمة. وقد نشأ البرهان الأول عبر عقود، وسد فيه مايكل أسيباخر وستيفن سميت فجوة في أحد الفروع الحرجة في 2004 بمجلد من 1221 صفحة، ثم ظهرت تصحيحات لاحقة، ما جعل التحقق البشري الكامل شبه متعذر. وخلال التدقيق الرسمي رصد أوكسيوم عشرات المخالفات الطفيفة، وأكتشف خطأ في خطوة من برهان زمرة غير متوازنة، فاستخدم مسارا بديلا بمشورة خبراء من المشاركين الأصليين وأثبت نتيجة زمريّة جديدة. وتأسست أوكسيوم في مارس 2025 على يد هونغ ليتونغ، الصينية من قوانغتشو، الحاصلة على جائزة مورغان في البحث في معهد ماساتشوستس للتكنولوجيا، وانضم إليها عالم الأعداد كين أونو. وجمعت 64 مليون دولار ثم 200 مليون، وتجاوزت قيمتها مليار وستمئة مليون. وقبل هذا الإنجاز تحقق فريقها في أغسطس من التحقق الرسمي لنتيجة 246 في تباعد الأعداد الأولية. وتعني الصياغة الرسمية أن البراهين الآلية يمكن أن تصبح قابلة للمراجعة من الجميع، لكنها لن تحل محل الرياضيين في فهم السؤال، وتفسير الفجوات، وتوليد الفروض، أو مراجعة المصطلحات التي يختارها البرهان الرسمي. ومع انتشار البراهين المكتوبة بالآلة، قد يتحول أساس اليقين الرياضي من سيرة المؤلفين إلى شيفرة قابلة للتدقيق من أي مختص.