ساعد AI لأول مرة في التحقق الرسمي من براهين حائزة على ميدالية فيلدز

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

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

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

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

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

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

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

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