HEXAGONbeta

A formal proof in Lean of the finiteness of planar five-body central configurations for all positive masses

A mix of human-written and AI-generated textHuman understanding: all partscs.LO — Logic in Computer Sciencemath.DS — Dynamical Systemsmath.AG — Algebraic Geometry

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, there are finitely many central configurations up to similarity. For five bodies in the plane, Albouy and Kaloshin proved finiteness outside a set of masses of codimension two. In a companion paper the author proved finiteness for every choice of five positive masses by their method, adding steps that cannot be checked by hand: exact computer algebra, rational certificates and a branch and bound. We formalize this theorem in Lean 4 with Mathlib without assuming the results of Albouy and Kaloshin that the informal proof uses. Instead we prove what the proof needs of their rules on limit diagrams, of their classification of these diagrams and of their mass conditions. We do so at places of complex algebraic curves, taken as valuations of the function field rather than points of a projective model. Almost every computation becomes data for a checker that we write in Lean, prove sound with respect to Mathlib's real and complex numbers, and run in the kernel (proof by reflection). The main theorem depends on about 680,000680{,}000 theorems proved in this way, and Mathlib's tactics prove the few other computations. The proof uses only Lean's three standard axioms, and two independent Lean kernels, nanoda and lean4lean, accept it.

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

References

  1. A. Albouy and V. Kaloshin, Finiteness of central configurations of five bodies in the plane , Ann. of Math. (2) 176 (2012), 535--588.
  2. H. Barendregt and E. Barendsen, Autarkic computations in formal proofs , J. Automat. Reason. 28 (2002), 321--336.
  3. A. Bastounis, F. Circelli and A. C. Hansen, Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs , arXiv:2610.08144 (2026).arXiv
  4. S. Boutin, Using reflection to build efficient and certified decision procedures , in: Theoretical Aspects of Computer Software (TACS 1997), Lecture Notes in Comput. Sci. 1281 , Springer, 1997, 515--529.
  5. M. Carneiro, Lean4Lean: Verifying a typechecker for Lean, in Lean , arXiv:2403.14064v3 (2025).arXiv
  6. 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
  7. 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 (2025).link
  8. L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language , in: Automated Deduction (CADE 28), Lecture Notes in Comput. Sci. 12699 , Springer, 2021, 625--635.
  9. G. Gonthier, Formal proof---the four-color theorem , Notices Amer. Math. Soc. 55 (2008), 1382--1393.
  10. T. Hales, M. Adams, G. Bauer, T. D. Dang, J. Harrison, L. T. Hoang, C. Kaliszyk, V. Magron, S. McLaughlin, T. T. Nguyen, Q. T. Nguyen, T. Nipkow, S. Obua, J. Pleso, J. Rute, A. Solovyev, T. H. A. Ta, N. T. Tran, T. D. Trieu, J. Urban, K. Vu and R. Zumkeller, A formal proof of the Kepler conjecture , Forum Math. Pi 5 (2017), e2.
Show all 27 referencesShow fewer references
  1. M. Hampton and R. Moeckel, Finiteness of relative equilibria of the four-body problem , Invent. Math. 163 (2006), 289--312.
  2. M. J. H. Heule, O. Kullmann and V. W. Marek, Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer , in: Theory and Applications of Satisfiability Testing (SAT 2016), Lecture Notes in Comput. Sci. 9710 , Springer, 2016, 228--245.
  3. F. Immler, A verified ODE solver and the Lorenz attractor , J. Automat. Reason. 61 (2018), 73--111.
  4. R. Krawczyk, Newton-Algorithmen zur Bestimmung von Nullstellen mit Fehlerschranken , Computing 4 (1969), 187--201.
  5. lean4export, an exporter of Lean 4 environments, version 3.1.0, https://github.com/leanprover/lean4export.link
  6. É. Martin-Dorel and G. Melquiond, Proving tight bounds on univariate expressions with elementary functions in Coq , J. Automat. Reason. 57 (2016), 187--217.
  7. The mathlib Community, The Lean mathematical library , in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020, 367--381.
  8. G. Melquiond, Proving bounds on real-valued functions with computations , in: Automated Reasoning (IJCAR 2008), Lecture Notes in Comput. Sci. 5195 , Springer, 2008, 2--17.
  9. R. E. Moore, A test for existence of solutions to nonlinear systems , SIAM J. Numer. Anal. 14 (1977), 611--615.
  10. nanoda, a type checker for Lean 4, version 0.4.17, https://github.com/ammkrn/nanoda_lib.link
  11. S. Smale, Mathematical problems for the next century , Math. Intelligencer 20 (1998), no. 2, 7--15.
  12. A. Solovyev and T. C. Hales, Formal verification of nonlinear inequalities with Taylor interval approximations , in: NASA Formal Methods (NFM 2013), Lecture Notes in Comput. Sci. 7871 , Springer, 2013, 383--397.
  13. B. Subercaseaux, W. Nawrocki, J. Gallicchio, C. Codel, M. Carneiro and M. J. H. Heule, Formal verification of the empty hexagon number , in: 15th International Conference on Interactive Theorem Proving (ITP 2024), LIPIcs 309 , 2024, 35:1--35:19.
  14. T. S. Tomar, Smale's sixth problem for five bodies in the plane, with a proof formalized in Lean , version 2, Zenodo (2026), https://doi.org/10.5281/zenodo.23406010; version 1: arXiv:2610.13100 (2026), titled Finiteness of planar central configurations of five bodies for all positive masses .arXivDOI
  15. T. S. Tomar, Supplementary material for ``Smale's sixth problem for five bodies in the plane, with a proof formalized in Lean'' , Zenodo (2026), https://doi.org/10.5281/zenodo.23202861.DOI
  16. T. S. Tomar, Uniqueness of four-body convex central configurations for all masses , arXiv:2609.35632 (2026).arXiv
  17. W. Tucker, A rigorous ODE solver and Smale's 14th problem , Found. Comput. Math. 2 (2002), 53--117.

Version history

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