AI Proof WatchKeep up with AI contributions

Uniqueness of convex four-body central configurations

For four positive masses in the planar Newtonian problem, is there exactly one strictly convex central configuration for each cyclic order, up to similarity? Nondegeneracy and dependence on the masses are related refinements.

Why it matters and what counts as progress

Why it matters: Uniqueness for every positive mass choice would complete a specific four-body central-configuration classification beyond special mass symmetries.

What counts as progress: Prove existence and uniqueness for all positive masses, establish uniform nondegeneracy or determine analytic variation of the configuration.

How the problem developed

  1. 2012 · Open problem [1]

    Alain Albouy, Hildeberto Cabral and Alan A. Santos Asked whether each choice of four positive masses and cyclic order has a unique convex planar central configuration up to similarity.

  2. 5 Mar 2019 · Classification [2]

    Montserrat Corbera, Josep M. Cors and Gareth E. Roberts Classified the full set of convex four-body central configurations for positive masses and described it as a three-dimensional graph over mass space.

  3. 1 Mar 2023 · Partial result [3]

    Shanzhong Sun, Zhifu Xie and Peng You Gave a rigorous computer-assisted uniqueness proof on a closed domain of the positive-mass space, rather than for all masses.

  4. 28 Sept 2026 · Reported claim [4]

    Tejasvi Singh Tomar Reported exactly one strictly convex planar configuration for every four positive masses and cyclic ordering, up to similarity, using interval arithmetic and an independently written second program.

AI contribution

Uniqueness of four-body convex central configurations for all masses

Tejasvi Singh Tomar

For four positive masses in the planar Newtonian problem, each cyclic order has exactly one strictly convex central configuration up to similarity. The v2 theorem also gives Q≥K/4 at every convex configuration, nondegenerate local minima and analytic dependence.

AI involvementAI-centered
ImportanceMajor
Technical verificationFormal (Lean 4 with Mathlib; kernel-checked interval certificates and Comparator)
Human understandingFull
Paper date:

Read the contribution and its assessment →

Sources

  1. Albouy, Cabral and Santos, Some problems on the classical n-body problem
  2. Corbera, Cors and Roberts, Classifying Four-Body Convex Central Configurations
  3. Sun, Xie and You, On the Uniqueness of Convex Central Configurations in the Planar 4-Body Problem
  4. Tomar, Uniqueness of four-body convex central configurations for all masses
  5. Tomar, four-body convex central configurations
  6. Four-body uniqueness Lean formalization
Website timeline

Publication dates and editorial changes.