الذكاء الاصطناعي يحوّل مبرهنة فيرما الأخيرة إلى أكبر برهان بلغة Lean حتى الآن

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

لا يحل هذا الإنجاز محل البرهان البشري الذي أنجزه أندرو وايلز وريتشارد تايلور في تسعينيات القرن الماضي، ولا يوسّعه. بل يحوّل ذلك الاستدلال الراسخ إلى صيغة يستطيع الحاسوب التحقق منها خطوة بخطوة. وتنص المبرهنة على أنه لا توجد أعداد صحيحة تحقق المعادلة aⁿ + bⁿ = cⁿ عندما تكون n أكبر من 2.

قدّم خبراء بشريون إرشادات عامة من حين إلى آخر. وواجه الوكلاء في البداية صعوبة في التنسيق، لكنهم نجحوا بعد استخدام Prove2Me، وهي أداة تعاون ساعدتهم على تتبع المهام المنجزة واختيار ما ينبغي معالجته تالياً. وأجرى عالم الرياضيات كيفن بازارد عملية تجميع الشيفرة الناتجة وشغّل اختبارات Lean القياسية، وخلص إلى أنها تبني بالفعل الأسس الرياضية المطلوبة.

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