ما الذي تحقق بالضبط؟
أعلنت Anthropic أول صياغة كاملة قابلة لفحص الحاسوب لمبرهنة فيرما الأخيرة داخل Lean. يمر المستودع عبر أداة التحقق بلا مواضع sorry أو مسلمات مضافة خارج إطار Lean القياسي.
هذا لا يعني أن الذكاء الاصطناعي وجد برهانًا جديدًا للمبرهنة. البرهان الرياضي معروف منذ عمل أندرو وايلز في التسعينيات؛ الجديد هو تحويله إلى لغة رسمية يمكن للحاسوب مراجعة خطواتها.
هل بُني كل شيء من الصفر؟
لا. استفاد المشروع من مكتبة Mathlib ومن مشاريع وصياغات بشرية مفتوحة سابقة. وراجع الخبير Kevin Buzzard بناء المستودع وقارن العبارة النهائية، لكن ذلك لا يساوي تدقيقًا بشريًا يدويًا لكل واحد من ملايين الأسطر.
الخلاصة الدقيقة: الإنجاز يجعل برهانًا معروفًا قابلًا للتحقق آليًا؛ لا يقدم رياضيات جديدة، ولا يثبت أن العمل تم بلا تدخل بشري أو من الصفر.