cs.LO — Logic in Computer Science
A formal proof in Lean of the finiteness of planar five-body central configurations for all positive masses
Smale's sixth problem asks whether, for every choice of positive masses, there are finitely many central configurations up to similarity. For five bodies in the plane, Albouy and Kaloshin proved finiteness outside a set of masses of codimension two. In a companion paper the author proved finiteness for every choice of five positive masses by their method, adding steps that cannot be checked by hand: exact computer algebra, rational certificates and a branch and bound. We formalize this theorem in Lean 4 with Mathlib without assuming the results of Albouy and Kaloshin that the informal proof uses. Instead we prove what the proof needs of their rules on limit diagrams, of their classification of these diagrams and of their mass conditions. We do so at places of complex algebraic curves, taken as valuations of the function field rather than points of a projective model. Almost every computation becomes data for a checker that we write in Lean, prove sound with respect to Mathlib's real and complex numbers, and run in the kernel (proof by reflection). The main theorem depends on about theorems proved in this way, and Mathlib's tactics prove the few other computations. The proof uses only Lean's three standard axioms, and two independent Lean kernels, nanoda and lean4lean, accept it.