يُبسط الذكاء الاصطناعي إثبات خمنية ساندوف

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