A central configuration in the n-body problem is defined for bodies of positive masses 
at positions 
. Let 
be their center of mass and
let 
be the Newtonian potential. A collision-free configuration 
is a central configuration if there is a number 
such that
 |
Central configurations generate homographic motions of the bodies. In the plane, each one generates a relative equilibrium that rotates rigidly about the center of mass. They are therefore normally considered up to similarity.
Tomar (2026a) proved that, for every choice of four positive masses and every cyclic ordering of the bodies, there is exactly one strictly convex planar central configuration with that ordering, up to similarity. This settles the Simó-Yoccoz conjecture. The proof uses interval arithmetic; the computation was repeated with an independently written program, and the uniqueness theorem and its computation were formalized in Lean and checked by its kernel.
Tomar (2026a) states that generative AI tools were used to find and prove the results and write both verification programs and the Lean formalization.
Tomar (2026b) reported that, for every choice of five positive masses, the planar five-body problem has finitely many central configurations up to similarity.
This addresses the planar five-body case of problem 6 in Smale's
problems, not the problem for an arbitrary number of bodies. For masses proportional
to a permutation of 
and 
, Tomar (2026b) reports exactly 306 and 294 central
configurations, respectively, up to orientation-preserving similarity.
The certificates and Lean formalization have not been independently checked here.
Tomar (2026b) states that generative AI was used to find and prove the results and
write the verification programs and formalization.
