الذكاء الاصطناعي يساعد للمرة الأولى في التحقق الشكلي من براهين حائزة على جائزة فيلدز

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

نالت فيازوفسكا الميدالية لحلّها واحدة من أكثر مسائل الرياضيات أناقةً ومكرًا، وهي مسألة رصّ الكرات. تبدو المسألة بسيطة: كيف نرتّب كرات متطابقة في الفضاء بأقصى كثافة ممكنة؟ في بعدين يعرف الجواب كل مربّي نحل، فهو خلايا العسل السداسية. وفي ثلاثة أبعاد يكون الترتيب الأمثل هرمًا من الكرات، كما في أكوام البرتقال المألوفة على واجهات المحال. لكن المسألة تغدو شديدة التعقيد مع ازدياد عدد الأبعاد. في عام 2016 أثبتت فيازوفسكا أن البنية المتناظرة E8 هي أفضل رصّ في الفضاء ثماني الأبعاد، وبعد وقت قصير أثبتت مع زملائها أن شبكة ليتش (Leech) هي المثلى في 24 بُعدًا. ورغم أن هذه النتائج تبدو مجرّدة، فإنها ترتبط مباشرة بشيفرات تصحيح الأخطاء التي تستخدمها الهواتف الذكية والمسابير الفضائية.

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

بدأ كل شيء بلقاء عابر. ففي لوزان، أخبر الطالب في السنة الثالثة سيدهارت هاريهاران فيازوفسكا كيف يستخدم صياغة البراهين في لغة Lean لفهم المفاهيم الرياضية فهمًا عميقًا. ولغة Lean هي في الوقت نفسه لغة برمجة وما يُسمّى «مساعد براهين»، إذ تتيح كتابة الاستدلال الرياضي بصيغة يستطيع الحاسوب التحقق من صحتها المطلقة. أبدت فيازوفسكا اهتمامًا، وفي مارس 2024 وُلد مشروع Formalising Sphere Packing in Lean. وانضم إليه خبراء من إمبريال كوليدج لندن وجامعة إيست أنجليا وجامعة كاليفورنيا في بيركلي. وأعدّ الفريق «مخططًا» يمكن للبشر قراءته، وهو خريطة لجميع عناصر البرهان في الأبعاد الثمانية، تبيّن العناصر التي صيغت شكليًا بالفعل وتلك التي لا يزال ينبغي نقلها إلى لغة Lean.

استمر العمل الدؤوب عامين، ثم حدث التحول. ففي أكتوبر 2025 انضمت إلى المشروع شركة Math, Inc. الناشئة، التي طوّرت نظام الذكاء الاصطناعي Gauss. وهو ليس نموذجًا لغويًا تقليديًا، بل «وكيل استدلالي» قادر على التناوب بين الاستدلال بلغة طبيعية والاستنتاج الرياضي المصاغ شكليًا بالكامل. أي أنه ذكاء اصطناعي يعرف كيف يترجم البراهين الرياضية تلقائيًا إلى لغة يفهمها المدقق الحاسوبي. وقد أسرع إشراك Gauss عملية الصياغة الشكلية بصورة جذرية، فأتاح إنجاز ما كان سيستغرق سنوات أخرى من العمل اليدوي.

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

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

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