كلاود يكمل أول إثبات شكلي لمبرهنة فيرما الأخيرة في 11 يوماً
أعلنت شركة أنثروبيك يوم 4 سبتمبر عن إنجاز باحثين بقيادة تيان يي بنغ لإتمام أول إثبات كامل ومُنظَّم آلياً لنظرية فيرما الأخيرة. استغرق النموذج اللغوي كلاود 11 يوماً فقط لإكمال هذه المهمة المعقدة تحت إشراف بشري محدود، في خطوة تُظهر قفزة نوعية في قدرات الذكاء الاصطناعي على هندسة المشاريع الرياضية الضخمة وإدارة البراهين المنطقية. اعتمد الفريق على منصة Prove2Me التي طوّرها، حيث تفاعل عشرات وكلاء كلاود بشكل متزامن لتوليد حوالي 13 مليون سطر من كود Lean، مع استهلاك نحو 6 مليارات رمز إخراجي. نجح النظام في إثبات نحو 30,300 نظرية وسيطة، استُخدم منها حوالي 29,500 نظرية لتشكيل الهيكل النهائي. تتبع العملية المسار الرياضي لأندرو وايلز وريشارد تايلر، مع تفكيك السلسلة الاستنتاجية إلى وحدات مستقلة قابلة للمعالجة الآلي، مما يتيح لكل عامل التركيز على جزئية محددة مع الربط المنطقي عبر منصة التعاون المركزية. تضمنت عملية المراجعة إجراءات تحقّق صارمة تتجاوز التجميع البرمجي التقليدي. استخدم الفريق أداة comparator لمطابقة الدلالة الرياضية النهائية مع المكتبات المرجعية، ثم أعاد تدقيق الإثبات عبر نواة Lean المستقلة nanoda التي استقبلت أكثر من مليون ادعاء. لم تعتمد النتائج إلا على ثلاث بديهيات رياضية قياسية، مما يؤكد خلوّ السلسلة من الفجوات المنطقية أو التحريف غير المصرح به. وتكمن القيمة الأبرز لهذا الإنجاز في تقديم إطار عملي لمعالجة إشكالية التحقق من صحة البراهين التي يولّدها الذكاء الاصطناعي، وهي قضية حاسمة مع تزايد الاعتماد على الآلات في البحث الرياضي. رغم الدقة التقنية، يشير التقرير إلى أن الإثبات المُنظَّم آلياً لا يزال يفتقر إلى الكثافة الهندسية والكفاءة المتعارف عليها، حيث يتجاوز حجم الكود حجم المكتبة الرياضية المرجعية بخمس مرات بسبب التكرار وعدم التحسين النهائي. كما لم تُكشف التكاليف الحسابية الكلية أو تقارن الجهود بالعمليات البشرية التقليدية. ومع ذلك، يظل هذا المشروع علامة فارقة تثبت جدارة الذكاء الاصطناعي في إدارة المشاريع الرياضية الشاسعة، مما يمهد الطريق لتطوير أدوات مساعدة أكثر موثوقية وقابلية للصيانة في المستقبل.
