Theorem 1 (Hampton–Moeckel): finiteness of four-body central configurations

Open

AlbouyKaloshin.theorem1_hampton_moeckel

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

celestial-mechanicscentral-configurationsn-body-problem

Let $m_1,m_2,m_3,m_4>0$ . Then the planar four-body problem with these masses has only finitely many positive normalized central configurations: configurations $(x_k,y_k)\in\mathbb R^2$ with pairwise positive distances $r_{kl}$ satisfying

\begin{pmatrix}x_k\\y_k\end{pmatrix}=\sum_{l\ne k}m_l\,r_{kl}^{-3}\begin{pmatrix}x_k-x_l\\y_k-y_l\end{pmatrix}\quad(k=1,\dots,4),\qquad y_{12}=0.

This answers Smale's 6th problem for $n=4$ ; the paper obtains it from Theorem 5.

Preamble

import Mathlib
import Definitions.Def_AlbouyKaloshin_CentralConfigurations

Formal statement

namespace AlbouyKaloshin

theorem theorem1_hampton_moeckel (m : Fin 4 → ℝ) (hm : ∀ k, 0 < m k) :
    (PosNormalizedCC 4 m).Finite := by sorry

end AlbouyKaloshin

Source

A. Albouy and V. Kaloshin, Finiteness of central configurations of five bodies in the plane, Annals of Mathematics 176 (2012), no. 1, 535–588, https://doi.org/10.4007/annals.2012.176.1.10, p. 536, Theorem 1 (Definition 1, p. 536)

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement (Aristotle by Harmonic), with full knowledge of the source paper and of the intended meaning. It was not produced by a blind, independent auditor, so it may unconsciously read the intended meaning into the code. Reviewers must not treat it as an independent audit; compare it against the Lean code yourself.

For every real vector $m=(m_0,m_1,m_2,m_3)$ with all $m_k>0$ , the set PosNormalizedCC 4 m is finite: the set of pairs $(x,y)\in\mathbb R^4\times\mathbb R^4$ such that, with $\rho_{kl}=\sqrt{(x_l-x_k)^2+(y_l-y_k)^2}$ , one has $\rho_{kl}>0$ for all $k\ne l$ , $x_k=\sum_{l\ne k}m_l\rho_{kl}^{-3}(x_k-x_l)$ and $y_k=\sum_{l\ne k}m_l\rho_{kl}^{-3}(y_k-y_l)$ for every $k$ , and $y_1-y_0=0$ .

Human review

Endorsed by Shuze Chen · Sep 30, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph