HEXAGONbeta

Smale's sixth problem for six bodies in the plane: finiteness of central configurations for generic masses, with a proof formalized in Lean

A mix of human-written and AI-generated textHuman understanding: all partsmath.DS — Dynamical Systemsmath.AG — Algebraic Geometrymath.NA — Numerical Analysiscs.LO — Logic in Computer Science

Contributed by Tejasvi Singh Tomar ↗

Version 1 / Nov 12, 2026 / CC BY 4.0

Abstract

Smale's sixth problem asks whether, for every choice of positive masses, the number of central configurations up to similarity is finite. We prove that it is finite for six bodies in the plane and all positive masses outside a proper algebraic subset of the mass space. This subset, which we describe only in part, contains every mass vector with three equal masses or with one mass equal to the sum of two others. Finiteness for all positive masses remains open. Infinitely many central configurations would give a curve of complex solutions; following Albouy and Kaloshin, we exclude such a curve using the valuations of the mutual distances at its points at infinity. The proof is computer-assisted and uses linear programs, Gröbner bases and interval arithmetic. The theorem is proved in the Lean proof assistant, whose kernel checks the computations as well.

Author comments: Published on Zenodo: https://doi.org/10.5281/zenodo.23720035

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. K. Aquino-Michaels, Reducing the Chang--Chen residual: certified eliminations in the planar six-body central-configuration problem , preprint (2026), https://github.com/no-way-labs/smale6-residual, commit 07f6c99 .link
  4. J. Berthomieu, C. Eder and M. Safey El Din, msolve: a library for solving polynomial systems , in: Proceedings of ISSAC 2021, ACM, 2021, 51--58.
  5. K.-M. Chang and K.-C. Chen, Toward finiteness of central configurations for the planar six-body problem by symbolic computations , arXiv:2303.02853 (2023).arXiv
  6. K.-M. Chang and K.-C. Chen, Toward finiteness of central configurations for the planar six-body problem by symbolic computations. (I) Determine diagrams and orders , J. Symbolic Comput. 123 (2024), 102277.
  7. K.-M. Chang and K.-C. Chen, Toward finiteness of central configurations for the planar six-body problem by symbolic computations. (II) Determine mass relations , SIAM J. Appl. Dyn. Syst. 24 (2025), 2369--2404.
  8. Z. Chen and Z. Tong, Finiteness of planar central configurations of five bodies for all positive masses: On Smale's sixth problem , arXiv:2610.16107 (2026).arXiv
  9. W. Decker, G.-M. Greuel, G. Pfister and H. Schönemann, Singular 4.4.1 --- A computer algebra system for polynomial computations , https://www.singular.uni-kl.de.link
  10. The FLINT team, FLINT: Fast Library for Number Theory , version 3.6.0, https://flintlib.org.link
Show all 27 referencesShow fewer references
  1. D. R. Grayson and M. E. Stillman, Macaulay2, a software system for research in algebraic geometry , version 1.25.11, https://macaulay2.com.link
  2. A. Grothendieck, Éléments de géométrie algébrique II , Publ. Math. IHÉS 8 (1961).
  3. M. Hampton and R. Moeckel, Finiteness of relative equilibria of the four-body problem , Invent. Math. 163 (2006), 289--312.
  4. Q. Huangfu and J. A. J. Hall, Parallelizing the dual revised simplex method , Math. Program. Comput. 10 (2018), 119--142.
  5. A. N. Jensen, Gfan, a software system for Gröbner fans and tropical varieties , version 0.7.
  6. A. Jensen and A. Leykin, Smale's 6th problem for generic masses , J. Exp. Math. 1 (2025), 306--314.
  7. F. Johansson, Arb: efficient arbitrary-precision midpoint-radius interval arithmetic , IEEE Trans. Comput. 66 (2017), 1281--1292.
  8. U. Junker, QuickXplain: preferred explanations and relaxations for over-constrained problems , in: Proceedings of AAAI 2004, AAAI Press, 2004, 167--172.
  9. R. Krawczyk, Newton-Algorithmen zur Bestimmung von Nullstellen mit Fehlerschranken , Computing 4 (1969), 187--201.
  10. A. Meurer et al., SymPy: symbolic computing in Python , PeerJ Comput. Sci. 3 (2017), e103.
  11. 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.
  12. M. Moczurad and P. Zgliczyński, Central configurations with unequal masses: finiteness in several exceptional cases of five bodies , arXiv:2601.01165 (2026).arXiv
  13. R. Moeckel, Lectures on central configurations , lecture notes, 2014.
  14. F. R. Moulton, The straight line solutions of the problem of nn bodies , Ann. of Math. (2) 12 (1910), 1--17.
  15. G. E. Roberts, A continuum of relative equilibria in the five-body problem , Physica D 127 (1999), 141--145.
  16. S. Smale, Mathematical problems for the next century , Math. Intelligencer 20 (1998), no. 2, 7--15.
  17. T. S. Tomar, Smale's sixth problem for five bodies in the plane, with a proof formalized in Lean , arXiv:2610.13100 (2026); version 1 is titled Finiteness of planar central configurations of five bodies for all positive masses . Numbering as in version 2, https://doi.org/10.5281/zenodo.23406010.arXivDOI

Version history

  1. v1 · 48 pagesSubmitted by Tejasvi Singh TomarPublished on Zenodo: https://doi.org/10.5281/zenodo.23720035CurrentNov 12, 2026