ده پیشرفت در ریاضیات و علوم نظری کامپیوتر

می‌خواهیم دانشمندان و ریاضی‌دانان را به ابزارهایی مجهز کنیم که سرعت اکتشاف را افزایش می‌دهند. به همین دلیل، به‌تازگی طرح ChatGPT for Academic Researchers⁠ را معرفی کردیم که دسترسی رایگان ۱۰۰٬۰۰۰ دانشمند و ریاضی‌دان را به بهترین مدل‌های ChatGPT ما فراهم می‌کند. همچنین همچنان در جریان توسعه، مدل‌هایمان را با مسائل حل‌نشدهٔ پژوهشی ارزیابی می‌کنیم.

در ماه مه، ابطال تولیدشده با هوش مصنوعی⁠ حدس فاصلهٔ واحد اردوش را منتشر کردیم که هنگام ارزیابی مدلی عرضه‌نشده کشف شده بود. این کار تاکنون الهام‌بخش پیشرفت‌های بیشتری در ریاضیات و علوم نظری کامپیوتر بوده است¹. امروز گزیده‌ای از ده نتیجه را منتشر می‌کنیم که هر یک مسئله‌ای حل‌نشده و دیرپا را حل کرده یا پیشرفت چشمگیری در آن رقم زده است. این مسائل هندسهٔ ابعاد بالا، نظریهٔ کدگذاری، پیچیدگی مدارهای حسابی، نظریهٔ گروه‌ها، جبرهای اپراتوری، پیچیدگی کوانتومی، رمزنگاری مشبکه‌ای و ترکیبیات اکسترمال را در بر می‌گیرند. همهٔ این مسائل برای جوامع ریاضی مرتبط اهمیت فراوانی دارند و چند مورد نیز برای کل حوزهٔ ریاضیات بسیار مهم‌اند.

برای مسائل زیر نتایج تازه‌ای ارائه می‌کنیم. این نتایج با نسخه‌ای داخلی از Astra، مدل بزرگ بعدی ما، به دست آمدند. هزینهٔ مجموع توکن‌های لازم برای یافتن راه‌حل این مسائل، با تعرفه‌های API مدل Sol، حدود ۲٬۰۰۰ دلار بود. سپس انسان‌ها با کمک همان مدل، این استدلال‌ها را در قالب مقاله آماده کردند. پس از آن، مدل هر استدلال را در قالب یک گواهی Lean⁠(در یک پنجره جدید باز می‌شود) صورت‌بندی صوری کرد. همچنین برای هر راه‌حل، روایت یک مدل از فرایند تفکرش را منتشر می‌کنیم.

1. بسته‌بندی کره‌ها در ابعاد بالا. کران‌های بالای جدید برای چگالی بسته‌بندی کره‌ها تا آستانهٔ کوهن–الکیس.
2. کدهای دودویی و کروی: کران‌هایی با بهبود نمایی برای حداکثر اندازهٔ کدهای دودویی با هر حداقل فاصلهٔ تعیین‌شده، همراه با نتایجی مشابه برای کدهای کروی در ابعاد بالا.
3. گروه‌های غیروسوفیک. ساختی که وجود گروه‌های غیروسوفیک را اثبات می‌کند و به پرسشی محوری و حل‌نشده در نظریهٔ گروه‌ها پاسخ می‌دهد.
4. حدس صلبیت کن. ابطال حدسی دیرپا مبنی بر اینکه برخی گروه‌ها به‌طور یکتا با جبرهای فون نویمان خود تعیین می‌شوند.
5. پیچیدگی مدارهای حسابی. کران‌های پایین جدید برای محاسبهٔ پرماننت با استفاده از مدارها و فرمول‌های حسابی، از جمله کران پایین مرتبهٔ n⁴/log n برای فرمول‌های حسابی.
6. تکرار موازی کوانتومی. قضیه‌ای برای تکرار موازی نمایی در بازی‌های کوانتومی عمومی دونفره که یکی از اصول بنیادی نظریهٔ پیچیدگی کلاسیک را تعمیم می‌دهد.
7. مسئلهٔ نزدیک‌ترین بردار. سختی تقریب با ضریب چندجمله‌ای برای مسئلهٔ نزدیک‌ترین بردار؛ پرسشی بنیادی دربارهٔ مشبکه‌ها که با رمزنگاری پساکوانتومی ارتباط دارد.
8. حدس حجم ارهارت. تعیین بیشترین حجم ممکن در هر بُعد برای جسمی محدب که مرکز جرم آن تنها نقطهٔ مشبکه‌ای درون آن باشد.
9. اعداد رمزی چندرنگ. کران پایینی ابرنمایی برای اعداد رمزی مثلث چندرنگ که مسئلهٔ ۱۸۳ اردوش را حل می‌کند.
10. حدس‌های اعداد اکسترمال. نتایجی دربارهٔ حدس‌های فشردگی و تباهیدگی در نظریهٔ اکسترمال گراف که مسائل ۱۴۶ و ۱۸۰ اردوش را حل می‌کنند.

ظهور سامانه‌هایی که می‌توانند در پژوهش‌های ریاضی مشارکت کنند، پرسش‌هایی را مطرح می‌کند که یک شرکت فناوری به‌تنهایی قادر به پاسخ‌گویی به آن‌ها نیست. دربارهٔ نقش هوش مصنوعی در ریاضیات دیدگاه‌های فراوانی وجود دارد و ما برای کسانی که نگران پیامدهای آن هستند، از جمله امضاکنندگان بیانیهٔ لیدن دربارهٔ هوش مصنوعی و ریاضیات⁠(در یک پنجره جدید باز می‌شود)، احترام و درک عمیقی قائلیم. به باور ما، انتساب باید صادقانه نشان دهد که یک نتیجه چگونه به دست آمده است: نسبت‌دادن اثباتی که کاملاً به‌وسیلهٔ یک سامانهٔ هوش مصنوعی تولید شده به نویسنده‌ای انسانی، هم نقش سامانه و هم ماهیت کار فکری اصیل انسان را نادرست جلوه می‌دهد. ما به آماده‌سازی مقاله‌ها و صورت‌بندی صوری اثبات‌ها در Lean کمک کردیم و مسئولیت درستی آن‌ها را می‌پذیریم، اما استدلال‌های ریاضی را سامانهٔ ما تولید کرده است. امیدواریم جامعهٔ ریاضی این نتایج را عمیقاً بررسی کند، آن‌ها را در بستر مناسب قرار دهد و با پژوهش‌ها و اکتشافات تازه، ایده‌های نهفته در آن‌ها را به ثمر برساند.

با تکامل سامانه‌های هوش مصنوعی و تبدیل آن‌ها به همکاران پژوهشی پیشرفته‌تر، فراهم‌کردن دسترسی گسترده برای حمایت از دانشمندان و ریاضی‌دانانی که در این دوران تحول‌آفرین مسیر آیندهٔ رشته‌های خود را می‌پیمایند و تعریف می‌کنند، ضرورتی بنیادی است.