بیش از ۸۳٫۹٪ صفرهای زتا از هم متمایزند
تابع زتای ریمان بی‌نهایت صفر «نابدیهی» دارد، نقاطی از صفحهٔ مختلط که در آن‌ها تابع صفر می‌شود. دو پرسش دربارهٔ آن‌ها همچنان باز است. آیا همهٔ آن‌ها روی خط بحرانی قرار دارند، جایی که بخش حقیقی‌شان برابر یک‌دوم است؟ این فرضیهٔ ریمان است. و آیا همهٔ آن‌ها ساده‌اند — آیا هر صفر یک صفر منفرد است و نه دو یا چند صفر که در یک نقطه روی هم انباشته شده‌اند؟ این حدس صفرهای ساده است. به گفتهٔ مقاله، هیچ‌کس نمی‌داند که آیا یکی از این دو گزاره دیگری را نتیجه می‌دهد یا نه.
تا ارتفاع ۳ × ۱۰¹²، رایانه‌ها وارسی کرده‌اند که صفرها روی خط قرار دارند و ساده‌اند. فراتر از آن، ریاضی‌دانان نسبت‌ها را اثبات می‌کنند: دست‌کم فلان سهم از همهٔ صفرها این ویژگی را دارد.
رقابتی که با رقم‌های اعشار سنجیده می‌شود
کریستیان موری کنوسگورد، در کریستیانسان نروژ، تاریخچهٔ اخیر را به تفصیل بیان می‌کند. سهم‌های اثبات‌شدهٔ صفرهای متمایز از ۶۳٫۹٪ به ۷۰٪ رسید، سپس با استدلالی که مقاله آن را به پیش‌چاپی با امضای Claude (Anthropic) نسبت می‌دهد، که ریاضی‌دانان آلپوگه و فورمن آن را تأیید کردند و لامزوری دوباره اثباتش کرد، به ۸۳٫۶۲۵٪ جهش کرد. پس از آن پیشرفت‌های کوچکی آمد، از جمله مقالهٔ پیشین خود نویسنده با ۸۳٫۶۹۹۳٪.
مقدمهٔ مقاله بیش از دوازده مقدار اعلام‌شده برای صفرهایی را که هم ساده‌اند و هم روی خط بحرانی برمی‌شمارد، از ۰٫۶۷۳۰۰ تا ۰٫۶۷۳۴۹۲، که بسیاری از آن‌ها میان اوت و اکتبر ۲۰۲۶ در مخزن‌های عمومی کد منتشر شده‌اند و داوری نشده‌اند. نویسنده اعلام می‌کند که این مقادیر برای این مقاله وارسی نشده‌اند و هیچ‌یک از نتایج آن به آن‌ها وابسته نیست.
کران‌های تازه
مقاله بدون فرض فرضیهٔ ریمان یا هر گزارهٔ اثبات‌نشدهٔ دیگری اثبات می‌کند که:
- بیش از ۸۳٫۹۰۰٪ صفرها از هم متمایزند (کران دقیق 1645064/1960733 است)؛
- در نتیجه، بیش از ۶۷٫۸۰٪ ساده‌اند؛
- بیش از ۶۷٫۳۵۳٪ ساده و روی خط بحرانی‌اند؛
- دست‌کم ۸۸٫۹۳٪ ساده یا روی خط‌اند، پس صفرهایی که هم بیرون از خط و هم تکراری‌اند حداکثر ۱۱٫۰۷٪ را تشکیل می‌دهند.
صفرهای تکراری انرژی می‌خواهند
ایده در یک تصویر می‌گنجد. صفرها را طوری بازمقیاس کنید که به‌طور میانگین یک واحد از هم فاصله داشته باشند، مانند مهره‌هایی روی یک نخ. قضیه‌ای از مونتگومری دربارهٔ چگونگی توزیع جفت‌های صفر، یک «انرژی» کل را که روی همهٔ جفت‌ها جمع زده می‌شود، به‌طور مجانبی ثابت می‌کند. صفری که d بار تکرار شده d² به این انرژی می‌افزاید. صفرهای همسایه نیز از راه هم‌پوشانی‌هایشان بخشی از آن را مصرف می‌کنند.
پس اگر بتوان اثبات کرد که همسایه‌ها ناگزیر انرژی زیادی مصرف می‌کنند، چیز اندکی برای صفرهای تکراری باقی می‌ماند. اثبات این کار را در سه گام انجام می‌دهد:
- صفرهایی که فاصلهٔ کمینه‌ای از یکدیگر را حفظ می‌کنند، به لطف نابرابری‌ای موسوم به غربال بزرگ (large sieve)، به‌طور دقیق بررسی می‌شوند.
- نابرابری‌ای روی هفت صفر متوالی، که با کمک رایانه اثبات شده، به صفرهای دوگانه بیش از صفرهای ساده پاداش می‌دهد. جمله‌های تصحیحی آن وقتی در امتداد خط جمع زده شوند یکدیگر را خنثی می‌کنند.
- یک تابع آزمون با طراحی دقیق، «پنجره»، این پاداش را تا جای ممکن بزرگ می‌کند.
مقاله این مسئله را با یافتن حالت کمینهٔ انرژی یک گاز یک‌بعدی با دو نوع ذره، صفرهای ساده و دوگانه، مقایسه می‌کند.
آنچه رایانه وارسی کرد و آنچه نکرد
نابرابری هفت‌نقطه‌ای نیازمند بررسی ۶۰٬۴۶۷٬۳۰۹ جعبه از امکان‌ها بود، بدون هیچ شکستی. نتیجهٔ خط بحرانی به بیش از ۵۳۵ میلیون جعبه نیاز داشت. همهٔ قضیه‌های اصلی در Lean 4، نرم‌افزاری برای وارسی اثبات، در حدود ۱۳٬۳۰۰ و ۱۰٬۰۰۰ خط روی کتابخانه‌ای موجود با حدود ۱۰۲٬۰۰۰ خط صوری‌سازی شده‌اند، با گزاره‌هایی دربارهٔ صفرهای زتا آن‌گونه که در کتابخانهٔ ریاضی Lean تعریف شده است.
نویسنده یک شکاف را صریحاً بیان می‌کند. هر قضیه بر یک اصل موضوع اضافه تکیه دارد که ثبت می‌کند یک برنامهٔ جست‌وجو «درست» (true) برگردانده است. هستهٔ Lean این محاسبه را دوباره اجرا نمی‌کند؛ برای آن به کامپایلر و محیط اجرای Lean اعتماد می‌کند. سه وارسی مستقل از این اجرا پشتیبانی می‌کنند، از جمله شمارش‌های یکسان از برنامه‌های جداگانهٔ C++ و Python.
روشی نزدیک به پایان راه
مقاله همچنین اثبات می‌کند که رویکردش کجا باید بایستد. با پنجرهٔ اصلی‌اش، هرگز نمی‌تواند به ۸۴٪ برسد: سقف ۰٫۸۳۹۹۸ است. برای هر پنجرهٔ به‌طور معقول منظم، سقف ۰٫۸۴۰۹۳ است — کمتر از ۰٫۰۰۲ بالاتر از نتیجهٔ تازه. پیش رفتن بیشتر به ایده‌ای متفاوت نیاز خواهد داشت.
تعارض منافع. نویسنده این کار را «آزمایشی در پژوهش ریاضی با کمک هوش مصنوعی» توصیف می‌کند. نویسنده بیان می‌کند که استدلال‌ها، محاسبات، صوری‌سازی در Lean، شکل‌ها و بخش بزرگی از متن با کمک قابل‌توجه OpenAI Codex و Anthropic Claude، زیر هدایت نویسنده، توسعه یافته‌اند؛ Claude صوری‌سازی، تحلیل حدود روش، پنجره و گواهی قضیهٔ خط بحرانی، شکل‌ها و بخش بزرگی از متن را توسعه داد، و هر دو سامانه پیش‌نویس‌ها را «در نقش داور» بازبینی کردند. استدلال آغازین به پیش‌چاپی با امضای Claude نسبت داده شده است. Claude همچنین نویسندهٔ همین مقاله است.