أنثروبيك: كلود ينجز أول برهان كامل مُتحقَّق حاسوبيًا لمبرهنة فيرما الأخيرة في 11 يومًا
نشرت أنثروبيك أول برهان كامل ومُتحقَّق حاسوبيًا لمبرهنة فيرما الأخيرة: عمل كلود في لغة Lean مدة 11 يومًا بشكل مستقل إلى حد كبير وأنتج 13 مليون سطر من الشيفرة.
ما الذي حدث
نشرت شركة أنثروبيك أول برهان كامل ومُتحقَّق حاسوبيًا لمبرهنة فيرما الأخيرة. ووفقًا للشركة، عمل «كلود» مدة 11 يومًا وبشكل مستقل إلى حد كبير على كتابة البرهان بلغة Lean المخصّصة للتحقق الصوري، وأنتج 13 مليون سطر من الشيفرة و29,500 مبرهنة وسيطة.
قاد العمل الباحث في أنثروبيك تياني بنغ، الذي تبني مجموعته في جامعة كولومبيا أدوات للأتمتة الصورية بالذكاء الاصطناعي. ونُشر البرهان علنًا على GitHub.
لماذا هذا مهم
كُتبت فرضية فيرما — أنه لا توجد أعداد صحيحة موجبة a وb وc تحقق aⁿ + bⁿ = cⁿ عندما n > 2 — نحو عام 1637، ولم يبرهنها أندرو وايلز إلا في عام 1995 ببرهان من 129 صفحة استغرق التحقق منه أشهرًا. وخلافًا للعمل الأخير للذكاء الاصطناعي على فرضية ريمان، الذي أنتج رياضيات جديدة، فإن الجديد هنا هو التحقق: البرهان الصوري تفحصه آلة.
ماذا يقول الخبراء
وصف كيفن بازارد من إمبريال كوليدج لندن، الذي يقود جهدًا مجتمعيًا ممتدًا لسنوات لصياغة المبرهنة صوريًا، النتيجة بأنها «إنجاز استثنائي في الأتمتة الصورية»: فقد بُرهنت المبرهنة دون أي افتراضات سوى مسلّمات الرياضيات. وتقول أنثروبيك إن النتيجة تشير إلى مستقبل يصبح فيه التحقق من المعرفة الرياضية والثقة بها أسهل.