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 (2026) 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 (2026) states that generative AI tools were used to find and prove the results, write both verification programs and the Lean formalization, and draft the text.
