كشفت شركة أنثروبيك عن أن برنامج الذكاء الاصطناعي «كلود» نجح في إعادة إثبات «نظرية فيرما الأخيرة» بصيغة رياضية رسمية قابلة للتحقق بواسطة الحاسوب، منتجاً ما وصفته الشركة بأنه أطول برهان رياضي رسمي على الإطلاق.
وأنجز «كلود» المهمة خلال 11 يوماً، وأنتج نحو 13 مليون سطر من التعليمات البرمجية التي يمكن للحاسوب فحصها خطوة بخطوة، بدلاً من الاعتماد على برهان مكتوب باللغة الرياضية التقليدية.
وتعود النظرية إلى عام 1637، قبل 389 عاماً عندما كتب عالم الرياضيات الفرنسي بيير دو فيرما على هامش كتاب أنه يمتلك «برهاناً رائعاً» للمسألة، لكنه لم يكن يتسع لهامش الكتاب. وظلت النظرية دون إثبات لأكثر من ثلاثة قرون، حتى قدم عالم الرياضيات البريطاني أندرو وايلز برهاناً عليها عام 1993. وبعد اكتشاف ثغرة فيها، أمضى وايلز قرابة عام في إصلاحها مع ريتشارد تايلور، قبل نشر النسخة النهائية عام 1995.
وتكمن أهمية إنجاز «كلود» في تحويل برهان وايلز إلى لغة «Lean»، التي تسمح للحاسوب بالتحقق من كل خطوة منطقية بصورة آلية.
وعمل عشرات من وكلاء «كلود» بالتوازي على تعريفات رياضية وبراهين فرعية، قبل تجميعها في البرهان النهائي. وبالبداية واجه النظام مشكلات في فقدان مسار ما أنجزه وتكرار العمل، لكن أداة «Prove2Me» ساعدت على تنظيم المهام وتنسيق جهود الوكلاء.
وبحسب أنثروبيك، أثبت «كلود» أكثر من 30 ألف نظرية داعمة، واستهلك مليارات الرموز، بينما بلغ حجم البرهان النهائي 13 مليون سطر، أي خمسة أضعاف حجم مكتبة «Mathlib» المستخدمة في الرياضيات الحاسوبية.
ورغم ضخامة الإنجاز، فإن «كلود» لم يكتشف برهاناً رياضياً جديداً فقد أثبت وايلز النظرية قبل ثلاثة عقود. الجديد هو إنتاج نسخة رسمية يمكن للحاسوب التحقق منها بالكامل.
وقال عالم الرياضيات كيفن بوزارد، الذي راجع البرهان، إنه يثبت النظرية من دون افتراضات إضافية تتجاوز بديهيات الرياضيات. وأصبح البرهان متاحاً مجاناً على GitHub لفحصه سطراً بسطر.
