Formal Verification of a Computer-Assisted Proof in Celestial Mechanics
In plain words
Albouy, Fu and Sun conjectured in 2008 that four masses, arranged in a given order, have exactly one convex shape in which they can spin together rigidly. An earlier paper proved it with a computer calculation. This paper checks the whole proof, including that calculation, inside the core checker of the proof assistant Lean, so no compiler needs to be trusted. The trick is to store each number range as two whole numbers, so the checker can hand the arithmetic to a fast library. A second checker, which does its own arithmetic, accepts the proof too.
Abstract
Albouy, Fu and Sun conjectured in 2008 that four positive masses admit, for each cyclic order of the bodies, exactly one convex central configuration up to similarity; the question is Problem 10 of a 2012 list of open problems on the n-body problem. We recently proved the conjecture by reducing it to an inequality for a trace at the real zeros of an equation in four variables; a branch and bound that starts from a grid of 136,448 boxes establishes the inequality. In this paper we describe a formalization of the whole proof in Lean 4 and Mathlib in which Lean's kernel checks the computation, using <code>decide +kernel</code>, so that no compiler has to be trusted. Our checker stores an interval as two natural numbers in a biased fixed-point format. The kernel can then hand all the arithmetic to GMP. Functions are enclosed over boxes by first-order slopes. An unverified search records the decisions for each box in one natural number, and the checker replays them. We write each formula once over a type class; evaluating it at a type that pairs a real number with an interval then proves the enclosure correct. Checking the 3418 certificate theorems takes 7.6 hours of processor time, and the independent type checker nanoda accepts the proof. A version rebuilt on one eighth of the boxes passed three type checkers in 2.9 hours on a public registry of formal proofs.
