أنثروبيك: كلود صاغ برهان مبرهنة فيرما الأخيرة صياغة شكلية في أحد عشر يوماً

برهان يستطيع الحاسوب التحقق منه

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

تنصّ مبرهنة فيرما الأخيرة على أنه لا توجد ثلاثة أعداد صحيحة موجبة تحقق a^n + b^n = c^n لأي عدد صحيح n أكبر من اثنين. برهنها أندرو وايلز عام 1995 في بحث يقع في نحو 129 صفحة، مستنداً إلى أدوات بُنيت على امتداد القرن العشرين. مراجعة برهان كهذا يدوياً تستغرق المتخصصين سنوات، وكان متوقعاً أن تستغرق صياغته الشكلية مدة مماثلة.

ما فعله النموذج فعلياً

بحسب أنثروبيك، كان النظام نموذجاً بحثياً داخلياً عام الأغراض، يقارب كلود فيبل 5.1، لا محركاً رياضياً مخصصاً. وتقول الشركة إن عشرات الوكلاء عملوا بالتوازي، وأنتجوا نحو ستة مليارات رمز، وبرهنوا 30300 مبرهنة، منها 29500 وردت في النتيجة النهائية. أما التدخل البشري فاقتصر على توجيه عام.

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

الأساس البشري تحت النتيجة

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

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

لماذا الصياغة الشكلية هي الجزء المهم

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

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

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