Finiteness of planar central configurations of five bodies for all positive masses
Tejasvi Singh Tomar
math.DS
Oct 9, 2026 · v1
math-ph math.AG
TL;DR
The main finiteness theorem is formally proved in Lean 4 with Mathlib, with the proof also checked by the independent kernels nanoda and lean4lean.
Abstract
We prove that for every choice of five positive masses the planar five-body problem has finitely many central configurations up to similarity. This settles Smale's sixth problem for five bodies in the plane. Albouy and Kaloshin proved it for masses outside a closed algebraic subset of codimension two. We follow their method. Infinitely many central configurations would give an algebraic curve of complex solutions. At the places at infinity of the curve the valuations of the mutual distances must balance. We determine the possible valuation vectors at all positive masses, together with the mass conditions under which each can occur. We treat limits in which four bodies form a cluster of zero potential energy by expanding the potential, which is constant along the curve, at a place. This excludes, at every positive mass, one of the two diagrams in which such clusters occur, and part of the other. The same expansion excludes one further diagram at every positive mass. What remains is an exact analysis, by computer algebra, of the sets of mass conditions that can hold together at positive masses. Exact rational certificates show that the balance fails under each of them, except on a few one-parameter families of masses, which we treat separately. On the rays through $(1,4,4,4,4)$ and $(1,1,4,4,4)$ the certificates do not apply. On the first ray they cannot apply: there the complex equations have a continuum of solutions, as Albouy and Kaloshin observed. On these rays we count the real central configurations: there are 306 and 294 up to orientation-preserving similarity. The certificates, the programs that check them and a proof of the theorem in the Lean proof assistant are available.
Problem
Smale's sixth problem asks whether, for every choice of positive masses, there are finitely many central configurations up to similarity. Albouy and Kaloshin proved finiteness for the planar five-body problem except on a closed algebraic exceptional set of codimension two, which remained open.
Approach
Following Albouy–Kaloshin, infinitely many central configurations would yield an algebraic curve of complex solutions whose valuation vectors at places at infinity must balance. The authors classify the possible valuation vectors and their mass conditions, and exclude zero-energy four-body cluster diagrams by expanding the potential at a place. Exact computer algebra with rational and modular certificates, using a lexicographic separation lemma, rules out the remaining cases. The full theorem is formalized in Lean 4 with Mathlib.
Results
Finiteness holds for every positive mass vector, which settles Smale's sixth problem for five bodies in the plane. On the special rays through (1,4,4,4,4) and (1,1,4,4,4), the authors count 306 and 294 real central configurations up to orientation-preserving similarity.