Smale's sixth problem for six bodies in the plane: finiteness of central configurations for generic masses, with a proof formalized in Lean

Abstract

Smale's sixth problem asks whether, for every choice of positive masses, the number of central configurations up to similarity is finite. We prove that it is finite for six bodies in the plane and all positive masses outside a proper algebraic subset of the mass space. We follow Albouy and Kaloshin: infinitely many central configurations would give a curve of complex solutions, and the valuations of the mutual distances at its points at infinity must balance. Summed over the fifteen pairs of bodies, the balance shows that at some point at infinity the product of the mutual distances does not tend to zero. For each of the 191 classes of diagrams allowed by the rules of Albouy and Kaloshin that we use, we enumerate the possible valuations at such a point as polyhedral cells, with exact rational certificates. We exclude all but 43 of the 91,273 cells at generic masses, by a single dominant term or by Gröbner bases over the field of rational functions of the masses. For 90,943 of the 91,273 cells we also give a proof by hand from the trees and the terms of least exponent of the cell. The 43 cells not excluded lie in seven diagrams. For these we use the torque of a cluster of bodies together with the leading configurations of the clusters, and in two of them a leading system that has no solution at generic masses. Each resulting condition on the masses is shown to be nontrivial at a single mass point. The theorem is formalized in the Lean proof assistant and proved there, with no hypotheses beyond those of its statement. Lean's kernel checks the formal proof with the standard axioms only, except two dimension bounds, which run as compiled code whose execution is trusted. The exceptional set is not described; it contains every mass vector in which three masses are equal or one mass is the sum of two others. Finiteness for all positive masses remains open.