HEXAGONbeta

Formal Verification of a Computer-Assisted Proof in Celestial Mechanics

A mix of human-written and AI-generated textHuman understanding: all partscs.LO — Logic in Computer Sciencemath.DS — Dynamical Systemscs.MS — Mathematical Software

Contributed by Tejasvi Singh Tomar ↗

Version 1 / Nov 12, 2026 / CC BY 4.0

Abstract

Albouy, Fu and Sun conjectured in 2008 that four positive masses admit, for each cyclic order of the bodies, exactly one convex central configuration up to similarity; the question is Problem 10 of a 2012 list of open problems on the nn-body problem. We recently proved the conjecture by reducing it to an inequality for a trace at the real zeros of an equation in four variables; a branch and bound that starts from a grid of 136,448 boxes establishes the inequality. In this paper we describe a formalization of the whole proof in Lean 4 and Mathlib in which Lean's kernel checks the computation, using decide +kernel, so that no compiler has to be trusted. Our checker stores an interval as two natural numbers in a biased fixed-point format. The kernel can then hand all the arithmetic to GMP. Functions are enclosed over boxes by first-order slopes. An unverified search records the decisions for each box in one natural number, and the checker replays them. We write each formula once over a type class; evaluating it at a type that pairs a real number with an interval then proves the enclosure correct. Checking the 3418 certificate theorems takes 7.6 hours of processor time, and the independent type checker nanoda accepts the proof. A version rebuilt on one eighth of the boxes passed three type checkers in 2.9 hours on a public registry of formal proofs.

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

References

  1. Albouy, A.: The symmetric central configurations of four equal masses. In: Hamiltonian Dynamics and Celestial Mechanics. Contemp. Math., vol. 198, pp. 131--135. AMS (1996)
  2. Albouy, A., Cabral, H.E., Santos, A.A.: Some problems on the classical nn-body problem. Celest. Mech. Dyn. Astron. 113 , 369--375 (2012)
  3. Albouy, A., Fu, Y., Sun, S.: Symmetry of planar four-body convex central configurations. Proc. R. Soc. A 464 , 1355--1365 (2008)
  4. Armand, M., Grégoire, B., Spiwack, A., Théry, L.: Extending Coq with imperative features and its application to SAT verification. In: Interactive Theorem Proving (ITP 2010). LNCS, vol. 6172, pp. 83--98. Springer (2010)
  5. Barendregt, H., Barendsen, E.: Autarkic computations in formal proofs. J. Autom. Reasoning 28 (3), 321--336 (2002)
  6. Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Theoretical Aspects of Computer Software (TACS 1997). LNCS, vol. 1281, pp. 515--529. Springer (1997)
  7. Brakensiek, J., Heule, M., Mackey, J., Narváez, D.: The resolution of Keller's conjecture. In: Automated Reasoning (IJCAR 2020). LNCS, vol. 12166, pp. 48--65. Springer (2020)
  8. Carneiro, M.: Lean4Lean: Towards a verified typechecker for Lean, in Lean. arXiv:2403.14064 (2024)arXiv
  9. Corbera, M., Cors, J.M., Roberts, G.E.: Classifying four-body convex central configurations. Celest. Mech. Dyn. Astron. 131 , Paper 34 (2019)
  10. de Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Automated Deduction (CADE 28). LNCS, vol. 12699, pp. 625--635. Springer (2021)
Show all 38 referencesShow fewer references
  1. Dziobek, O.: Über einen merkwürdigen Fall des Vielkörperproblems. Astron. Nachr. 152 , 33--46 (1900)
  2. Gonthier, G.: Formal proof---the four-color theorem. Notices Amer. Math. Soc. 55 (11), 1382--1393 (2008)
  3. Grégoire, B., Leroy, X.: A compiled implementation of strong reduction. In: International Conference on Functional Programming (ICFP 2002), pp. 235--246. ACM (2002)
  4. Hales, T., Adams, M., Bauer, G., Dang, T.D., Harrison, J., Hoang, L.T., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, Q.T., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, T.H.A., Tran, N.T., Trieu, T.D., Urban, J., Vu, K., Zumkeller, R.: A formal proof of the Kepler conjecture. Forum Math. Pi 5 , e2 (2017)
  5. Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In: Theory and Applications of Satisfiability Testing (SAT 2016). LNCS, vol. 9710, pp. 228--245. Springer (2016)
  6. Heule, M.J.H., Scheucher, M.: Happy ending: An empty hexagon in every set of 30 points. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2024). LNCS, vol. 14570, pp. 61--80. Springer (2024)
  7. Immler, F.: Verified reachability analysis of continuous systems. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015). LNCS, vol. 9035, pp. 37--51. Springer (2015)
  8. Immler, F.: A verified ODE solver and the Lorenz attractor. J. Autom. Reasoning 61 , 73--111 (2018)
  9. Johansson, F.: Arb: efficient arbitrary-precision midpoint-radius interval arithmetic. IEEE Trans. Comput. 66 (8), 1281--1292 (2017)
  10. Krawczyk, R., Neumaier, A.: Interval slopes for rational functions and associated centered forms. SIAM J. Numer. Anal. 22 (3), 604--616 (1985)
  11. Leandro, E.S.G.: Finiteness and bifurcations of some symmetrical classes of central configurations. Arch. Ration. Mech. Anal. 167 , 147--177 (2003)
  12. Long, Y., Sun, S.: Four-body central configurations with some equal masses. Arch. Ration. Mech. Anal. 162 , 25--44 (2002)
  13. MacMillan, W.D., Bartky, W.: Permanent configurations in the problem of four bodies. Trans. Amer. Math. Soc. 34 , 838--875 (1932)
  14. Martin-Dorel, É., Melquiond, G.: Proving tight bounds on univariate expressions with elementary functions in Coq. J. Autom. Reasoning 57 (3), 187--217 (2016)
  15. Melquiond, G.: Proving bounds on real-valued functions with computations. In: Automated Reasoning (IJCAR 2008). LNCS, vol. 5195, pp. 2--17. Springer (2008)
  16. Moeckel, R.: Central configurations. In: Llibre, J., Moeckel, R., Simó, C.: Central Configurations, Periodic Orbits, and Hamiltonian Systems, pp. 105--167. Advanced Courses in Mathematics CRM Barcelona, Birkhäuser (2015)
  17. Moore, R.E., Kearfott, R.B., Cloud, M.J.: Introduction to Interval Analysis. SIAM (2009)
  18. Pérez-Chavela, E., Santoprete, M.: Convex four-body central configurations with some equal masses. Arch. Ration. Mech. Anal. 185 , 481--494 (2007)
  19. Shub, M.: Appendix to Smale's paper: Diagonals and relative equilibria. In: Manifolds -- Amsterdam 1970. Lecture Notes in Math., vol. 197, pp. 199--201. Springer (1971)
  20. Solovyev, A., Hales, T.C.: Formal verification of nonlinear inequalities with Taylor interval approximations. In: NASA Formal Methods (NFM 2013). LNCS, vol. 7871, pp. 383--397. Springer (2013)
  21. Subercaseaux, B., Nawrocki, W., Gallicchio, J., Codel, C., Carneiro, M., Heule, M.J.H.: Formal verification of the empty hexagon number. In: Interactive Theorem Proving (ITP 2024). LIPIcs, vol. 309, pp. 35:1--35:19 (2024)
  22. Sun, S., Xie, Z., You, P.: On the uniqueness of convex central configurations in the planar 4-body problem. Regul. Chaotic Dyn. 28 , 512--532 (2023)
  23. Tan, Y.K., Heule, M.J.H., Myreen, M.O.: cake_lpr: Verified propagation redundancy checking in CakeML. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021). LNCS, vol. 12652, pp. 223--241. Springer (2021)
  24. The mathlib Community: The Lean mathematical library. In: Certified Programs and Proofs (CPP 2020), pp. 367--381. ACM (2020)
  25. Tomar, T.S.: Uniqueness of four-body convex central configurations for all masses. arXiv:2609.35632 (2026)arXiv
  26. Tomar, T.S.: lean4body: programs, certificates and Lean formalization for the uniqueness of convex four-body central configurations, version 1.0. Zenodo (2026). 10.5281/zenodo.23004297DOI
  27. Tucker, W.: A rigorous ODE solver and Smale's 14th problem. Found. Comput. Math. 2 (1), 53--117 (2002)
  28. Xia, Z.: Convex central configurations for the nn-body problem. J. Differential Equations 200 , 185--190 (2004)

Version history

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