نشرت Anthropic في 4 سبتمبر صياغةً رسميةً مُتحققاً منها آلياً لـ مبرهنة فيرما الأخيرة في Lean 4؛ وتضع واجهة GitHub API إنشاء المستودع عند 14:21:04 UTC. وكان الادعاء المتداول أن Claude أثبت مبرهنة فيرما الأخيرة في 11 يوماً. لكن ملفات المستودع نفسها تصف أمراً أضيق، وأكثر إثارة للاهتمام من وجهٍ واحد.

ما الذي يقوله ملف الإسناد

يتضمن المستودع ملف ATTRIBUTION.md يسجل 106 ملفات تحتوي مواد من مشروع FLT في Imperial College London بقيادة Kevin Buzzard، ومن مشروع flt-regular — "54 تحت Definitions/، و52 تحت P2M/Sol/؛ و23 ملفاً تعيد إنتاج نص Mathlib". وترد في عشرات الصفوف عبارة "whole file (100%)". أما ملف NOTICE فيؤرخ الاقتباس: "Material was taken from the project's main branch as of 2026-05-21". ومع الانتقال إلى سلسلة الأدوات Lean 4.33، يسجل ملف الإسناد أنه "left the other 41 byte-identical".

التحقق حقيقي

ولا ينقض ذلك التحقق. فـ README يذكر أن جميع 60,475 modules بُنيت، وأن #print axioms fermat_last_theorem محصورة في البديهيات القياسية الثلاثة، وأنه لا توجد في أي وحدة axiom أو sorry أو native_decide أو unsafe أو partial def. واستغرق التجميع 5 hours 32 minutes at 96 jobs مع ذروة ذاكرة بلغت 153 GB. ووفق أرقام Anthropic نفسها: 13 million lines من Lean، و29,500 نظرية وسيطة استُخدمت في البرهان النهائي، ونحو six billion output tokens.

ما الذي يخطئ فيه التأطير المتداول

ثلاثة أمور. Claude لم يثبت شيئاً جديداً — فهذا عمل autoformalisation لعرض Darmon–Diamond–Taylor لعام 1995 لحجة Wiles–Taylor–Wiles، أي برهان أكمله البشر قبل واحد وثلاثين عاماً. وهو ليس من دون مساعدة: فبحسب حساب Anthropic نفسه، يحتوي عُشر المستودع على نص Lean بشري، بعضه حرفياً. كما كتب Buzzard، عالم الرياضيات الذي يستشهد Anthropic بمراجعته، على مدونته في اليوم نفسه أن "mathematically this work of anthropic tells us essentially nothing" وأن الصياغة الرسمية "just faithfully follows the early literature on the proof and adds nothing." كما وصفت عدة وسائل إعلام المشروع بأنه أكبر ملف من نوعه؛ لكنه في الواقع 60,475 module، لا ملفاً واحداً.

الادعاء الصادق لا يزال كبيراً

يمكن للآلات الآن ترجمة آلاف الصفحات من الأدبيات الرياضية القائمة إلى صيغة قابلة للتحقق على مستوى kernel في أقل من أسبوعين، بعد أن استندت إلى عدة سنوات من عمل Lean التطوعي. وهذه نتيجة حقيقية تتعلق بسرعة الترجمة. لكنها ليست نتيجة عن الاكتشاف الرياضي، ويقرّ README نفسه بالفجوة المتبقية: "What no tool can check is that each intermediate theorem means what its name suggests."