← All problems

✦
Smale's 1998 list, Problem 6

Central Configurations Finiteness

For each n ≥ 4, are there only finitely many central configurations of n point masses under Newtonian gravity?

Progress

80%
Lean-verified proof skeleton
Current approach
Algebraic geometry + Morse theory on the configuration space quotient; finiteness via critical point count on a compact manifold.
Status notes
Core finiteness argument Lean-verified for positive masses. Extension to general mass signs is the remaining target.

Direct contributions

1 paper
Formal Verification Working Paper Lean DOI Flagship
Dimension-Independent Finiteness of Central Configurations for Positive Masses
We prove that for any $N \geq 3$ bodies with positive masses in $\mathbb{R}^d$ ($d \geq 2$), the number of central configurations modulo similarity is finite, resolving Smale's 6th Problem in **every spatial dimension $d \geq 2$ simultaneously**.
18,003 words 1 claims