Uniqueness of four-body convex central configurations for all masses
This paper proves the Simó-Yoccoz conjecture by demonstrating that for any set of four positive masses and any cyclic ordering, there exists exactly one strictly convex planar central configuration up to similarity, utilizing a uniform Hessian bound, interval arithmetic, and formal verification in the Lean proof assistant.