Anthropic تنجح بتوثيق نظرية فيرما الأخيرة بالذكاء الاصطناعي
حققت Anthropic إنجازًا بارزًا في مجال الرياضيات الحاسوبية، بعدما تمكن وكلاء Claude من إنتاج أول برهان كامل لنظرية فيرما الأخيرة يمكن التحقق منه حاسوبيًا، وذلك خلال 11 يومًا من العمل شبه المستقل باستخدام لغة البرمجة Lean. وكتب الوكلاء نحو 13 مليون سطر من التعليمات البرمجية وأثبتوا عشرات الآلاف من النظريات الوسيطة خلال العملية.
تفاصيل الخبر
تُعد نظرية فيرما الأخيرة واحدة من أشهر المسائل في تاريخ الرياضيات، وقد أثبتها عالم الرياضيات البريطاني Andrew Wiles عام 1995 بعد قرون من المحاولات. لكن تحويل هذا البرهان إلى صيغة يستطيع الكمبيوتر التحقق من جميع خطواتها كان مشروعًا أكثر تعقيدًا.
- عمل وكلاء Claude على المشروع لمدة 11 يومًا بصورة شبه مستقلة.
- أنتجوا نحو 13 مليون سطر من كود Lean خلال عملية التوثيق الرياضي.
- أثبت النظام نحو 30,300 نظرية أثناء العمل، مع استخدام نحو 29,500 منها في البرهان النهائي.
- اعتمد المشروع على Lean، وهو نظام يساعد أجهزة الكمبيوتر على التحقق آليًا من صحة البراهين الرياضية.
- تعاون عشرات وكلاء Claude في تحديد المفاهيم وإثبات النظريات الوسيطة وربطها للوصول إلى النتيجة النهائية.
- اعتمد البرهان على نسخة مبسطة من المسار الرياضي الذي استخدمه Andrew Wiles لإثبات نظرية فيرما الأخيرة.
- استخدم الفريق منصة Prove2Me لتنظيم العمل بين الوكلاء عبر رسم بياني يوضح العلاقات بين النظريات التي يجب إثباتها.
- استفاد المشروع من أعمال رياضية سابقة ومكتبات مثل Mathlib ومشروع نظرية فيرما في Imperial College London.
- تم التحقق من البرهان النهائي بواسطة Lean، مع الاعتماد على بديهياته القياسية الثلاث دون استخدام نتائج غير مثبتة كبدائل مؤقتة.
وتكمن أهمية الإنجاز في أن Claude لم يكتشف برهانًا رياضيًا جديدًا لنظرية فيرما الأخيرة، بل نجح في تحويل المعرفة الرياضية الموجودة إلى صيغة رسمية يمكن للكمبيوتر فحصها بالكامل. وترى Anthropic أن هذه القدرة قد تساعد مستقبلًا في تقليل الوقت الذي يحتاجه علماء الرياضيات لمراجعة البراهين الجديدة.
كيف ساعد الذكاء الاصطناعي في المهمة؟
واجهت المحاولات الأولى صعوبات في الحفاظ على حالة المشروع والتنسيق بين الوكلاء. لكن استخدام Prove2Me ساعد على تقسيم البرهان إلى مجموعة من المهام المترابطة، بحيث يستطيع كل وكيل العمل على جزء محدد ثم استخدام النتائج التي توصل إليها وكلاء آخرون.
كما ساعد النظام في تسريع عملية تجميع أكواد Lean وإعادة استخدام النظريات التي تم إثباتها، ما جعل من الممكن إدارة مشروع رياضي ضخم كان من المتوقع أن يستغرق سنوات من العمل البشري.
الأهداف المستقبلية
وتركز Anthropic على استخدام قدرات التوثيق الرياضي لتسهيل التحقق من الأبحاث الرياضية التي ينتجها البشر والذكاء الاصطناعي، وتشمل أبرز الأهداف المستقبلية ما يلي:
- تسريع عملية التحقق من البراهين الرياضية المعقدة.
- تقليل العبء الواقع على علماء الرياضيات والمراجعين.
- تطوير أدوات قادرة على تحويل الأبحاث الرياضية إلى براهين رسمية.
- تعزيز الثقة في النتائج الرياضية التي ينتجها الذكاء الاصطناعي.
- استخدام الذكاء الاصطناعي لاكتشاف الأخطاء المحتملة في المعرفة الرياضية الحالية.
- توسيع استخدام Lean ومكتبات الرياضيات الرسمية.
- مساعدة الباحثين على توثيق نتائجهم الرياضية بالتزامن مع كتابة الأبحاث.
- تطبيق الأسلوب نفسه على نظريات ومسائل رياضية كبيرة أخرى.
يمثل إنجاز Anthropic خطوة مهمة في تطور استخدام الذكاء الاصطناعي في الرياضيات، إذ أظهر وكلاء Claude قدرتهم على التعامل مع مشروع توثيق رياضي ضخم والتعاون في إثبات آلاف النظريات الوسيطة. ورغم أن الذكاء الاصطناعي لم يكتشف البرهان الأصلي لنظرية فيرما الأخيرة، فإن قدرته على تحويله إلى صيغة قابلة للتحقق آليًا قد تغير مستقبل مراجعة الأبحاث الرياضية والتحقق من صحتها.
