رمزگشایی از ۴ ادعای بزرگ OpenAI در ریاضیات؛ از فرضیه ریمان تا بازی‌های یکتادر میان صدها مقاله منتشرشده در مخزن ریاضیات OpenAI، چهار ادعای کلیدی وجود دارد که در صورت تایید نهایی توسط جامعه دانشگاهی، تاریخ ریاضیات و علوم کامپیوتر را دگرگون می‌کنند. نخستین و جذاب‌ترین دستاورد، پیشرفت روی حدس شبه‌ریمان است. توزیع صفرهای تابع زتا قلب تپنده نظریه اعداد است و محل قرارگیری آن‌ها رفتار تمام اعداد اول جهان را تعیین می‌کند. حدس کلاسیک ریمان ادعا می‌کند تمام صفرها روی خط ۱/۲ قرار دارند، اما تاکنون هیچ ریاضیدانی موفق نشده بود حتی یک نوار ثابت و پهن از این صفحه را به عنوان محدوده بدون صفر پاکسازی کند. مدل OpenAI ادعا کرده است که هیچ صفری با بخش حقیقی بزرگتر از ۷/۸ وجود ندارد و کد اعتبارسنجی کامل آن در زبان Lean ۴ را نیز ارائه داده است.
دومین شگفتی بزرگ، اثبات حدس بازی‌های یکتا (Unique Games Conjecture) است؛ معمایی ۲۴ ساله در نظریه پیچیدگی محاسباتی که سوبهاش خوت در سال ۲۰۰۲ مطرح کرد. این مسئله مشخص می‌کند رایانه‌ها تا چه حد می‌توانند برای مسائل فوق‌سخت بهینه‌سازی، پاسخ‌های تقریبی تولید کنند. اثبات این فرضیه نشان می‌دهد الگوریتم‌های تقریبی فعلی ما برای مسائلی مانند Max-Cut، بهترین الگوریتم‌های ممکن تاریخ هستند و هیچ مهندسی نمی‌تواند به تقریب بهتری برسد، مگر اینکه روزی ثابت شود P = NP است. این دستاورد نیز مانند شبه‌ریمان، همراه با اثبات رایانه‌ای در Lean منتشر شده است.
دو ادعای بزرگ دیگر به هندسه جبری و آنالیز تابعی مربوط می‌شوند. در هندسه، مدل ادعای حل حالت خاصی از حدس هاج برای واریته‌های آبلی با ضرب مختلط (CM) را مطرح کرده است؛ مسئله‌ای از جوایز هزاره که ارتباط میان ساختارهای توپولوژیکی یک فضا و زیرفضاهای جبری آن را می‌سنجد (این مورد هنوز فاقد کد Lean است و متن آن بازنویسی انسانی شده است). در نهایت، حل مسئله فاکتورهای گروه آزاد که از دهه ۱۹۴۰ توسط فون نویمان و موری بی‌پاسخ مانده بود، اثبات می‌کند که جبرهای عملگری برآمده از گروه‌های آزاد با ۲ و ۳ مولد کاملاً هم‌ارز و ایزومورف هستند. اگرچه تایید قطعی این دستاوردها ماه‌ها زمان می‌برد، اما وجود کدهای اثبات ماشینی در اکثر آن‌ها، امکان بررسی سریع و قطعی را به جامعه علمی هدیه داده است.
@ACCELERATIONERS
