Claude يحوّل برهان فيرما إلى 13 مليون سطر يمكن للحاسوب تدقيقها
نشرت Anthropic في 4 سبتمبر 2026 صياغة حاسوبية كاملة لنظرية فيرما الأخيرة، أنتجها Claude خلال 11 يومًا من العمل شبه المستقل. وتقول ورقة Anthropic البحثية إن العملية ولّدت نحو 13 مليون سطر بلغة Lean، وأثبتت 30,300 نظرية وسيطة، استُخدم نحو 29,500 منها في المسار النهائي.
لا يعني الإصدار المنشور في ذلك التاريخ أن Claude اكتشف برهانًا جديدًا لمسألة مفتوحة؛ فالعمل يحوّل حجة رياضية معروفة إلى تعريفات واستنتاجات يستطيع مساعد البرهان Lean فحصها خطوة بخطوة. الجديد هنا هو اكتمال الصياغة الآلية بهذا الحجم والسرعة، لا النتيجة الرياضية نفسها.
ما الذي حوّله Claude إلى كود؟
البرهان الموجّه إلى الرياضيين لا يذكر بالضرورة كل تفصيل منطقي. يمكنه الإحالة إلى نتيجة معروفة، أو تجاوز حساب روتيني، أو استخدام مفهوم يتشارك المتخصصون فهمه من دون إعادة بنائه. أما Lean فيحتاج إلى تعريف الكائنات والفرضيات والعمليات بدقة، ثم إلى دليل صريح يربط كل نتيجة بما سبقها.
لهذا لا تمثل ملايين الأسطر ترجمة لفظية مطوّلة لبحث واحد. إنها قاعدة برمجية تضم تعريفات ووحدات ونظريات مساعدة واعتماديات كثيرة، بحيث يصبح الانتقال من مقدمات الحجة إلى عبارتها النهائية مسارًا يمكن للنواة المنطقية تتبعه.
استخدم المشروع عشرات من وكلاء Claude ضمن بنية متعددة الوكلاء قائمة على منصة Prove2Me. حفظت المنصة رسمًا بيانيًا موجّهًا للنظريات، وساعدت الوكلاء على اختيار المسائل التالية والعثور على النتائج السابقة وإعادة استخدامها. وقد اتبعت الصياغة عرض دارمون ودايموند وتايلور لحجة وايلز وتايلور–وايلز، مع الاستفادة من Mathlib وأجزاء من مشروعات Lean بشرية سابقة.
كيف جرى فحص 13 مليون سطر؟
الدليل العملي على الإنجاز هو مستودع قابل للبناء، لا وصف صحفي وحده. يعرّف مستودع الصياغة المنشور العبارة النهائية للأعداد الطبيعية الموجبة، ويثبت بيئته على Lean 4.33.1 وMathlib 4.33.0، ويضم مسارًا يربط مراحل الحجة بالنظريات التي تنفذها.
يفيد توثيق المستودع بأن البناء من المصدر شمل 60,475 وحدة، وفحصت نواة Lean كل تصريح. كما يفرض الهدف النهائي أن يعتمد البرهان على مسلمات Lean القياسية الثلاث فقط، ويمنع تمرير فجوة من نوع sorry أو إضافة مسلمة خاصة تمنح النتيجة من دون برهان.
لم يقتصر الاختبار على نجاح البناء. قارن برنامج منفصل العبارة المثبتة بصيغة نظرية فيرما الموجودة في Mathlib، بما في ذلك الثوابت التي تذكرها، ثم قبلت nanoda، وهي نواة مستقلة مكتوبة بلغة Rust، عدد 1,052,234 تصريحًا من البيئة المصدّرة من دون أخطاء. لا تجعل هذه الطبقات أي نظام برمجي معصومًا نظريًا، لكنها تقلل احتمال أن يكون النجاح نتيجة اختلاف خفي في العبارة أو اعتماد غير معلن.
يتضمن المستودع أيضًا صفحات ثابتة لنحو 29,511 نظرية و1,450 وحدة تعريف، مع بيان ما تستدعيه كل نظرية وما يعتمد عليها. ويجب التمييز بين هذه الأعداد: 30,300 هو إجمالي النظريات التي تقول Anthropic إن العملية أثبتتها، ونحو 29,500 استُخدمت في البرهان النهائي، بينما 29,511 هو عدد صفحات النظريات التي يوثقها المستودع.
لماذا لا يعد ذلك اكتشافًا لبرهان جديد؟
اكتشاف البرهان يضيف حجة أو فكرة رياضية لم تكن معروفة، أما إضفاء الطابع الرسمي فيحوّل حجة قائمة إلى لغة دقيقة يستطيع الحاسوب التحقق من استنتاجاتها. مشروع Claude يقع في الفئة الثانية: بنى تمثيلًا رسميًا متصلًا لحجة من الأدبيات المعروفة، ولم يقدم طريقًا رياضيًا جديدًا إلى النظرية.
عالم الرياضيات كيفن بازارد، الذي يقود مشروعًا بشريًا لصياغة نظرية فيرما في Lean، قال في مراجعته المستقلة للعمل إنه بنى قاعدة الكود وشغّل أداة المقارنة بنجاح، وإن الصياغة تتبع الأدبيات المبكرة للبرهان ولا تضيف رياضيات جديدة. وقدّر القاعدة بأكثر من 13.4 مليون سطر؛ لذلك يمثل رقم 13 مليونًا في العنوان تقريب Anthropic للحجم، لا قياسًا مخالفًا لنتيجة المراجعة.
لا يقلل هذا الفصل من قيمة الإنجاز، لكنه يحددها. الأثر المنشور يبين أن نظامًا متعدد الوكلاء استطاع ملء عدد هائل من التفاصيل التي تتركها الكتابة البشرية ضمنية، وربطها حتى عبارة نهائية تقبلها نواة التحقق. طول الكود يقيس حجم الأثر الرسمي الناتج، ولا يقيس عمق فكرة رياضية جديدة أو جودة تنظيمها.
ما الذي يضمنه Lean وما الذي يبقى للبشر؟
قبول النواة للكود يعني أن العبارة النهائية تتبع منطقيًا من التعريفات والمسلمات المحددة داخل البيئة المفحوصة. لكنه لا يعني تلقائيًا أن اسم كل تعريف يطابق المفهوم الذي يوحي به، أو أن وصف كل نظرية وسيطة باللغة الطبيعية يفسر محتواها الرسمي بدقة. في هذا المستودع، التصريح المكتوب بلغة Lean هو المرجع عند اختلافه مع الاسم أو الملخص المولد.
تكتسب العبارة النهائية درجة إضافية من الثقة لأنها تستخدم الأعداد الطبيعية والعمليات الأساسية في Lean، ولأن المقارن طابقها مع صيغة Mathlib. مع ذلك، تبقى مراجعة بنية الصياغة ضرورية لفهم كيف تمثل مراحل الحجة الكلاسيكية، وما إذا كانت التعريفات عامة ومنظمة وقابلة لإعادة الاستخدام، وكيف ينبغي نسب الأجزاء المقتبسة أو المعدلة إلى المشروعات السابقة.
الصحة المنطقية لا تكفي أيضًا لإدماج 13 مليون سطر في Mathlib. المكتبة المجتمعية تهتم بإيجاز البراهين وعمومية التعريفات وقابلية الصيانة وإعادة الاستخدام، بينما يصف المستودع نفسه بأنه أثر بحثي غير خاضع للصيانة ولا يقبل مساهمات. لذلك لا يحل الإصدار محل المشروع البشري الرامي إلى بناء عرض حديث ومقروء ومندمج تدريجيًا في المكتبة.
الحالة المؤكدة الآن هي وجود صياغة علنية قابلة لإعادة البناء، اجتازت نواة Lean والمقارن ونواة مستقلة، وخضعت لفحص خارجي من بازارد. أما المرحلة المفتوحة فهي تنقيح هذا الأثر الضخم، ومراجعة تمثيله للمفاهيم الوسيطة، وتحديد الأجزاء التي يمكن تحويلها إلى مكونات أوضح وأقصر وأكثر نفعًا للرياضيات الرسمية.
اقرأ أيضًا:
اشترك في نشرتنا الإخبارية
احصل على أحدث أخبار الويب 3 والذكاء الاصطناعي والعملات المشفرة مباشرة في بريدك.