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

A mix of human-written and AI-generated textHuman understanding: all partsmath.DS — Dynamical Systems

Contributed by Tejasvi Singh Tomar ↗

Version 1 / Oct 26, 2026/ arXiv: 2610.13100 / CC BY 4.0

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)(1,4,4,4,4) and (1,1,4,4,4)(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.

References

  1. A. Albouy, H. E. Cabral and A. A. Santos, Some problems on the classical NN-body problem , Celest. Mech. Dyn. Astron. 113 (2012), 369--375.
  2. A. Albouy and V. Kaloshin, Finiteness of central configurations of five bodies in the plane , Ann. of Math. (2) 176 (2012), 535--588.
  3. Z. Chen and Z. Tong, Finiteness of planar central configurations of five bodies for all positive masses: On Smale's sixth problem , arXiv:2610.16107v1 (2026).arXiv
  4. M. Hampton and R. Moeckel, Finiteness of relative equilibria of the four-body problem , Invent. Math. 163 (2006), 289--312.
  5. A. Jensen and A. Leykin, Smale's 6th problem for generic masses , J. Exp. Math. 1 (2025), 306--314.
  6. R. Krawczyk, Newton-Algorithmen zur Bestimmung von Nullstellen mit Fehlerschranken , Computing 4 (1969), 187--201.
  7. R. Moeckel, Lectures on central configurations , lecture notes, 2014.
  8. R. E. Moore, A test for existence of solutions to nonlinear systems , SIAM J. Numer. Anal. 14 (1977), 611--615.
  9. F. R. Moulton, The straight line solutions of the problem of nn bodies , Ann. of Math. (2) 12 (1910), 1--17.
  10. M. Moczurad and P. Zgliczyński, Central configurations in planar nn-body problem for n=5,6,7n=5,6,7 with equal masses , Celest. Mech. Dyn. Astron. 131 (2019), 46.
Show all 16 referencesShow fewer references
  1. M. Moczurad and P. Zgliczyński, Central configurations on the plane with NN heavy and kk light bodies , Commun. Nonlinear Sci. Numer. Simul. 114 (2022), 106533.
  2. M. Moczurad and P. Zgliczyński, Central configurations with unequal masses: finiteness in several exceptional cases of five bodies , arXiv:2601.01165 (2026).arXiv
  3. A. Neumaier, Interval Methods for Systems of Equations , Cambridge University Press, 1990.
  4. G. E. Roberts, A continuum of relative equilibria in the five-body problem , Physica D 127 (1999), 141--145.
  5. S. Smale, Mathematical problems for the next century , Math. Intelligencer 20 (1998), no. 2, 7--15.
  6. T. S. Tomar, Complex solution sets of the planar five-body problem at special masses , preprint (2026), https://doi.org/10.5281/zenodo.23444949.DOI

Version history

  1. v1Submitted by Tejasvi Singh TomarInitial depositCurrentOct 26, 2026