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

حوالي عام 1637، دوّن بيير دي فيرما ادعاءً في هامش نسخته من كتاب الحساب لديوفانتوس سيصبح واحدًا من أشهر التخمينات الرياضية على الإطلاق: لا توجد أعداد صحيحة موجبة a، b، c تحقق aⁿ + bⁿ = cⁿ لأي n > 2. تبين أن نظرية فيرما الأخيرة (FLT)، كما أصبح التخمين معروفًا، صعبة للغاية في إثباتها. أول برهان، من السير أندرو وايلز في عام 1995، بلغ 129 صفحة وتطلب أشهرًا من العمل المضني للتحقق.

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

مؤخرًا، تيان يي بينغ، باحث في Anthropic ومجموعته في جامعة كولومبيا تبني أدوات للصياغة الرسمية بالذكاء الاصطناعي، شرع في اختبار ما إذا كان Claude قادرًا على إحراز تقدم في صياغة FLT. كانت النتيجة أبعد مما توقع. في 11 يومًا، عمل بشكل مستقل إلى حد كبير، أنتج Claude أول برهان شامل ومُتحقَّق منه بالحاسوب لنظرية FLT. على طول الطريق، كتب 13 مليون سطر من Lean وأثبت 29,500 نظرية وسيطة.