A formal proof in Lean of the finiteness of planar central configurations of five bodies

Abstract

We describe a formalization in Lean 4 and Mathlib of the theorem that for every choice of five positive masses the planar five-body problem has finitely many central configurations up to similarity. The theorem settles Smale's sixth problem for five bodies in the plane, which Albouy and Kaloshin had solved outside a set of masses of codimension two. Its proof for all masses rests on exact computer algebra, on rational certificates and on counts of real central configurations by a branch and bound on two rays of masses and at one further mass point. The formal statement consists of twelve lines of definitions about configurations in ℂ⁵, and its proof uses only the axioms propext, Classical.choice and Quot.sound. We do not assume the results of Albouy and Kaloshin used as inputs by the informal proof. Instead we prove what we need of them at places of complex algebraic curves, which we build from the function field without a projective model, and a search by the kernel recovers their classification of limit diagrams. Almost every computation in the proof 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. The main theorem depends on 680,112 theorems proved in this way, and 621,675 of them replay the branch and bound. Two independent Lean kernels, nanoda and lean4lean, accept the main theorem together with all declarations on which it depends. We compare the formal statement with the informal one, list where the formal proof departs from the informal proof, and describe what made evaluation by the kernel feasible at this scale.