اجتمع باحثون في لندن هذا الأسبوع لتسريع صياغة مبرهنة فيرما الأخيرة باستخدام نماذج ذكاء اصطناعي متقدمة. وتركز ورشة العمل على تحويل إثبات أندرو وايلز لعام 1993 إلى كود بلغة "Lean" للتحقق منه حاسوبياً. وقد كان التقدم سريعاً، حيث تضاعفت أسطر الكود بعد اليوم الأول.
اجتمع خمسة وعشرون من علماء الرياضيات وعلوم الحاسوب وخبراء الذكاء الاصطناعي في فندق بوسط لندن للعمل على المشروع الذي يقوده كيفن بوزارد من إمبريال كوليدج لندن. ويهدف هذا الجهد الذي يمتد لخمس سنوات، والذي تم تمويله في عام 2024، إلى إضافة المبرهنة إلى مستودع "Mathlib" للرياضيات المصاغة رسمياً.
قبل ورشة العمل، كان هناك 20,000 سطر من الكود في المشروع. وبعد اليوم الأول، وصل الإجمالي إلى 40,000 سطر. وأشار بوزارد إلى أن قدرات الذكاء الاصطناعي تحسنت بشكل حاد منذ ديسمبر من العام الماضي، مما سمح للفريق بمعالجة المزيد من الرياضيات الأساسية أكثر مما كان مخططاً له في الأصل.
وصف هانغ لو سو، من إمبريال كوليدج لندن أيضاً، العملية بأنها تصنيع للعمل الفكري. ويستخدم المشاركون نماذج تشمل "Claude" لإنشاء الكود وتنقيحه، على الرغم من بقاء مخاوف بشأن الإسهاب وقابلية الصيانة طويلة المدى للمخرجات التي ينتجها الذكاء الاصطناعي.
وأعرب بوزارد عن ثقته في أن الأهداف الأصلية ستتحقق بحلول نهاية المشروع. وسيعتمد مدى التقدم الذي سيحققه الفريق في الهرم الكامل للنظريات الداعمة على التطورات المستقبلية في مجال الذكاء الاصطناعي.