كلود
ونتج عن ذلك نحو 13 مليون سطر من الشيفرة البرمجية بلغة “Lean”، وحوالي 29,500 مبرهنة وسيطة، وهو ما يعادل نحو خمسة أضعاف حجم مكتبة الرياضيات الرسمية “Mathlib” بأكملها.
يُذكر أن عالم الرياضيات الفرنسي بيير دي فيرما صاغ المبرهنة في القرن السابع عشر، لكن إثباتها ظل مستعصيا لأكثر من ثلاثة قرون، إلى أن تمكن عالم الرياضيات البريطاني أندرو وايلز من إثباتها في عام 1995، بعد نحو سبع سنوات من العمل عليها بسرية.
أما الصياغة الرسمية، فتعني ترجمة البرهان الرياضي إلى شيفرة حاسوبية تتيح للحاسوب التحقق من صحة كل خطوة فيه.
وحاول العديد من علماء الرياضيات إيجاد برهان لهذه المسألة، لكن محاولاتهم انتهت بالفشل. وعمل وايلز على المسألة سرا لمدة سبع سنوات، قبل أن يعلن عن توصله إلى اختراق كبير عام 1993. وغالبا ما تتكون البراهين الرياضية من سلاسل طويلة من الاستدلالات المنطقية التي يعتمد بعضها على بعض، بحيث إن تسلل خطأ إلى إحدى الخطوات قد يؤدي إلى انهيار البرهان بأكمله.
وهذا ما حدث بالفعل مع وايلز، عندما اكتُشفت ثغرة في برهانه، واستغرق الأمر نحو عام لسدها.
وتعمل رقمنة النظريات الرياضية، أو إضفاء الطابع الرسمي عليها، على نقلها من عالم “الورقة والقلم” إلى عالم الشيفرات البرمجية، بما يسمح للحواسيب بمعالجتها والتحقق من صحة منطقها خطوة بخطوة، وكشف أي أخطاء أو ثغرات فيها. ويحتوي المستودع المركزي “Mathlib” على نحو مليوني سطر من الرياضيات المصاغة رسميا.
وأمضى البروفيسور كيفن بازارد، من إمبريال كوليدج لندن، خمس سنوات في تنفيذ هذه المهمة، بينما أنجزها نموذج “Claude” في 11 يوما. ووفقا لبازارد، فإن البرهان “لا يعتمد على أي شيء سوى بديهيات الرياضيات”.
وقُسّمت المهمة بين وكلاء للذكاء الاصطناعي كانوا يتلقون توجيهات عامة بصورة دورية، وساعدتهم في تنسيق العمل أداة “Prove2Me”، التي صُممت في الأصل لمساعدة علماء الرياضيات البشر.
وإذا أصبحت هذه النتائج قابلة للتكرار بصورة موثوقة، فقد يتمكن الذكاء الاصطناعي من تسريع عملية ترجمة الرياضيات الحديثة إلى صيغ قابلة للتحقق آليا.
المصدر الأصلي: arabic.rt.com — للاطلاع على المادة الأصلية.