باحثون يرصدون تباينات في إثبات OpenAI لمعادلات نافييه–ستوكس المكتوب بلغة Lean

قارن باحثون إثبات OpenAI المنشور لمعادلات نافييه–ستوكس بنسخته الشكلية المكتوبة بلغة Lean، ورصدوا تباينات في عدة مواضع رئيسية. فالنسخة القابلة للتحقق آليًا تثبت في تلك المواضع عبارات أضعف من تلك المعلنة في النص الموجَّه للقرّاء البشر. وتندرج معادلات نافييه–ستوكس ضمن «مسائل الألفية» السبع التي أعلنها معهد كلاي للرياضيات، وخصّص لحل كل منها 1 مليون دولار، ولذلك يلفت أي شرخ في مثل هذه النتيجة الأنظار فورًا. ومع ذلك، فإن هذا ليس دحضًا للإثبات حتى الآن.

ما الذي اكتُشف بالضبط

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

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

لماذا يُعد «الادعاء الأضعف» أمرًا خطيرًا

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

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

الاحتمالان الأول والرابع غير ضارَّين، أما الثالث فخطير. وما دام المؤلفون أو خبراء مستقلون لم يفحصوا كل موضع على حدة، فلا يمكن الاختيار بين هذه الاحتمالات.

أبرز الحقائق من البيانات المتاحة:

• موضوع التحقق: إثبات OpenAI لمعادلات نافييه–ستوكس؛
• المنهج: مقارنة النص المنشور بنسخة Lean الخوارزمية؛
• النتيجة: تباينات في عدة مواضع رئيسية؛
• طبيعة التباينات: العبارات في النسخة الآلية أضعف؛
• الحالة: هذا ليس دحضًا بعد، بل سبب للشك.

ما الذي ينبغي متابعته لاحقًا

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

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