五つの天体、有限個の完璧なダンス

いくつかの恒星や惑星が、とても精密に配置されていて、群れ全体が形を変えずに剛体のように回転できるところを想像してほしい。そのためには、それぞれの天体にかかる重力がちょうど群れの質量中心を向き、その強さが中心からの距離に比例していなければならない。こうした配置は中心配置と呼ばれる。中心配置は、天体が同じ相対的なパターンを保つn体問題の特別な解の形であり、剛体のように回転する相対平衡もそこに含まれる。

あるパターンが成り立つなら、それを回転させたり、拡大したり、ずらしたりしたものも成り立つ。そのため数学者は、中心配置を「相似を除いて」数える。

スメイルの第6問題

問いを述べるのは簡単だ。正の質量をどう選んでも、中心配置の数は有限なのか。 これは、数学者スメイルがまとめた未解決問題のリストの第6問題である。

論文によれば、これまでの状況は次のとおりだ。

• 三体:ちょうど五つ。ラグランジュの二つの正三角形と、オイラーの三つの直線配置だ。
• 四体:ハンプトンとメッケルが、すべての正の質量について有限性を証明した。
• 平面上の五体:アルブイとカロシンが2012年に有限性を証明したが、それは例外集合の外側の質量に限られていた。例外集合とは、多項式の方程式で定義される質量の組み合わせの薄い族で、そこでは彼らの議論が破綻していた。

例外集合を閉じる

テジャスヴィ・シン・トマール(Tejasvi Singh Tomar)は、その例外集合を取り除いた。主定理は次のとおりだ。五つの正の質量をどう選んでも、平面五体問題の中心配置は相似を除いて有限個である。

戦略はアルブイとカロシンにならっている。もし配置が無限に多くあれば、方程式を複素数に拡張したとき、それらは解の連続した曲線をなすはずだ。その曲線を「無限遠」までたどると、天体間の距離は、精密な釣り合いのなかで打ち消し合うようにふるまわなければならない。天体は、アルブイとカロシンが特定した16の極限図式のどれかに近づき、それぞれの図式が質量に条件を課す。

新しい研究は、すべての正の質量についてこれらの条件を厳密にし、厄介なケースを一つずつ排除していく。

• 四つの天体が密集した塊をつくり、そこに五つ目が近づく配置は、ポテンシャルエネルギー(曲線に沿って一定に保たれる)をどんどん高次まで展開することで排除される。正の質量では、得られる条件が互いに矛盾する。
• さらに二つの図式は、決して現れないことが示される。
• それ以外のすべてについて、著者は厳密な計算機代数(2,206個の代数系)で両立しうる質量条件をすべて記述し、それぞれについて数値的な証明書を作る。証明書とは有理数のリストで、その性質を厳密な算術で確かめると、釣り合いが不可能であることが証明される。

負の質量が仕掛けた罠

純粋な代数では回避できない落とし穴がある。別の数学者ロバーツは、質量(1, 1, 1, 1, −¼)、つまり負の質量を一つ含む場合に、無限に多くの中心配置を見つけていた。いくつかの符号を反転させると、それは質量(4, 4, 4, 4, 1)に対する複素化された方程式の無限に多くの解に変わる。これらは実際の配置ではないが、複素方程式しか見ない議論では区別がつかない。

そこで、その質量と、関連する比(1, 1, 4, 4, 4)については、著者は実際の配置を、保証つきの区間演算を使うコンピューター探索で直接数えた。

• 質量(1, 4, 4, 4, 4)では、回転と拡大縮小を除いて306個。うち60個は一直線上に並び、24個は凸五角形をなし、残りは一つか二つの天体が内側にある。
• (1, 1, 4, 4, 4)では294個。

一直線上の60個は、モールトンによる以前の数え上げと一致する。

機械による検証

これほど多くの計算に支えられた証明には、強力な検証が必要だ。各証明書は、論文の定義から書かれた別のプログラムで再確認された。何よりも、この定理は証明支援系Lean 4で証明されている。Leanは論理のすべてのステップを確認するプログラムだ。形式的な証明は、アルブイとカロシンの結果さえ前提にしていない。必要なものを導き直し、彼らの規則を満たす1,376個のラベルつき図式を探索によって見つけている。この証明は、Leanの証明を検査する独立したほか二つのチェッカーでも受理された。ゼロからビルドするには約860 CPU時間かかる。

論文は短い声明で締めくくられている。結果の発見と証明、プログラムとLeanによる形式化の作成、本文の下書きに、生成AIツールが使われたという。ツールの名前は挙げられていない。

言えること、言えないこと

この結果は平面上の五つの天体に関するものだ。正の質量のどの組についても配置の数が有限であることを証明しているが、正確な数が示されているのは、調べられた少数の質量比についてだけだ。