تقرير: Claude صاغ برهان فيرما الأخير بلغة Lean في 11 يوماً

لا يعني الإعلان أن Claude اكتشف برهاناً جديداً لمبرهنة فيرما الأخيرة. فالمبرهنة حُسمت رياضياً منذ عقود؛ وما تقول Anthropic إن نظامها أنجزه هو تحويل مسار برهان حديث معروف إلى صياغة رسمية كاملة بلغة Lean، بحيث يستطيع مدقّق Lean التحقق آلياً من كل خطوة مرمّزة. وتفيد الشركة بأن العمل استغرق 11 يوماً من تشغيل الوكلاء بصورة مستقلة إلى حد كبير، وأنتج نحو 13 مليون سطر من شفرة Lean. 215

ما هي مبرهنة فيرما الأخيرة؟

تنص المبرهنة، بصيغتها المألوفة، على أنه لا توجد أعداد صحيحة موجبة غير صفرية (a,b,c) وأُس صحيح (n\geq3) تحقق المعادلة:

[
a^n+b^n=c^n
]

أما الصياغة الموجودة في مكتبة Lean الرياضية Mathlib فتقول إن أي حل في الأعداد الطبيعية، عندما يكون (n\geq3)، لا بد أن يحتوي على واحد على الأقل من (a) أو (b) أو (c) مساوياً للصفر. وهي صياغة مكافئة لغياب الحلول الموجبة غير البديهية. 31

أي برهان اتّبع النظام؟

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

وهنا تكمن الصعوبة: الورقة الرياضية التقليدية قد تقول «يتبع ذلك من الحجة القياسية» وتترك تفاصيل كثيرة ضمنية للخبير. أما المساعد البرهاني فلا يقبل هذه القفزات؛ إذ يجب ترميز التعريفات والافتراضات والنتائج المساندة وكل صلة استدلالية بصورة دقيقة قابلة لفحص الآلة.

لماذا بلغ الحجم 13 مليون سطر؟

وفقاً لـAnthropic، أنتج المشروع قرابة 30,300 مبرهنة تحقّق منها الحاسوب، منها نحو 29,500 مبرهنة تدخل في سلسلة الاعتمادات النهائية للبرهان. وتمتد هذه البنية عبر الجبر والهندسة والتحليل التوافقي ونظرية الأعداد. 215

لذلك لا ينبغي قراءة عبارة «11 يوماً» باعتبارها اختصاراً لتاريخ فكري طويل إلى أقل من أسبوعين. تقول الشركة أيضاً إن التشغيل ولّد نحو ستة مليارات رمز (tokens)، وشمل محاولات برهان كثيرة، وفحوص Lean، وإصلاحات استجابة للأخطاء، وهندسة لتنظيم مشروع رسمي ضخم طويل المدى. 5

التنسيق بين وكلاء متعددين: دور Prove2Me

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

تقوم الفكرة على رسم بياني موجّه للاعتمادات:

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

وتصف Prove2Me هذا النموذج بأنه «مهام» للصياغة الرسمية يساهم فيها الوكلاء ببراهين قابلة لإعادة الاستخدام. 29 وعملياً، يحوّل الرسم البياني مهمة هائلة وهشة إلى مسائل أصغر يمكن التحقق من كل منها، ويؤمن ذاكرة عمل دائمة للمشروع خارج نطاق تشغيل نموذج منفرد.

ماذا يعني «متحقَّق منه حاسوبياً»؟

تقول Anthropic إن المشروع النهائي لا يحتوي على عناصر sorry، وهي آلية في Lean تسمح بقبول عبارة من دون برهان مكتمل، وإنه يعتمد فقط على بديهيات Lean القياسية الثلاث. 5

هذا أقوى من نص رياضي يبدو مقنعاً كتبه نموذج لغوي. إذ يفحص نواة Lean ما إذا كانت كل خطوة رسمية تتبع من قواعد النظام المنطقي وبديهياته والاعتمادات المستوردة. وتقول Anthropic أيضاً إنها تحققت من أن الادعاء النهائي يطابق صياغة FermatLastTheorem المعتمدة في Mathlib. 531

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

لماذا وصف كيفن بازارد النتيجة بأنها استثنائية؟

نقلت Anthropic عن عالم الرياضيات كيفن بازارد وصفه النتيجة بأنها «إنجاز استثنائي في الصياغة الآلية». 21 والأهمية، في هذا الإطار، ليست حل تمارين منفصلة في Lean، بل الادعاء بأن وكلاء منسقين استطاعوا إنشاء تطوير رسمي متعدد الطبقات وقابل لإعادة الاستخدام على نطاق كان يُتوقع سابقاً أن يستلزم سنوات من العمل البشري المنسق.

وإذا أصبح هذا النهج قابلاً للتكرار وأقل كلفة، فقد يفيد البحث الرياضي في عدة جوانب:

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

الخلاصة: إنجاز مهم، لا «حل جديد» للمبرهنة

التفسير الدقيق للخبر هو أن Anthropic تقول إن منظومة وكلاء منسقة نقلت برهاناً معروفاً لمبرهنة فيرما الأخيرة إلى مشروع Lean هائل يمكن التحقق منه، عبر تفكيك العمل إلى شبكة اعتماد وتلقي تغذية راجعة مستمرة من المدقق الرسمي. 21529

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