رياضيات مبرهنة فيرما تُصاغ رسميا بالذكاء الاصطناعي بعد 350 عاماًفي حدث علمي استضافته لندن بين 6 و10 يوليو 2026، أحرز رياضيون وباحثون في الذكاء الاصطناعي تقدماً سريعاً بشكل غير متوقع في مشروع طموح: تحويل برهان مبرهنة فيرما الأخيرة — أحد أشهر البراهين في تاريخ الرياضيات — إلى صيغة يمكن للحاسوب التحقق منها آلياً.من الورق إلى الآلةيقود المشروع الأستاذ كيفن بازارد من إمبريال كوليدج لندن، بتمويل من هيئة البحوث الهندسية والعلوم الفيزيائية البريطانية (EPSRC). يعمل الفريق على “أَسْلَمة” البرهان الذي وضعه أندرو وايلز وريتشارد تايلور في التسعينيات، داخل نظام Lean، وهو مُثبِت براهين يفحص كل خطوة منطقية بدقة متناهية. ولا يعتمد الفريق النسخة الأصلية حرفياً، بل صياغة أحدث تستند إلى أفكار خاري ووينتنبرغر، لما توفره من ملاءمة أكبر للأتمتة الحاسوبية.الذكاء الاصطناعي يدخل المعادلةالنقلة النوعية جاءت من تمويل شركة Logos Research، التي اقترحت تجربة “الأسلمة الذاتية” (autoformalization)، أي جعل نماذج الذكاء الاصطناعي تتولى بنفسها صياغة المتطلبات الرياضية الأولية للبرهان، وربما أفكار البرهان الرئيسية ذاتها. شاركت نماذج من OpenAI (ChatGPT Pro) ونظام Aristotle من Harmonic، بدعم من عالم الرياضيات تيرينس تاو، الذي شجّع مراراً على دمج الذكاء الاصطناعي في صياغة البراهين والتعاون الرياضي الجماعي.لماذا هذا مهم؟مبرهنة فيرما ليست الهدف النهائي — فهي مُثبتة منذ 1998 — بل الغاية اختبار قدرة أدوات الصياغة الرسمية على التعامل مع برهان ضخم يمتد لنحو 130 صفحة ويمس حقولاً رياضية متعددة. نجاح جزئي قد يمهّد الطريق لاستخدام الذكاء الاصطناعي في التحقق من براهين أخرى أكثر تعقيداً، بدلاً من الاعتماد على المراجعة البشرية البطيئة. كما يُغذّي المشروع مكتبة Mathlib الخاصة بنظام Lean، ما يجعله استثماراً طويل الأمد في البنية التحتية الرياضية.المصادر:مدونة Xena Project — Kevin Buzzardمستودع GitHub: ImperialCollegeLondon/FLTScience News
#بشرى الهادي#مجلة ايليت فوتو ارت.
