五个天体，有限多种完美之舞

想象几颗恒星或行星排列得如此精确，整个系统可以像刚体一样旋转而不改变形状。要做到这一点，作用在每个天体上的引力必须恰好指向系统的质心，且大小与它到质心的距离成正比。这样的排布称为中心构型（central configuration）。它们是n体问题中一类特殊解的形状——在这类解中，各天体保持相同的相对图案，其中包括刚性旋转的相对平衡解。

如果某个图案成立，那么它旋转、放大或平移后的任何副本也都成立，因此数学家是“在相似意义下”计数的。

斯梅尔第六问题

这个问题表述起来很简单：对于任意一组正质量，中心构型的数目是否有限？ 它是数学家斯梅尔（Smale）列出的一份公开问题清单中的第六个问题。

据论文介绍，此前的进展如下：

• 三体：恰好五个——拉格朗日的两个等边三角形和欧拉的三条直线。
• 四体：汉普顿（Hampton）和默克尔（Moeckel）对所有正质量证明了有限性。
• 平面五体：阿尔布伊（Albouy）和卡洛申（Kaloshin）在2012年证明了有限性，但只针对例外集之外的质量——例外集是由多项式方程定义的一个很“薄”的质量组合族，在那里他们的论证失效。

消除例外集

特贾斯维·辛格·托马尔（Tejasvi Singh Tomar）消除了这个例外集。主要定理是：对于每一种五个正质量的选择，平面五体问题在相似意义下只有有限多个中心构型。

其策略沿用了阿尔布伊和卡洛申的思路。如果构型有无穷多个，那么把方程推广到复数后，它们会构成一条连续的解曲线。沿着这条曲线“走向无穷远”，天体之间的距离必须以某种方式变化，使各项在精确的平衡中相互抵消。天体会趋近阿尔布伊和卡洛申确定的十六种极限图之一，每一种都对质量施加条件。

新工作对每一种正质量都把这些条件刻画得十分精确，并逐一排除了棘手的情形：

• 对于四个天体形成紧密团簇、第五个天体向其靠近的构型，通过把势能（它沿曲线保持不变）展开到越来越高的阶来排除；对于正质量，所得的条件相互矛盾；
• 另外两种极限图被证明永远不会出现；
• 对于其余所有情形，作者用精确的计算机代数描述了全部相容的质量条件——共2,206个代数方程组——并为每一个给出一份数值证书：一串有理数，用精确算术核验其性质，即可证明那种平衡不可能成立。

负质量设下的陷阱

有一个障碍是纯代数绕不过去的。另一位数学家罗伯茨（Roberts）曾发现，对于质量(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个直线构型与莫尔顿（Moulton）早先的计数一致。

由机器核验

一个依赖如此多计算的证明需要强有力的核验。每一份证书都由一个根据论文定义独立编写的程序重新检查。最重要的是，该定理在Lean 4证明助手中得到了证明——这是一个检查每一步逻辑推理的程序。形式化证明甚至不预设阿尔布伊和卡洛申的结果：它自行重新推导所需内容，通过搜索找到了满足其规则的1,376个带标记的极限图。另外两个独立的Lean证明检查器也接受了它。从零开始构建它大约需要860个CPU小时。

论文末尾有一段简短声明：生成式AI工具被用于发现和证明结果、编写程序和Lean形式化，以及起草文本。这些工具的名称没有给出。

它说明了什么，没有说明什么

这一结果针对的是平面上的五个天体。它证明了对于每一组正质量，构型数目都是有限的，但只在所研究的少数几个质量比下给出了精确数目。