Smale's sixth problem for five bodies in the plane, with a proof formalized in Lean
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.
Related
- Finiteness of planar central configurations of five bodies for all positive masses: On Smale's sixth problem
- From boundary geometry to counterexamples in Smale's mean value problem
- A complete solution to the reverse isoperimetric problem for λ-convex bodies
- An isoperimetric problem for Fourier zeros of centrally symmetric convex bodies
- Sylvester's four point problem for ball-convex bodies
BibTeX
@misc{tomar2026smales,
title = {{Smale's sixth problem for five bodies in the plane, with a proof formalized in Lean}},
author = {Tejasvi Singh Tomar},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.13100},
eprint = {2610.13100},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.13100},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Smale's sixth problem for five bodies in the plane, with a proof formalized in Lean
AU - Tejasvi Singh Tomar
PY - 2026
DA - 2026/10/15
PB - arXiv
DO - 10.48550/arxiv.2610.13100
UR - https://arxiv.org/abs/2610.13100
AB - 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.
ER -