أول برهان لمبرهنة فيرما الأخيرة يتحقق منه الحاسوب أُنجز في 11 يوماً: 13 مليون سطر و30 ألف مبرهنة
أعلنت Anthropic أن Claude صاغ مبرهنة فيرما الأخيرة صياغة صورية كاملة بلغة Lean. وهو أكبر برهان بلغة Lean كُتب حتى اليوم، وأثبت في طريقه أكثر من 29 ألف مبرهنة أخرى في مجالات لم تُصَغ صورياً من قبل.
أعلنت شركة Anthropic أن نموذجها Claude أنتج أول برهان كامل يمكن للحاسوب التحقق منه لـمبرهنة فيرما الأخيرة بلغة Lean، وذلك في منشور بحثي مؤرخ في الرابع من أيلول. ويتبع البرهان نسخة مبسّطة من البرهان الذي نشره أندرو وايلز عام 1995.
طُرحت المبرهنة في القرن السابع عشر ولم تُبرهن إلا بعد أكثر من 350 عاماً، على يد وايلز عام 1995. أما الصياغة الصورية فعمل مستقل: تحويل الاستدلال الرياضي إلى صيغة تستطيع مساعدات البرهان الحاسوبية مثل Lean فحصها سطراً سطراً.
الأرقام
- 13 مليون سطر من Lean
- إثبات 30,300 مبرهنة، استُخدم منها 29,500 في البرهان النهائي
- استغرق 11 يوماً
- استهلك نحو ستة مليارات رمز مخرجات
وتصف Anthropic النموذج المستخدم بأنه "نموذج بحثي داخلي عام الغرض يقارَب تقريباً بـClaude Fable 5.1". والبرهان كامل متاح على GitHub.
نصيب البشر
بدأ المشروع تيانيي بينغ، الباحث في Anthropic الذي يقود في جامعة كولومبيا مجموعة تبني أدوات للصياغة الصورية بالذكاء الاصطناعي. وبحسب الشركة، فإن "المدخلات الرياضية من البشر اقتصرت على توجيهات عالية المستوى من تيانيي بين حين وآخر".
وراجع البرهان المكتمل كيفن بازارد من إمبريال كوليدج لندن، وكان مجتمعه يعمل على صياغة هذه المبرهنة منذ 2024. كما استند العمل إلى Prove2Me، وهي منصة تعاون مفتوحة لصياغة الرياضيات صمّمها بينغ وزملاؤه في كولومبيا.
وتشدد Anthropic على أن العمل مبني على "جهد ثلاثة قرون من الرياضيين وجهود مئات المساهمين في Lean وMathlib".
التحفّظ الذي تذكره الشركة نفسها
تكتب Anthropic حداً بوضوح: برهان Claude أكبر من Mathlib بأكثر من خمس مرات و"على الأرجح أطول بكثير مما يلزم". أي أن ما خرج ليس أنيق البراهين، بل برهان كامل وعامل يستطيع الحاسوب التحقق منه.
لماذا يهمّ
قد يستغرق التحقق من صحة برهان رياضي كبير سنوات. والصياغة الصورية تنقل هذا العبء إلى الحاسوب: فمتى تُرجم البرهان إلى Lean أمكن للآلة التحقق من صحته. وتقدّم Anthropic هذا بوصفه خطوة نحو تخفيف "عبء التحكيم الرياضي في عصر يُنتَج فيه من البراهين أكثر من أي وقت مضى".
وتمثّل المبرهنات التي أُثبتت في الطريق، وعددها يتجاوز 29 ألفاً، مكسباً مستقلاً، إذ تقع في مجالات رياضية لم تُصَغ صورياً من قبل وصارت الآن أرضية لأعمال الصياغة اللاحقة.
