برهان رياضي كبير بمساعدة Claude وCodex يُتحقق منه في Lean، ومؤلفاه يصفان مسودته الأولى بأسوأ كتابة
المخرج الضخم الذي يصعب على البشر قراءته يصبح مقبولًا حين تقف خلفه أداة آلية تحكم بالصحة أو الخطأ، وهو الدور نفسه الذي تؤديه الـ tests للكود الذي تكتبه الوكلاء.
كتب عالم الرياضيات Terence Tao في 7 سبتمبر 2026 عن نتيجة جديدة توصل إليها Levent Alpöge، الباحث في Anthropic، وTristan Buckmaster من جامعة NYU. أثبت الباحثان حدوث blowup في زمن محدود، مع قوة خارجية سلسة، لمعادلات IPM وBoussinesq ثنائية الأبعاد ومعادلات Euler ثلاثية الأبعاد للموائع غير القابلة للانضغاط. والـ blowup يعني أن كمية فيزيائية تصل إلى ما لا نهاية خلال زمن محدود. ويبني العمل على نتائج سابقة لـ Córdoba وMartínez-Zoroa.
وصف Tao النتيجة بأنها إنجاز لافت وتقدم نحو مسألة الانتظام العام لمعادلات Navier-Stokes.
دور الذكاء الاصطناعي
بحسب التدوينة، كان العمل معتمدًا بدرجة كبيرة على AI. استُخدم Claude لمراجعة الأدبيات السابقة، واستُخدم Claude وCodex في الصياغة وفي ضبط حسابات الثوابت وخطوات الاستقراء، تحت إشراف بشري. ثم صيغ البرهان في Lean، وهو مساعد برهان يتحقق من كل خطوة آليًا بطريقة تشبه عمل الـ compiler، فلا يجامل ولا يتعب.
واللافت أن المؤلفين وصفا مسودتهما الأولى بأنها “أسوأ كتابة رأيناها في تاريخ الرياضيات”، ثم بذلا جهدًا كبيرًا لتبسيطها وإعادة كتابتها في صورة مهنية يقرؤها البشر.
تكشف القصة الشكل الذي يصبح فيه عمل الذكاء الاصطناعي مقبولًا: مخرج ضخم قد لا يفهمه أحد من القراءة الأولى، لكن خلفه أداة آلية تحسم صحته. وهذا قريب مما يحدث في تطوير البرمجيات. فالوكيل ينتج كودًا يعمل لكنه صعب الصيانة، وما يقابل Lean هناك هو الـ tests. ومن دونها يصبح الحكم الوحيد على الكود أنه عمل مرة واحدة.
أما الخطوة الأخيرة، أي تحويل البرهان إلى نص مفهوم، فأنجزها الباحثان بأنفسهما بعد أن اجتاز البرهان التحقق.