Smale's sixth problem for five bodies in the plane, with a proof formalized in Lean

Introduction

A configuration $q=(q_1,\ldots,q_n)$ of $n$ distinct points in the plane, carrying positive masses $m_1,\ldots,m_n$, is a central configuration if there are $\lambda\in\mathbb{R}$ and $c\in\mathbb{R}^2$ such that

The right side is minus the Newtonian force on the body $i$: the force on each body points towards the centre of mass $c$ and is proportional to its distance from it. Central configurations are the shapes of the homographic solutions of the $n$-body problem, and in particular the shapes of its relative equilibria. If $q$ is a central configuration, so is any configuration similar to it. Smale’s sixth problem [15] (Problem 9 of [1]) asks whether, for every choice of positive masses, the number of central configurations up to similarity is finite.

For $n=3$ there are five, the two equilateral triangles of Lagrange and the three collinear configurations of Euler. Moulton [9] counted the collinear ones for all $n$. Hampton and Moeckel [4] proved finiteness for four bodies and all positive masses. Albouy and Kaloshin [2] proved finiteness for five bodies in the plane when the masses lie outside a closed algebraic subset $\mathcal{A}\subset(\mathbb{R}_{>0})^5$ of codimension two. Their argument produces singular sequences that approach one of the first eight limit diagrams in their list of sixteen. Each of these eight forces a polynomial

2020 Mathematics Subject Classification. 70F10, 70F15, 14Q20, 65G40.

Key words and phrases. Central configurations, relative equilibria, five-body problem, Smale’s sixth problem, singular sequences, Puiseux series, computer-assisted proof. condition on the masses. The set $\mathcal{A}$ is where two independent conditions hold at once. Jensen and Leykin [5] gave a tropical proof of finiteness for generic masses. Moczurad and Zgliczyński [12] counted the central configurations exactly, with a computer-assisted proof, at several mass vectors of the exceptional set. We remove the exceptional set.

We use the results of [2] listed in §2.6, in particular their classification of the limit diagrams (their Fig. 11) and the mass conditions of their §8.

Part of the exceptional set of [2] cannot be avoided by an argument about the complexified equations alone. Roberts [14] found a continuum of central configurations for the masses $(1,1,1,1,-\frac{1}{4})$. Albouy and Kaloshin observe that changing the signs of $m_5$ and of the four distances $r_{k5}$ turns it into a continuum of solutions, with masses $(4,4,4,4,1)$, of the polynomial system they work with [2 pp. 543–544]. These solutions are not central configurations, because the distances $r_{k5}$ are negative square roots, but an argument that sees only the complexified system cannot tell them apart. At $(1,4,4,4,4)$ the complex solution set is therefore infinite. Finiteness of the real central configurations there must use the signs of the distances. On the rays through $(1,4,4,4,4)$ and $(1,1,4,4,4)$ and their images under permutations of the bodies we count the real central configurations directly: for every positive multiple of a permutation of $(1,4,4,4,4)$ there are exactly 306 such configurations up to orientation-preserving similarity, and for $(1,1,4,4,4)$ exactly 294 (Theorems 10.1 and 10.2). We call these rays the special rays: a mass vector lies on a special ray if and only if it is a positive multiple of a permutation of $(1,4,4,4,4)$ or of $(1,1,4,4,4)$.

The method

The method. Our argument has six parts.

Curves and balancing. If there are infinitely many central configurations, the complex solution set contains an irreducible curve on which the potential $U$ is a nonzero constant and some mutual distance is not constant. At each place at infinity of this curve the inverse distances $p_{kl}=r_{kl}^{-1}$ have valuations. The vectors $\rho(P)=(-\operatorname{val}_P p_{kl})_{k<l}$ sum to zero over the places (§ 1.5). This is the starting point of [2].

Types and mass conditions. At a singular place, Albouy and Kaloshin show that the configuration approaches one of sixteen diagrams and that most diagrams force polynomial conditions on the masses. We make this sharp at all positive masses. For each diagram and labelling of the bodies we give the set of vectors $\rho(P)$ that can occur, as an explicit polyhedral set (a piece) that is present only when certain mass conditions hold (Theorem 3.12). Besides results of [2], Theorem 3.12 contains our sharper type statements for several diagrams and a lemma on diagram 7 (§ 2.5) that is not in [2].

Lexicographic separation. If the pieces present at $m$ admit a staged family of linear functionals that are nonnegative on all of them and positive on each in turn, the vectors $\rho(P)$ cannot sum to zero and $m$ has no such curve (§ 3). On the sixteen strata of the sorted, scaled masses we analyse by exact computer algebra the sets of mass conditions that can hold together (§ 8). We certify such a family for each of these sets, with rational functionals checked in exact arithmetic, except for the sets at two mass points, where we use a smaller hull of diagram 5, and on a few one-parameter families of masses, which we treat separately (§§§ 6, § 9 and § 10.4).

Clusters of zero energy. Using all the singular places of a curve, rather than two well-chosen singular sequences, brings in diagrams 14 and 15 of [2]. In them four bodies form a cluster, approached by the fifth body. The leading part of the cluster is a complex configuration of zero potential energy: a solution of the systems that we call K14 and K15. These systems have solutions on hypersurfaces of the space of masses. The two diagrams impose no condition on the masses in [2]. Since their pieces are present for every set of mass conditions (§§§ 2.7 and § 3.2), we need an argument that does not go through the mass conditions. To exclude diagram 15 we use that the potential is constant along the curve and that its gradient vanishes there. At a place, the expansion of the potential in a uniformizing parameter is then constant, while the Euler identity of the weights relates its coefficients to those of the equations. At order three this forces the three outer bodies of the cluster into one of four explicit shapes. At order five, if the leading cluster configuration is nondegenerate, it forces a cubic moment of the shape to vanish. For positive masses the two conditions are incompatible: the vanishing of the weighted sums of $x_i$, $x_i^{-2}$ and $x_i^3$ would force three angles, their doubles and their triples each to surround 0. Three angles cannot do this. With an analysis of the degenerate leading configurations this excludes diagram 15 at every positive mass (§§§ 4.2–5.4). Diagram 14 gives two kinds of pieces, called d14a and d14b in Table 3. At a place of type d14b the leading cluster solves K14. Its outer bodies form one of the same four shapes. At positive masses such clusters exist only when the three outer masses are equal and in one ratio to the fourth, where the outer bodies form an equilateral triangle centred at the fourth. An expansion at the place excludes this case too. Thus the pieces d14b are excluded at every positive mass (§ 4.6). We exclude the remaining piece of diagram 14, d14a, where it is needed, by showing that K14 has no solution: at finitely many mass points (§ 6) and along the curve families off finitely many special points (§ 9). At the special points we exclude it by a local analysis at the place (§ 9).

piece	vertices	attained	enabled by
d1[$T$]	$a_1(T)$, $b_1(T)$	open segment	$E(T)$
d4[$T$]	$b_1(T)$	point	$E(T)$
d2[$T$]	$a_1(T)$	point	always
d3($s;D_1\mid D_2$)	$h(s;D_1\mid D_2)$	point	$H(D_1\mid D_2)$, read as $\mathcal{D}_3(s;D_1\mid D_2)$
d6($A\mid B$)	$v_7(0,0)$	point	D6($ab\mid cd$)
d7($A\mid B$)	cells of Table 2	see Table 2	$E(A)$, $E(B)$, RA, RB
d8($A\mid B$)	$v_7(0,0)$, $v_7(1,0)$	open segment	RA
d9($T;ax,by$)	$n(T;ax,by)$	point	always
d10($A\mid B$)	$u_A(0)$, $u_A(\frac{1}{3})$	$(u_A(0),u_A(\frac{1}{3}))$	$E(A)$
d11($A\mid B$)	$u_A(0)$	point	$E(A)\lor$ RA
d12($A\mid B$)	$u_A(0)$	point	RA
d14a($j$)	$u_0(j)$	point	always
d14b($j,k$)	$b_k(j)$, $u_0(j)$	open segment	always
d15($j,k$)	$b_k(j)$	point	always

Diagrams 9 and 2. Diagram 9, whose mass condition is the polynomial $N$ of [2], does not occur at any positive mass (§ 5.1); we prove this with an expansion of the potential at the place as for diagrams 14 and 15. Diagram 2 does not occur at any positive mass either (§ 7): a condition at the leading order of a place and closed forms of its first obstructions leave twelve mass vectors of the triangle, at which the torque cannot vanish.

The special rays. On the rays through $(1, 4, 4, 4, 4)$ and $(1, 1, 4, 4, 4)$ the separation fails. At the first of them it must fail, since the modified Roberts continuum lies in the complex solution set there. Following Moczurad and Zgliczyński [10, 12], we count the real central configurations on these rays by a branch-and-bound search with interval arithmetic and Krawczyk’s test (§ 10).

Computations and their verification

We describe the sets of mass conditions at all positive masses by 2206 ideals on the sixteen strata, computed with exact standard bases and minimal primes over $\mathbb{Q}$ (§ 8). The mass points of the special rays that need a separate argument are exact algebraic points. At one of them, $P_1$, defined in § 10.4, we count the central configurations, as on the special rays. At the other points, except the special points of the curve families (§ 9), we show, where it is needed, that the relevant systems K14 have no solution, by Gröbner bases modulo a large prime together with a lifting argument. The counts rest on a branch and bound in outward-rounded floating point. § 12 describes how the computations are checked and the proof of Theorem 1.1 in Lean.

Organization

In § 1.5 we set up the system of [2], the slice, the potential form of the equations and the balancing condition. In § 2 we determine the types of singular places and the mass conditions and state Theorem 3.12. In § 3 we give the separation lemma and the certificates. In § 4 we give the energy argument, in § 6 the certificates for the four-body systems at finitely many masses, and in § 7 the proof that diagram 2 does not occur. In § 8 we analyse by exact computer algebra the sets of mass conditions that can hold together at positive masses, and in § 9 we treat the curve families. In § 10 we count the central configurations on the special rays and at $P_1$, in § 11 we prove Theorem 1.1, and in § 12 we describe the verification. The appendices derive the types of the sixteen diagrams and the hulls of diagram 5. They contain the proof of the sharpened condition for diagram 3, the label polynomials, the analysis of places of diagram 2 used in §7, the polynomial of degree eleven and the tests for diagrams 6 and 3 at two exceptional mass points.

Note added

Version 1 of this paper was submitted to arXiv on 9 October 2026, and its supplementary material, including the complete Lean formalization (§12.4), was published on Zenodo the same day (https://doi.org/10.5281/zenodo.23202861). On 12 October 2026, Z. Chen and Z. Tong submitted arXiv:2610.16107 [3], which states Theorem 1.1 and gives a different proof. Theorem 1.2 of version 1 of [3] begins “Assume the computational statements listed in Appendix A”, and that version names the programs for these statements but does not include them.

Version 3 (October 2026) adds Remark 5.43 on [2 Prop. 8], the description of version 1 of [3] above, and comparisons with that version in Remark 5.44 and after Proposition G.1. It also gives the DOI of [16] and the numbers of the results cited from it. Remark 5.44 was Remark 5.43 in version 2. The theorems and their proofs are unchanged.

Normalized central configurations and curves of them

The system of Albouy and Kaloshin

Let $m=(m_1,\ldots,m_5)$. Following [2 p. 540], a normalized central configuration is a solution $(x,y,\delta)\in\mathbb{C}^5\times\mathbb{C}^5\times\mathbb{C}^{10}$ of

for $k\ne l$ in $\{1,\ldots,5\}$, with $\delta_{kl}=\delta_{lk}$. It is real if $x,y\in\mathbb{R}^5$, and positive if moreover all $\delta_{kl}$ are positive. Summing the first equation multiplied by $m_k$ shows that solutions have their centre of mass at the origin. The multiplier $\lambda$ of (1) is normalized to 1.

Proof. Taking the scalar product of (1) with $m_i(q_i-c)$ and summing gives $\lambda I=U$ with $I=\sum_i m_i\lvert q_i-c\rvert^2>0$ and $U=\sum_{i<j}m_im_j/r_{ij}>0$. So $\lambda>0$. We translate $c$ to the origin, scale by $\lambda^{1/3}$, and rotate so that $q_1-q_2$ is horizontal. Exactly two rotations do this. Conversely, the translation and the scale of a positive normalized central configuration are fixed by (2). □