پنج جسم، شمار محدودی از رقص‌های بی‌نقص
چند ستاره یا سیاره را تصور کنید که چنان دقیق چیده شده‌اند که کل گروه می‌تواند بی‌آن‌که شکلش عوض شود، مانند جسمی صلب بچرخد. برای این کار، کشش گرانش بر هر جسم باید دقیقاً به سوی مرکز جرم گروه باشد و شدتش با فاصلهٔ جسم از آن متناسب. چنین آرایش‌هایی را پیکربندی‌های مرکزی (central configurations) می‌نامند. این‌ها شکل‌های جواب‌های ویژهٔ مسئلهٔ n جسم هستند که در آن‌ها اجسام الگوی نسبی‌شان را حفظ می‌کنند، از جمله تعادل‌های نسبی (relative equilibria) که صلب‌وار می‌چرخند.
اگر الگویی جواب بدهد، هر نسخهٔ چرخانده، بزرگ‌شده یا جابه‌جاشدهٔ آن هم جواب می‌دهد، پس ریاضی‌دانان آن‌ها را «در حد تشابه» می‌شمارند.
ششمین مسئلهٔ اسمیل
بیان پرسش ساده است: برای هر انتخابی از جرم‌های مثبت، آیا شمار پیکربندی‌های مرکزی محدود است؟ این ششمین مسئله در فهرست مسائل گشوده‌ای است که ریاضی‌دانی به نام اسمیل (Smale) فراهم کرد.
به گفتهٔ مقاله، وضعیت چنین بود:
- سه جسم: دقیقاً پنج — دو مثلث متساوی‌الاضلاع لاگرانژ و سه آرایش خطی اویلر.
- چهار جسم: محدود بودن را همپتون و موکل برای همهٔ جرم‌های مثبت اثبات کردند.
- پنج جسم در صفحه: آلبوئی و کالوشین در ۲۰۱۲ محدود بودن را اثبات کردند، اما فقط برای جرم‌هایی بیرون از یک مجموعهٔ استثنایی — خانواده‌ای باریک از ترکیب‌های جرم که با معادلات چندجمله‌ای تعریف می‌شود و استدلال آن‌ها در آن‌جا از کار می‌افتاد.
بستن مجموعهٔ استثنایی
تجسوی سینگ تومار این مجموعهٔ استثنایی را از میان برمی‌دارد. قضیهٔ اصلی: برای هر انتخابی از پنج جرم مثبت، مسئلهٔ پنج جسم صفحه‌ای در حد تشابه شمار محدودی پیکربندی مرکزی دارد.
راهبرد از آلبوئی و کالوشین پیروی می‌کند. اگر بی‌نهایت پیکربندی وجود داشت، وقتی معادلات به اعداد مختلط گسترش داده شوند، آن‌ها منحنی پیوسته‌ای از جواب‌ها می‌ساختند. با دنبال کردن این منحنی «تا بی‌نهایت»، فاصله‌های میان اجسام باید به گونه‌ای رفتار کنند که در توازنی دقیق یکدیگر را خنثی کنند. اجسام به یکی از شانزده نمودار حدی که آلبوئی و کالوشین شناسایی کرده‌اند نزدیک می‌شوند و هر کدام شرط‌هایی بر جرم‌ها تحمیل می‌کند.
کار تازه این شرط‌ها را برای هر جرم مثبت دقیق می‌کند و موارد دردسرساز را یکی‌یکی کنار می‌گذارد:
- پیکربندی‌هایی که در آن‌ها چهار جسم خوشه‌ای فشرده می‌سازند و پنجمی به آن نزدیک می‌شود، با بسط انرژی پتانسیل — که در طول منحنی ثابت می‌ماند — تا مرتبه‌های بالاتر و بالاتر کنار گذاشته می‌شوند؛ برای جرم‌های مثبت، شرط‌های حاصل با هم تناقض دارند؛
- نشان داده می‌شود که دو نمودار دیگر هرگز رخ نمی‌دهند؛
- برای همهٔ موارد دیگر، نویسنده همهٔ شرط‌های جرمیِ سازگار را با جبر رایانه‌ای دقیق توصیف می‌کند — ۲٬۲۰۶ دستگاه جبری — و برای هر کدام یک گواهی عددی می‌سازد: فهرستی از اعداد گویا که ویژگی‌هایشان، وقتی با حساب دقیق وارسی شوند، ثابت می‌کند توازن ناممکن است.
دامی که جرم‌های منفی پهن کرده‌اند
گیری هست که جبر محض نمی‌تواند دورش بزند. ریاضی‌دان دیگری به نام رابرتس، برای جرم‌های (۱, ۱, ۱, ۱, −¼) — با یک جرم منفی — بی‌نهایت پیکربندی مرکزی یافته بود. وارونه کردن برخی علامت‌ها این را به بی‌نهایت جواب برای معادلات مختلط‌شده با جرم‌های (۴, ۴, ۴, ۴, ۱) تبدیل می‌کند. این‌ها پیکربندی‌های واقعی نیستند، اما استدلالی که فقط معادلات مختلط را می‌بیند نمی‌تواند آن‌ها را از هم تشخیص دهد.
از این رو در آن جرم‌ها، و در نسبت مرتبط (۱, ۱, ۴, ۴, ۴)، نویسنده پیکربندی‌های واقعی را مستقیماً می‌شمارد، با جست‌وجویی رایانه‌ای که از حساب بازه‌ای تضمین‌شده بهره می‌گیرد:
- برای جرم‌های (۱, ۴, ۴, ۴, ۴): ۳۰۶ پیکربندی در حد چرخش و تغییر مقیاس — ۶۰ تا روی یک خط راست، ۲۴ تا به شکل پنج‌ضلعی محدب، و بقیه با یک یا دو جسم در درون؛
- برای (۱, ۱, ۴, ۴, ۴): ۲۹۴.
آن ۶۰ پیکربندی خطی با شمارش پیشینی از مولتون مطابقت دارند.
وارسی‌شده با ماشین
اثباتی که بر این‌همه محاسبه تکیه دارد به راستی‌آزمایی محکمی نیاز دارد. هر گواهی با برنامهٔ جداگانه‌ای که از روی تعریف‌های مقاله نوشته شده بود دوباره وارسی شد. مهم‌تر از همه، قضیه در دستیار اثبات Lean 4 اثبات شده است، برنامه‌ای که هر گام منطقی را وارسی می‌کند. اثبات صوری حتی نتایج آلبوئی و کالوشین را مفروض نمی‌گیرد: آنچه لازم دارد را دوباره به دست می‌آورد و با جست‌وجو ۱٬۳۷۶ نمودار برچسب‌دار می‌یابد که قواعد آن‌ها را برآورده می‌کنند. دو وارسی‌گر مستقل دیگرِ اثبات‌های Lean هم آن را می‌پذیرند. ساختن آن از صفر حدود ۸۶۰ ساعت-CPU طول می‌کشد.
مقاله با بیانیه‌ای کوتاه پایان می‌یابد: ابزارهای هوش مصنوعی مولد برای یافتن و اثبات نتایج، نوشتن برنامه‌ها و صوری‌سازی Lean، و نوشتن پیش‌نویس متن به کار رفته‌اند. نام ابزارها ذکر نشده است.
آنچه می‌گوید و آنچه نمی‌گوید
نتیجه به پنج جسم در صفحه مربوط است. ثابت می‌کند که شمار پیکربندی‌ها برای هر مجموعه از جرم‌های مثبت محدود است، اما شمار دقیق را فقط در چند نسبت جرمیِ بررسی‌شده به دست می‌دهد.