Anthropic تصيغ برهان مبرهنة فيرما الأخيرة بلغة Lean في 11 يومًا
حين يوجد حَكَم آلي يرفض الخطأ، يستطيع الـ agent العمل أيامًا وإخراج نتيجة صحيحة. وما لا يملك حكمًا كهذا، وهو أغلب البرمجيات، ما زال يحتاج مراجعة بشرية.
نشرت Anthropic في 4 سبتمبر 2026 نتيجة مشروع أعاد كتابة برهان مبرهنة فيرما الأخيرة بالكامل بلغة Lean، واستغرق العمل 11 يومًا. وبحسب صفحة البحث، بلغ الناتج 13 مليون سطر، و30,300 مبرهنة مبرهنة، دخلت منها 29,500 في البرهان النهائي، مع استهلاك نحو 6 مليارات output token.
والإنجاز ليس حل مسألة رياضية مفتوحة. فبرهان Andrew Wiles موجود منذ 1995. ما كان ينقص هو الصياغة الرسمية (formalization)، أي إعادة كتابة البرهان بلغة يتحقق منها الحاسوب سطرًا بسطر، فتصبح صحته مؤكدة آليًا لا بمراجعة البشر.
واعتمد العمل على منصة اسمها Prove2Me، تحتفظ بمخطط (graph) للمبرهنات وتوزعها، فيعمل عدة agents على فروع مختلفة في الوقت نفسه، بينما يقدم البشر توجيهات عامة على فترات فقط.
وما يهم المطورين هنا ليس الرياضيات، بل طبيعة التحقق. فهذا من أوضح الأمثلة حتى الآن على عمل فيه تحقق آلي حقيقي. المترجم (compiler) الخاص بـ Lean يرفض أي خطوة خاطئة، فلا يستطيع الـ agent أن يعلن انتهاء العمل وهو لم ينته. ولهذا أنتجت 11 يومًا من العمل المتواصل نتيجة صحيحة.
والوجه المقابل هو ما يستحق الانتباه. فالعمل الذي لا يوجد فيه حَكَم آلي على الصواب ما زال يحتاج إلى عين بشرية تراجعه، وهذا ينطبق على معظم الكود الذي يُكتب يوميًا. والفرق بين النوعين قد يحدد أين يمكن ترك الـ agents تعمل لفترات طويلة، وأين لا يمكن ذلك بعد.