Claude يصوغ برهان فيرما في Lean خلال 11 يومًا، لكنه لا يقدّم برهانًا جديدًا
نشرت Anthropic في 4 سبتمبر 2026 صياغة كاملة لمبرهنة فيرما الأخيرة أنشأها Claude، إلى حد كبير بصورة مستقلة، خلال 11 يومًا بلغة Lean. ويذكر إعلان Anthropic عن المشروع أن الناتج هو أول برهان كامل للمبرهنة قابل للفحص الحاسوبي من البداية إلى النهاية، وأن العمل ولّد نحو 13 مليون سطر من شيفرة Lean و29,500 مبرهنة وسيطة مستخدمة في المسار النهائي.
لكن الإصدار المنشور في 4 سبتمبر لا يتضمن حجة رياضية جديدة لمبرهنة فيرما الأخيرة. ما أنجزه Claude هو تحويل المسار المعروف، المبني على أعمال غيرهارد فراي وجان بيير سير وكين ريبيه وأندرو وايلز وريتشارد تايلور، إلى كائن برهاني رسمي يستطيع Lean فحص اعتمادياته وخطواته وفق قواعد محددة.
ما الذي اكتمل خلال 11 يومًا؟
تقول مبرهنة فيرما الأخيرة إنه لا توجد أعداد صحيحة موجبة تحقق aⁿ + bⁿ = cⁿ عندما يكون الأس n أكبر من 2. حُسمت النتيجة رياضيًا في تسعينيات القرن الماضي؛ أما الجديد في هذا المشروع فهو بناء سلسلة رسمية متصلة تبدأ من التعريفات والنتائج المساعدة وتنتهي بعبارة المبرهنة داخل Lean 4.
يتبع المسار عرض هنري دارمون وفريد دايموند وريتشارد تايلور لحجة وايلز–تايلور–وايلز، ويعتمد على نتائج كلاسيكية منها مبرهنة لانغلاندز–تونيل وخفض المستوى لريبيه. كما يستفيد من أجزاء سابقة كتبها البشر في Mathlib ومشروعات رسمية مفتوحة، ولذلك لا يصح وصف الناتج بأنه عمل بدأ من الصفر أو برهان ابتكره النموذج وحده.
شارك عشرات الوكلاء القائمين على Claude في تعريف المفاهيم وإثبات النتائج الوسيطة وربطها. ونظمت منصة Prove2Me العمل في رسم اعتماد موجّه للمبرهنات، مع فصل ملفات العبارات عن ملفات البراهين لتوزيع المهام وتقليل كلفة إعادة الترجمة.
كيف تحوّل البرهان البشري إلى ملفات Lean؟
يمكن للبرهان الموجّه إلى المختصين أن يتجاوز خطوات مألوفة، أو يستدعي نتيجة منشورة من دون إعادة تفصيل مقدماتها، أو يستخدم مفهومًا يفهم القارئ خصائصه من السياق. Lean لا يعتمد على هذا النوع من المعرفة الضمنية؛ بل يحتاج إلى تعريف كل كائن وتحديد نوعه وافتراضاته وربط كل نتيجة بالتصريحات التي تسبقها.
لهذا لم تكن المهمة ترجمة نص وايلز سطرًا بسطر. كان على المشروع بناء طبقات واسعة من الجبر والهندسة ونظرية الأعداد والتحليل، ثم سد المسافات المنطقية بينها بمبرهنات أصغر. وتتوزع المادة على مجلدات للتعريفات وعبارات المبرهنات والبراهين، مع مسار موثق يبين أي تصريح في Lean يحمل كل خطوة من الحجة الرياضية.
يفسر ذلك الحجم الضخم للمشروع، لكنه لا يجعل البرهان الرياضي الأصلي أطول أو أعمق. فالـ13 مليون سطر تقيس مقدار التفصيل البرمجي وما احتاجت إليه الصياغة خارج المكتبة المتاحة، كما تقر Anthropic بأن الشيفرة المولدة آليًا أطول على الأرجح مما يلزم.
ماذا فحص Lean بالضبط؟
يعرّف المشروع العبارة النهائية على الأعداد الطبيعية الموجبة وللأسس التي تبدأ من 3. بعد ذلك يفحص Lean أن الكائن البرهاني الذي بناه المشروع يملك النوع المنطقي المطابق لهذه العبارة؛ أي إن النواة تعيد التحقق من صحة تطبيق قواعد الاستدلال، ولا تكتفي بثقة مسبقة في مخرجات Claude.
يوضح مستودع البرهان في Lean 4 أن هدف البناء الافتراضي FinalCheck.lean يفشل عند وجود فجوات من نوع sorry أو بديهيات مضافة أو وسائل محظورة مثل native_decide، ويحصر الاعتماد في بديهيات Lean القياسية الثلاث: propext وClassical.choice وQuot.sound. كما نجح بناء 60,475 وحدة، وقارن مدقق منفصل العبارة النهائية بصيغة Mathlib، ثم قبلت نواة مستقلة مكتوبة بلغة Rust أكثر من مليون تصريح من البيئة المصدرة من دون أخطاء.
هذه الفحوص تثبت، ضمن الثقة في قواعد النواة وأدوات التحقق، أن العبارة الرسمية تتبع من اعتمادياتها المعلنة. لكنها لا تثبت أن الاسم الإنجليزي لكل مبرهنة وسيطة يصف معناها بدقة؛ فالعبارة المكتوبة بلغة Lean هي المرجع الحاكم، بينما الأسماء والملخصات المصاحبة تساعد البشر على التصفح فقط.
إعادة الاختبار ممكنة لأن الشيفرة متاحة، لكنها ليست خفيفة. تسجل تعليمات المستودع أن البناء الكامل لدى الفريق استغرق 5 ساعات و32 دقيقة باستخدام 96 مهمة متوازية وبلغت ذروة الذاكرة 153 غيغابايت، فيما احتاج تشغيل أداة المقارنة قرابة 14 ساعة و46 دقيقة وذاكرة أعلى. لذا فالقابلية للفحص لا تعني أن أي قارئ يستطيع إعادة البناء بسهولة على حاسوب شخصي.
لماذا لا يُعد ذلك برهانًا رياضيًا جديدًا؟
التمييز يتعلق بمصدر الجدة. البرهان الرياضي الجديد يقدم فكرة أو مسارًا استدلاليًا لم يكن معروفًا، بينما الصياغة الرسمية تجعل حجة موجودة مسبقًا صريحة بالقدر الذي يسمح لنواة برمجية بفحصها. إنجاز Claude يقع في الفئة الثانية: جديد في سرعة الأتمتة واتساعها، لا في النتيجة أو الطريق الرياضي الأساسي.
قدّم عالم الرياضيات وخبير Lean كيفن بازارد مراجعة مستقلة؛ إذ قال في تقييمه المنشور يوم الإعلان إنه جمع قاعدة الشيفرة وشغّل أداة comparator وإن الفحص نجح، كما أوضح أن الصياغة تتبع أدبيات البرهان المبكرة ولا تضيف، بحسب فهمه، رياضيات جديدة. وذكر أيضًا أنه فحص يدويًا الشيفرة التي لا تبدو تعريفات أو براهين رياضية، مع إقراره بأن هذا الفحص اليدوي ليس ضمانًا كاملًا بمفرده.
مع ذلك، لا يقلل غياب الجدة الرياضية من صعوبة الإنجاز الهندسي. تحويل آلاف الصفحات من الاعتماديات المنشورة إلى سلسلة قابلة للفحص في أقل من أسبوعين يشير إلى تقدم كبير في الصياغة الآلية للبراهين، وقد يساعد مستقبلًا على كشف افتراضات مخفية أو فجوات في أعمال لم تُفحص رسميًا.
ما الذي لم يحسمه الإصدار؟
الحالة المؤكدة بعد النشر هي وجود مستودع مفتوح يحتوي على صياغة كاملة، ونجاح فحصها بنواة Lean وأدوات إضافية، ونجاح مراجعة تقنية مستقلة في تجميعها وتشغيل المقارنة عليها. أما سهولة قراءة 13 مليون سطر وصيانتها أو إدماج نتائجها العامة في Mathlib فمسائل مختلفة لم يحسمها نجاح البناء.
المستودع نفسه يصف المشروع بأنه أثر بحثي غير خاضع للصيانة ولا يقبل مساهمات. وستتوقف قيمته طويلة الأجل على قدرة الباحثين على فهم بنيته وتقليص أجزائه وإعادة استخدام التعريفات والبراهين المفيدة منه. كما يبقى اختبار الأتمتة على نتائج حديثة غير محسومة تحديًا آخر؛ فإعادة بناء حجة صحيحة ومعروفة تثبت قدرة كبيرة على الصياغة والتحقق، لكنها لا تثبت وحدها قدرة Claude على ابتكار رياضيات جديدة.
اقرأ أيضًا:
اشترك في نشرتنا الإخبارية
احصل على أحدث أخبار الويب 3 والذكاء الاصطناعي والعملات المشفرة مباشرة في بريدك.