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

وقد لفت هذا الإنجاز اهتمامًا فوريًا عبر مجتمع البحث، حيث تصدر موقع Hacker News في غضون ساعات من نشره. كان من المتوقع أن يستغرق إثبات النظرية رسميًا جهدًا مجتمعيًا لعدة سنوات؛ بدلاً من ذلك، أكمل فريق من العشرات من عملاء كلود المتعاونين المهمة في أقل من أسبوعين. لمزيد من السياق حول وضع قدرات الذكاء الاصطناعي اليوم، راجع [أحدث تطورات الذكاء الاصطناعي] (https://aibuzzwire.news).

ما هي نظرية فيرما الأخيرة؟ ولماذا قاومت البرهان لمدة 350 عامًا

تنص نظرية فيرما الأخيرة على أنه لا يمكن لأي أعداد صحيحة موجبة أ، ب، ج أن تحقق المعادلة أⁿ + بⁿ = جⁿ لأي قيمة ن أكبر من 2. دوّن بيير دي فيرما هذا الادعاء حوالي عام 1637 في هامش نسخته من كتاب ديوفانتوس الحساب، مضيفًا ملاحظته التي أصبحت الآن أسطورية بأنه اكتشف دليلًا رائعًا حقًا كان الهامش ضيقًا جدًا بحيث لا يمكن احتواؤه.

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

كيف بنى كلود دليلاً مكونًا من 13 مليون سطر

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

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

من خلال استخدام أداة متعددة الوكلاء قائمة على Claude Code، استهلك فريق الوكلاء ما يقرب من ستة مليارات رمز إخراج من نموذج بحث داخلي تصفه Anthropic بأنه مشابه تقريبًا لـ Claude Fable 5.1. اقتصرت المدخلات البشرية على تعليمات عرضية عالية المستوى - تستشهد الأنثروبيك برسائل مثل "يبدو أن جاكوبيان كمخطط له أولوية عالية" وطلب دفع نظرية مازور ليتم تنفيذها قريبًا. اكتمل الإثبات في تمام الساعة 02:00 بالتوقيت العالمي المنسق في 18 أغسطس، عندما انقلبت نظرية الجذر الخاصة بالمنصة إلى Proved.

وعلى طول الطريق، أثبت كلود 30300 نظرية، مستخدمًا 29500 منها في البرهان النهائي. عند 13 مليون سطر من Lean، تكون النتيجة أكثر من خمسة أضعاف حجم Mathlib، المكتبة المجتمعية الرئيسية للرياضيات الرسمية. يتبع الدليل عرضًا مبسطًا لحجة ويلز التي قدمها هنري دارمون، وفريد ​​دايموند، وريتشارد تايلور، ويقتبس أجزاء من مشروع إضفاء الطابع الرسمي على كلية إمبريال كوليدج لندن بقيادة كيفن بوزارد.

لماذا يحسم الدليل البسيط السؤال؟

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

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

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

ماذا يعني ذلك بالنسبة للرياضيات وأبحاث الذكاء الاصطناعي

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

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

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

---

ابقَ في طليعة الذكاء الاصطناعي

احصل على آخر الأخبار والتحليلات والإنجازات في مجال الذكاء الاصطناعي — كل ذلك في مكان واحد.

اقرأ المزيد من أخبار الذكاء الاصطناعي →