Theorem 2 (Albouy–Kaloshin): finiteness of planar five-body central configurations for generic masses

Open

AlbouyKaloshin.theorem2_five_body_finiteness

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

celestial-mechanicscentral-configurationsn-body-problem

There is a closed algebraic subset $A\subset\mathbb R^5$ of the mass space, of codimension at least $2$ , such that for every choice of positive masses $(m_1,\dots,m_5)\in(\mathbb R_{>0})^5\setminus A$ there are finitely many positive normalized central configurations of the planar five-body problem: configurations $(x_k,y_k)\in\mathbb R^2$ , $k=1,\dots,5$ , 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,5),\qquad y_{12}=0.

This is the main theorem of the paper and answers Smale's 6th problem for five bodies, for all positive masses outside a codimension-2 exceptional set.

Formalization Note $A$ is the real zero locus of an ideal $I\subseteq\mathbb R[m_1,\dots,m_5]$ , and "codimension at least $2$ " is expressed as $\dim_{\mathrm{Krull}}\mathbb R[m_1,\dots,m_5]/I\le3$ ; bodies $1,2$ of the paper are indices $0,1$ in Lean.

Preamble

import Mathlib
import Definitions.Def_AlbouyKaloshin_CentralConfigurations

Formal statement

namespace AlbouyKaloshin

theorem theorem2_five_body_finiteness :
    ∃ I : Ideal (MvPolynomial (Fin 5) ℝ),
      ringKrullDim (MvPolynomial (Fin 5) ℝ ⧸ I) ≤ 3 ∧
      ∀ m : Fin 5 → ℝ, (∀ k, 0 < m k) → m ∉ massZeroLocus I →
        (PosNormalizedCC 5 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 2 (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.

There exists an ideal $I$ of the ring $\mathbb R[m_0,\dots,m_4]$ of real polynomials in five variables such that (i) the Krull dimension of $\mathbb R[m_0,\dots,m_4]/I$ is at most $3$ (the zero ring, $I$ = whole ring, has dimension $-\infty$ and qualifies; $I=0$ does not, the polynomial ring having dimension $5$ ), and (ii) for every $m\in\mathbb R^5$ with all $m_k>0$ at which not every polynomial of $I$ vanishes, the set PosNormalizedCC 5 m is finite: the set of pairs $(x,y)\in\mathbb R^5\times\mathbb R^5$ such that, with $\rho_{kl}=\sqrt{(x_l-x_k)^2+(y_l-y_k)^2}$ , $\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