Theorem 6: five bodies, finitely many complex normalized central configurations for generic masses

Open

AlbouyKaloshin.theorem6_five_body_complex_finite

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 $(m_1,\dots,m_5)\in(\mathbb R_{>0})^5\setminus A$ the planar five-body problem has finitely many normalized central configurations, i.e. system (4) with $n=5$ has finitely many complex solutions.

This is the stronger form of the main Theorem 2, from which Theorem 2 follows.

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$ .

Preamble

import Mathlib
import Definitions.Def_AlbouyKaloshin_CentralConfigurations

Formal statement

namespace AlbouyKaloshin

theorem theorem6_five_body_complex_finite :
    ∃ I : Ideal (MvPolynomial (Fin 5) ℝ),
      ringKrullDim (MvPolynomial (Fin 5) ℝ ⧸ I) ≤ 3 ∧
      ∀ m : Fin 5 → ℝ, (∀ k, 0 < m k) → m ∉ massZeroLocus I →
        (NormalizedCC 5 (fun k => (m k : ℂ))).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. 581, Theorem 6

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 the quotient ring $\mathbb R[m_0,\dots,m_4]/I$ is at most $3$ (the Krull dimension of the zero ring, i.e. $I$ the whole ring, counts as $-\infty$ and satisfies this), and (ii) for every $m\in\mathbb R^5$ with all $m_k>0$ and such that not every polynomial of $I$ vanishes at $m$ , the set NormalizedCC 5 m (masses viewed as complex numbers) is finite, i.e. there are finitely many triples $(x,y,\delta)$ , $x,y\in\mathbb C^5$ , $\delta$ a symmetric $5\times5$ complex array with zero diagonal, with $\delta_{kl}^2((x_l-x_k)^2+(y_l-y_k)^2)=1$ for $k\ne l$ , $x_k=\sum_{l\ne k}m_l\delta_{kl}^3(x_k-x_l)$ , $y_k=\sum_{l\ne k}m_l\delta_{kl}^3(y_k-y_l)$ for all $k$ , and $y_1=y_0$ . Note $I=0$ is excluded by (i), since $\mathbb R[m_0,\dots,m_4]$ has Krull dimension $5$ .

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