FIVE BODIES, A FINITE NUMBER OF PERFECT DANCES

Imagine a few stars or planets arranged so precisely that the whole group can rotate like a rigid object, without changing shape. For that to happen, the pull of gravity on each body must point exactly toward the group’s centre of mass, with a strength proportional to its distance from it. Such arrangements are called central configurations. They are the shapes of the special solutions of the n-body problem in which the bodies keep the same relative pattern, including the relative equilibria that turn rigidly.

If a pattern works, any rotated, enlarged or shifted copy of it also works, so mathematicians count them “up to similarity”.

Smale’s sixth problem

The question is simple to state: for any choice of positive masses, is the number of central configurations finite? It is the sixth problem on a list of open problems drawn up by the mathematician Smale.

Here is where things stood, according to the paper:

Three bodies: exactly five — Lagrange’s two equilateral triangles and Euler’s three straight lines.
Four bodies: finiteness was proved by Hampton and Moeckel, for all positive masses.
Five bodies in a plane: Albouy and Kaloshin proved finiteness in 2012, but only for masses outside an exceptional set — a thin family of mass combinations defined by polynomial equations, where their argument broke down.

Closing the exceptional set

Tejasvi Singh Tomar removes that exceptional set. The main theorem: for every choice of five positive masses, the planar five-body problem has finitely many central configurations up to similarity.

The strategy follows Albouy and Kaloshin. If there were infinitely many configurations, they would form a continuous curve of solutions when the equations are extended to complex numbers. Following that curve “to infinity”, the distances between the bodies must behave in ways that cancel out in a precise balance. The bodies approach one of sixteen limiting diagrams identified by Albouy and Kaloshin, each imposing conditions on the masses.

The new work makes these conditions sharp for every positive mass, and rules out the troublesome cases one by one:

configurations where four bodies form a tight cluster approached by the fifth are excluded by expanding the potential energy — which stays constant along the curve — to higher and higher order; for positive masses the resulting conditions contradict each other;
two further diagrams are shown never to occur;
for everything else, the author describes all compatible mass conditions with exact computer algebra — 2,206 algebraic systems — and, for each, produces a numerical certificate: a list of rational numbers whose properties, checked in exact arithmetic, prove that the balance is impossible.

A trap set by negative masses

There is a catch that pure algebra cannot get around. Another mathematician, Roberts, had found infinitely many central configurations for masses (1, 1, 1, 1, −¼) — with one negative mass. Flipping some signs turns it into infinitely many solutions of the complexified equations for masses (4, 4, 4, 4, 1). They are not real configurations, but an argument that only sees the complex equations cannot tell them apart.

So at those masses, and at the related ratio (1, 1, 4, 4, 4), the author counts the real configurations directly, with a computer search that uses guaranteed interval arithmetic:

for masses (1, 4, 4, 4, 4): 306 configurations up to rotation and scaling — 60 in a straight line, 24 forming a convex pentagon, the rest with one or two bodies inside;
for (1, 1, 4, 4, 4): 294.

The 60 straight-line ones match an earlier count by Moulton.

Checked by machine

A proof that rests on so many computations needs strong verification. Each certificate was rechecked by a separate program written from the paper’s definitions. Above all, the theorem is proved in the Lean 4 proof assistant, a program that checks every logical step. The formal proof does not even assume Albouy and Kaloshin’s results: it rederives what it needs, finding by search 1,376 labelled diagrams that satisfy their rules. It is accepted by two further independent checkers of Lean proofs. Building it from scratch takes about 860 CPU-hours.

The paper ends with a short statement: generative AI tools were used to find and prove the results, to write the programs and the Lean formalisation, and to draft the text. The tools are not named.

What it does and doesn’t say

The result concerns five bodies in a plane. It proves that the number of configurations is finite for every set of positive masses, but gives exact counts only at the few mass ratios studied.