چگونه OpenAI اثبات معادلات Navier-Stokes خود را به طریق غلط به کد ترجمه کرد

آنچه که OpenAI اعلام کرد

OpenAI در ۸ سپتامبر ۲۰۲۶ اعلام کرد که سیستم چند عاملی داخلی خود اثباتی برای مسئله وجود و صافی Navier-Stokes تولید کرده است، که یکی از هفت مسئله جایزه هزاره است که جایزه‌ای ۱ میلیون دلاری از موسسه ریاضیات Clay به همراه دارد، به گفته سایت ردیابی هوش مصنوعی implicator.ai. شرکت گزارش داد که تقریباً ۱۰٬۰۰۰ عامل برای ۸۸ ساعت شروع از ۲۸ اگست کار کردند و ۲٫۷ میلیون پیام عامل و حدود ۱۳۰ میلیارد توکن خروجی تولید کردند، قبل از آنکه یک مدل جداگانه، که به عنوان GPT-6 Astra توصیف شده است، ۱۷ ساعت بیشتر صرف برای بررسی رسمی استدلال در زبان اثبات Lean کند.

نتیجه یک دست‌نوشته متن طبیعی با عنوان "Finite time blowup for Navier–Stokes" بود، که همراه با پروژه Lean که هدف آن اجازه دادن به رایانه‌ها برای بررسی هر مرحله منطقی است، به گفته implicator.ai و مقاله arXiv که بعداً کار را تجزیه و تحلیل کرد.

یافته‌های خطای ترجمه

مقاله‌ای که روی سرور پیش‌چاپ arXiv منتشر شد، با عنوان "Navier-Stokes Lost in Translation" و نوشته‌ی ریاضی‌دانان Alexander Bastounis، Fabian Circelli و Anders C. Hansen، بررسی کرد که آیا کد Lean از OpenAI واقعاً با استدلال ریاضیاتی در مقاله متن طبیعی مطابقت دارد. نویسندگان بین اثبات Lean که صرفاً کامپایل می‌شود و آن‌چه که از لحاظ معنا‌شناسی وفادار به استدلال اصلی است، تمایز قائل می‌شوند و استدلال می‌کنند که نوع دوم بسیار سخت‌تر از اولی است.

مقاله عدم تطابق‌های مشخصی را فهرست می‌کند. در یک مورد، Lemma 8.6 مقاله متن طبیعی نیاز به محدود کردن مشتقات با استفاده از چهار مرتبه ورودی اضافی دارد که به صورت m+4 نوشته می‌شود، اما قضیه Lean متناظر به جای آن نیاز به پنج مرتبه اضافی دارد، m+5 — شرطی قوی‌تر از آنچه که مقاله بیان می‌کند. در مورد دیگر، معادله ۱۰٫۱۹ دست‌نوشته محدودیت یک جمله فشار-شار را با استفاده از تنها یک متغیر به نام B_R محدود می‌کند، در حالی که نسخه Lean همان محدودیت نیز به متغیر دوم A_R بستگی دارد، که از تکنیک ریاضیاتی متفاوتی مشتق شده است.

نویسندگان نتیجه می‌گیرند که پرونده Lean که با موفقیت کامپایل می‌شود تنها نشان می‌دهد که برای قضیه بیان شده برخی اثبات صحیح موجود است، نه اینکه اثبات یکسان است که به‌طور کلامی توصیف شده است. آن‌ها می‌نویسند که کد Lean از OpenAI اغلب شروط قوی‌تری را برای محدودیت‌های توابع مختلف نسبت به نتایج متناظر در مقاله متن طبیعی اعمال می‌کند، و آن‌ها توصیه می‌کنند که Navier-Stokes و رسمی‌سازی‌های معادله Euler مرتبط از OpenAI همان بررسی نقادانه‌ای را که اثبات‌های سنتی دریافت می‌کنند، قبل از قابل اعتماد شدن، طی کنند.

اختلاف جداگانه: کدام مسئله حل شده است؟

مستقل از سؤال ترجمه، چندین ریاضی‌دان بر سر اینکه OpenAI نسخه‌ای از Navier-Stokes را که بیشتر محققان به آن اهتمام می‌دهند، حل کرده است، اختلاف نظر داشتند. بیان مسئله رسمی موسسه Clay از سال ۲۰۰۰، نوشته‌ی Charles Fefferman، گزینه‌ای برچسب خورده با C را شامل می‌شود که اجازه جمله نیروی بیرونی صاف را می‌دهد، در حالی که بیشتر ریاضی‌دانان بر روی حالت غیر اجباری تمرکز کرده‌اند، به گفته Scientific American.

اثبات OpenAI گزینه C را هدف قرار می‌دهد. Luis Silvestre از دانشگاه شیکاگو و همکاران مقاله‌ای منتشر کردند که استدلال می‌کنند مکانیسم blowup از OpenAI پس از حذف نیروی خارجی کار نمی‌کند، به گفته Scientific American.

بخشی از الگوی گسترده‌تر نقد و بررسی

تحقیق در ادعاهای ریاضیاتی OpenAI جدید نیست. در اکتبر ۲۰۲۵، Kevin Weil، معاون رئیس سابق OpenAI، گفت که GPT-5 ده مسئله حل نشده Erdős را حل کرده است و پیشرفتی روی یازده مورد دیگر ایجاد کرده است؛ ریاضی‌دانانی از جمله Thomas Bloom گفتند که نتایج در حال حاضر در ادبیات منتشر شده وجود دارد، و Weil پست را پس گرفت، به گفته TechCrunch. وقتی OpenAI در می ۲۰۲۶ اعلام کرد که مدل استدلال‌گر حدسی هندسی Erdős از سال ۱۹۴۶ را رد کرده است، بیانیه‌های حمایتی از ریاضی‌دانان Noga Alon، Melanie Wood و Thomas Bloom — همان Bloom که خطای قبلی را پرچم‌گذاری کرده بود — در کنار ادعا منتشر کرد، به گفته TechCrunch.

در ۷ اکتبر ۲۰۲۶، OpenAI ۳۷۲ نتیجه ریاضیاتی تولید شده توسط هوش مصنوعی را روی GitHub منتشر کرد، هر کدام هدف آن حل کردن یک مسئله باز یا پیشرفت قابل توجهی نسبت به آن است، بیشتر از یک پرومپت منفرد به یک مدل داخلی با هزینه حدود سه ساعت حساب ChatGPT Pro برای هر کدام تولید شده‌اند، به گفته the-decoder. بیست و پنج برنده جایزه Fields Medal نامه‌ای باز امضا کردند که هشدار می‌دهند تولید انبوه نتایج ریاضی صحیح می‌تواند به جای پیشرفت آن، به زمینه آسیب برساند، به گفته همان گزارش، که یادآوری کرد بیشتر نتایج از بررسی نقادانه معیاری عبور نکرده‌اند.

جایی که ادعا اکنون قرار دارد

موسسه ریاضیات Clay هنوز Navier-Stokes را در میان مسائل جایزه هزاره حل نشده فهرست می‌کند، به گفته implicator.ai. رئیس موسسه Martin Bridson گفت که اعلام خیلی هیجان‌انگیز بود اما هر گونه ارزیابی رسمی آهسته و دقیق خواهد بود.