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

برهان معروف في صيغة قابلة للفحص

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

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

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

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

أرقام تكشف حجم المهمة

تفيد أنثروبيك بأن الناتج بلغ 13 مليون سطر من شيفرة Lean، وأن الوكلاء ولّدوا نحو ستة مليارات وحدة نصية أثناء العمل. وتقول إن المشروع أثبت 30,300 نتيجة وسيطة، استُخدم نحو 29,500 منها في البرهان النهائي. أما جرد المستودع فيسجل 29,511 صفحة للمبرهنات، و1,450 وحدة للتعريفات، و60,475 وحدة مبنية. هذه الأرقام لا تصف الشيء نفسه، ولذلك ينبغي إبقاؤها منفصلة بدلاً من جمعها أو معاملتها كمقاييس مترادفة.

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

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

ما الذي فُحص فعلاً؟

يثبت المشروع الإصدار 4.33.1 من Lean والإصدار v4.33.0 من Mathlib. ويشترط الفحص الافتراضي أن تعتمد المبرهنة النهائية تحديداً على propext وClassical.choice وQuot.sound. كما يذكر ملف المستودع أن وحدات المشروع لا تستخدم أوامر axiom أو sorry أو native_decide أو unsafe أو extern أو implemented_by أو partial def أو #eval. ويوجد ملف تحدٍّ منفصل يستخدم sorry عن قصد، لكنه يقع خارج الحزمة التي يشملها البرهان النهائي.

وبحسب المستودع، أكد comparator v4.33.0 تطابق صيغة التحدي، والالتزام بقيد المسلمات، وإمكان إعادة فحص البرهان في نواة Lean، وانتهى إلى الرسالة «Your solution is okay!». وكتب عالم الرياضيات كيفن بازارد، في شهادة مستقلة عن إعلان الشركة، أنه بنى الشيفرة وشغّل أداة المقارنة وأن النتيجة اجتازت الفحص. وهذه قرينة مستقلة قوية على أن الشيفرة قابلة للبناء وأن الأداة قبلتها، لكنها لا تعني أن شخصاً راجع يدوياً كل سطر أو كل شرح رياضي في ملايين الأسطر.

ويورد المشروع اختباراً آخر باستخدام nanoda 0.4.13، وهو تنفيذ مستقل لنواة Lean مكتوب بلغة Rust. ووفق التقرير، قبل البرنامج ملفاً مصدّراً يضم 1,052,234 تصريحاً من دون أخطاء. وقد أدخلت أنثروبيك أربعة تعديلات على nanoda، وتقول إنها تخص عرض التقدم وسرعة البحث ولا تمس قواعد تحديد الأنواع. لذا يوفر الاختبار بنواة ثانية دعماً إضافياً، مع بقاء تلك التعديلات موضعاً مشروعاً للفحص المستقل.

حدود الثقة الحاسوبية

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

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

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

أثر بحثي لا مكتبة جاهزة

نُشر المستودع بوصفه أثراً بحثياً بترخيص Apache-2.0، مع تنبيه صريح إلى أنه غير خاضع للصيانة ولا يستقبل مساهمات. كما ينسب مواد مشتقة إلى مشروع مبرهنة فيرما الأخيرة في إمبريال كوليدج لندن، وإلى flt-regular وMathlib. وتؤكد هذه الإحالات أن النتيجة قامت على تراكم من الرياضيات البشرية والبنية البرمجية السابقة، حتى لو تولى الوكلاء قسماً كبيراً من عملية الصياغة الجديدة.

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

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

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

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

تمثيل بصري لمعادلة مبرهنة فيرما وبنية برهان صوري داخل نظام تحقق حاسوبي