LIMA BENDA, SEJUMLAH TERHINGGA TARIAN SEMPURNA

Bayangkan beberapa bintang atau planet yang disusun begitu tepat sehingga seluruh kelompok bisa berputar seperti benda kaku, tanpa berubah bentuk. Agar itu terjadi, tarikan gravitasi pada setiap benda harus mengarah tepat ke pusat massa kelompok, dengan kekuatan yang sebanding dengan jaraknya dari pusat itu. Susunan semacam ini disebut konfigurasi sentral. Konfigurasi ini adalah bentuk dari solusi-solusi khusus masalah n-benda yang membuat benda-benda tetap mempertahankan pola relatif yang sama, termasuk kesetimbangan relatif yang berputar secara kaku.

Jika sebuah pola berhasil, salinannya yang diputar, diperbesar, atau digeser juga berhasil, sehingga matematikawan menghitungnya “sampai dengan keserupaan”.

Soal keenam Smale

Pertanyaannya mudah dirumuskan: untuk pilihan massa positif apa pun, apakah jumlah konfigurasi sentral terhingga? Ini adalah soal keenam dalam daftar soal terbuka yang disusun oleh matematikawan Smale.

Inilah keadaannya, menurut makalah tersebut:

Tiga benda: tepat lima — dua segitiga sama sisi Lagrange dan tiga garis lurus Euler.
Empat benda: keterhinggaannya dibuktikan oleh Hampton dan Moeckel, untuk semua massa positif.
Lima benda di sebuah bidang: Albouy dan Kaloshin membuktikan keterhinggaannya pada 2012, tetapi hanya untuk massa di luar suatu himpunan pengecualian — keluarga tipis kombinasi massa yang didefinisikan oleh persamaan polinomial, tempat argumen mereka gagal.

Menutup himpunan pengecualian

Tejasvi Singh Tomar menghapus himpunan pengecualian itu. Teorema utamanya: untuk setiap pilihan lima massa positif, masalah lima benda pada bidang memiliki sejumlah terhingga konfigurasi sentral sampai dengan keserupaan.

Strateginya mengikuti Albouy dan Kaloshin. Jika ada tak terhingga banyaknya konfigurasi, konfigurasi-konfigurasi itu akan membentuk kurva solusi yang kontinu ketika persamaannya diperluas ke bilangan kompleks. Dengan menelusuri kurva itu “hingga tak terhingga”, jarak antarbenda harus berperilaku dengan cara-cara yang saling meniadakan dalam suatu keseimbangan yang presisi. Benda-benda itu mendekati salah satu dari enam belas diagram limit yang diidentifikasi Albouy dan Kaloshin, masing-masing memberi syarat pada massa.

Karya baru ini mempertajam syarat-syarat tersebut untuk setiap massa positif, dan menyingkirkan kasus-kasus yang merepotkan satu per satu:

konfigurasi tempat empat benda membentuk gugus rapat yang didekati benda kelima disingkirkan dengan menjabarkan energi potensial — yang tetap konstan di sepanjang kurva — ke orde yang makin tinggi; untuk massa positif, syarat-syarat yang dihasilkan saling bertentangan;
dua diagram lain ditunjukkan tidak pernah terjadi;
untuk sisanya, penulis menguraikan semua syarat massa yang sesuai dengan aljabar komputer eksak — 2.206 sistem aljabar — dan, untuk masing-masing, menghasilkan sertifikat numerik: daftar bilangan rasional yang sifat-sifatnya, setelah diperiksa dengan aritmetika eksak, membuktikan bahwa keseimbangan itu mustahil.

Jebakan dari massa negatif

Ada satu hambatan yang tak bisa diatasi oleh aljabar murni. Matematikawan lain, Roberts, pernah menemukan tak terhingga banyaknya konfigurasi sentral untuk massa (1, 1, 1, 1, −¼) — dengan satu massa negatif. Membalik beberapa tanda mengubahnya menjadi tak terhingga banyaknya solusi persamaan yang dikompleksifikasi untuk massa (4, 4, 4, 4, 1). Itu bukan konfigurasi nyata, tetapi argumen yang hanya melihat persamaan kompleks tidak bisa membedakannya.

Maka, pada massa-massa itu, dan pada rasio terkait (1, 1, 4, 4, 4), penulis menghitung konfigurasi nyata secara langsung, dengan pencarian komputer yang memakai aritmetika interval terjamin:

untuk massa (1, 4, 4, 4, 4): 306 konfigurasi sampai dengan rotasi dan penskalaan — 60 dalam satu garis lurus, 24 membentuk segi lima cembung, sisanya dengan satu atau dua benda di dalam;
untuk (1, 1, 4, 4, 4): 294.

Ke-60 konfigurasi garis lurus itu cocok dengan hitungan Moulton sebelumnya.

Diperiksa oleh mesin

Bukti yang bertumpu pada begitu banyak perhitungan membutuhkan verifikasi yang kuat. Setiap sertifikat diperiksa ulang oleh program terpisah yang ditulis berdasarkan definisi dalam makalah. Terutama, teorema ini dibuktikan dalam asisten pembuktian Lean 4, sebuah program yang memeriksa setiap langkah logis. Bukti formalnya bahkan tidak mengandaikan hasil Albouy dan Kaloshin: bukti itu menurunkan ulang apa yang dibutuhkannya, dengan menemukan lewat pencarian 1.376 diagram berlabel yang memenuhi aturan mereka. Bukti ini juga diterima oleh dua pemeriksa bukti Lean independen lainnya. Membangunnya dari nol memakan sekitar 860 jam-CPU.

Makalah ini diakhiri dengan pernyataan singkat: perangkat AI generatif digunakan untuk menemukan dan membuktikan hasil-hasilnya, menulis program dan formalisasi Lean, serta menyusun draf teks. Perangkat tersebut tidak disebutkan namanya.

Apa yang dikatakan dan tidak dikatakan

Hasil ini menyangkut lima benda di sebuah bidang. Hasil ini membuktikan bahwa jumlah konfigurasinya terhingga untuk setiap himpunan massa positif, tetapi hanya memberi hitungan tepat pada sedikit rasio massa yang dikaji.