\documentclass[11pt]{amsart} \pdfsuppressptexinfo=-1 \usepackage[margin=1.1in]{geometry} \usepackage[T1]{fontenc} \usepackage{lmodern} \usepackage{amsmath,amssymb,amsthm,mathtools} \usepackage{booktabs,enumitem,array} \usepackage{listings} \usepackage{xcolor} \usepackage{tikz} \usetikzlibrary{arrows.meta,positioning} \usepackage{microtype} \usepackage[hidelinks]{hyperref} \hypersetup{pdftitle={A formal proof in Lean of the finiteness of planar five-body central configurations for all positive masses}, pdfauthor={Tejasvi Singh Tomar}} \setlength{\emergencystretch}{2em} \frenchspacing \raggedbottom \setlength{\belowcaptionskip}{4pt} % Sentences that wait for a decision of the author are wrapped in \pending{...}. % Compile with \def\PENDINGFATAL{} before \input to make any remaining \pending an error. \newif\ifpendingfatal \ifdefined\PENDINGFATAL\pendingfataltrue\fi \newcommand{\pending}[1]{\ifpendingfatal\errmessage{PENDING TEXT LEFT IN THE PAPER}\fi\textbf{[PENDING: }#1\textbf{]}} \theoremstyle{plain} \newtheorem{theorem}{Theorem}[section] \theoremstyle{remark} \newtheorem{remark}[theorem]{Remark} \newcommand{\R}{\mathbb{R}} \newcommand{\C}{\mathbb{C}} \newcommand{\Q}{\mathbb{Q}} \newcommand{\Z}{\mathbb{Z}} \newcommand{\N}{\mathbb{N}} \DeclareUrlCommand\file{\urlstyle{tt}\def\UrlBreaks{\do\/}\def\UrlBigBreaks{}\def\UrlOrds{\do\*\do\-\do\~\do\'\do\"\do\.\do\_}} \DeclareUrlCommand\lean{\urlstyle{tt}\def\UrlBreaks{\do\.}\def\UrlBigBreaks{}\def\UrlOrds{\do\*\do\-\do\~\do\'\do\"\do\_}} \newcommand{\Tom}{\cite{Tom26a}} \lstdefinelanguage{lean}{ keywords={def,theorem,structure,where,abbrev,by,fun,let,if,then,else,noncomputable,open,namespace,end}, sensitive=true, comment=[l]{--}, morecomment=[s]{/-}{-/}, } \lstset{ language=lean, basicstyle=\ttfamily\footnotesize, keywordstyle=\bfseries, columns=fullflexible, keepspaces=true, captionpos=t, frame=tb, framesep=3pt, aboveskip=8pt, belowskip=6pt, abovecaptionskip=2pt, belowcaptionskip=6pt, escapeinside={(*}{*)}, upquote=true, } \begin{document} \title[Finiteness of planar five-body central configurations in Lean]{A formal proof in Lean of the finiteness of planar five-body central configurations for all positive masses} \author{Tejasvi Singh Tomar} \renewcommand{\urladdrname}{{\itshape ORCID}} \urladdr{\href{https://orcid.org/0000-0003-4668-3639}{https://orcid.org/0000-0003-4668-3639}} \subjclass[2020]{68V20, 68V15, 70F10, 70F15, 14H05} \keywords{Central configurations, five-body problem, Smale's sixth problem, Lean, Mathlib, proof by reflection, computer-assisted proof, formal verification, valuations} \begin{abstract} 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 $680{,}000$ 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. \end{abstract} \maketitle \section{Introduction}\label{sec:intro} A configuration $q=(q_1,\dots,q_n)$ of distinct points in the plane, with positive masses $m_1,\dots,m_n$, is a \emph{central configuration} if there are $\lambda\in\R$ and $c\in\R^2$ such that \begin{equation}\label{eq:cc} \lambda\,m_i(q_i-c)=\sum_{j\ne i}\frac{m_im_j\,(q_i-q_j)}{|q_i-q_j|^3}\qquad(i=1,\dots,n). \end{equation} Central configurations are the shapes of homographic solutions in the Newtonian $n$-body problem, and a configuration similar to a central configuration is again one. Smale's sixth problem \cite{Sma98} asks whether, for every choice of positive masses, there are finitely many central configurations up to similarity. Hampton and Moeckel \cite{HM06} proved finiteness for four bodies. For five bodies in the plane, Albouy and Kaloshin \cite{AK12} proved it when the masses lie outside a closed algebraic subset of codimension two. The author's paper \Tom\ removes the exceptional set. \begin{theorem}[{\cite[Theorem~1.1]{Tom26a}}]\label{thm:main} For every $m\in(\R_{>0})^5$ the planar five-body problem with masses $m$ has finitely many central configurations up to similarity. \end{theorem} Z.~Chen and Z.~Tong \cite{CT26} state the same theorem and give a different proof, which, as far as we know, has not been formalized. The method of \cite{AK12} starts from the fact that infinitely many central configurations would give a curve of complex solutions, at whose places at infinity the valuations of the mutual distances must balance; this is the balancing condition of \cite{AK12}. The proof in \Tom\ follows this method, but it adds two kinds of steps that a reader cannot check by hand. First, there is exact computer algebra. Standard bases and minimal primes over $\Q$ give ideals on sixteen strata, which describe the sets of mass conditions that can hold together at positive masses \cite[\S8]{Tom26a}. Then rational certificates show that the balancing condition of \cite{AK12} fails under the resulting sets of conditions, except at two mass points and on a few one-parameter families of masses \cite[Theorem~8.2]{Tom26a}. Further certificates treat the two mass points, relative to a smaller hull of diagram~$5$, and the one-parameter families. At finitely many points of the families they use Gr\"obner bases modulo large primes with a lifting argument. Second, there is a counting step. On the rays through $(1,4,4,4,4)$ and $(1,1,4,4,4)$, and at one further mass point, the certificates do not apply. There the real central configurations are counted by a branch and bound in outward-rounded floating point \cite[\S10]{Tom26a}. Independent programs re-check most of these computations \cite[\S12]{Tom26a}, but they still rely on computer algebra systems and on floating-point code. We formalized the whole proof in Lean~4 \cite{dMU21} with Mathlib \cite{mC20}. The theorem \lean{CC5Full.Core.Compose.MainTheorem_holds} proves the formal statement \lean{CC5Full.MainTheorem} of Theorem~\ref{thm:main} with no hypotheses, using only the three standard axioms (\S\ref{ss:trust}). We do not assume the inputs from \cite{AK12} that are listed in \cite[\S2.6]{Tom26a}. Data produced by our programs enter only as certificates checked by the Lean kernel. Almost all of them go through checkers that we have proved sound in Lean, and a few polynomial identities and inequalities through Mathlib's tactics. The main theorem and the declarations on which it depends form its closure. Lean's kernel checks each of them when its module is built, and the independent kernels nanoda \cite{nanoda} and lean4lean \cite{Car24} check the whole closure again from exports (\S\ref{sec:kernels}). We write for a reader who knows the mathematics. In \S\ref{sec:statement} we state the formal theorem and compare it with Theorem~\ref{thm:main}. In \S\ref{sec:arch} we describe how the informal proof maps onto the development, with a table that links the main results of \Tom\ to Lean statements and their proofs, and we list where the formal proof departs from \Tom. The new parts of the development are the subject of \S\S\ref{sec:places}--\ref{sec:kernels}: a theory of places of complex algebraic curves, built on Mathlib, in which we prove the inputs from \cite{AK12} (\S\ref{sec:places}); checkers for the certificates, written so that the kernel can evaluate them at this scale (\S\ref{sec:certs}); and the check of the whole closure by two independent kernels, which revealed an issue in one of them (\S\ref{sec:kernels}). In \S\ref{sec:repro} we describe how we reproduce the build, with all checks collected in Table~\ref{tab:checks}, and in \S\ref{sec:discussion} we compare the project with other formal proofs that depend on large computations. \emph{Citations and files.} We cite the statements of \Tom\ by their numbers in its version~2. File names refer to the Lean project \texttt{lean\_full} (package \texttt{CC5Full}) at commit \texttt{52858e1}, in the supplementary material \cite{Tom26b}. Paths in tables are relative to the project directory \file{CC5Full/} unless they start with it. \section{The formal statement}\label{sec:statement} Lean checks the proof of the formal statement, but only a reader can check that the statement is the intended theorem. Translations between informal and formal mathematics can fail in subtle ways \cite{BCH26}. We therefore print the statement in full, compare it with Theorem~\ref{thm:main} line by line, and say exactly what has to be trusted. \subsection{The definitions} In Listing~\ref{lst:statement} we copy the definitions of \file{CC5Full/System.lean}, lines~38--66, with \lean{Masses} from \file{CC5Full/Basic.lean}, line~26, and the final theorem. \lean{MainTheorem} uses twelve lines of these definitions. We also show \lean{SimilarOP}, the orientation-preserving relation, which \lean{MainTheorem} does not use. After \texttt{import CC5Full.Core.Compose.Main}, the command \texttt{\#print CC5Full.IsCC} and its analogues print the elaborated definitions, in which the casts appear explicitly. With the option \texttt{pp.all}, Lean prints them without any notation. \begin{lstlisting}[float=tp,caption={[The formal statement]The formal statement of Theorem~\ref{thm:main} (\file{Basic.lean}, line~26; \file{System.lean}, lines~38--66) and its proof (\file{Core/Compose/Main.lean}, line~48), without the docstrings. Here \texttt{univ.erase i} is the set of indices $j\ne i$. The map \texttt{starRingEnd}~$\C$ is complex conjugation. \lean{MainTheorem} does not use \lean{SimilarOP}.},label=lst:statement] abbrev Masses := Fin 5 (*$\to$*) (*$\mathbb{R}$*) abbrev Conf := Fin 5 (*$\to$*) (*$\mathbb{C}$*) def CollisionFree (q : Conf) : Prop := (*$\forall$*) i j, i (*$\neq$*) j (*$\to$*) q i (*$\neq$*) q j def IsCC (m : Masses) (q : Conf) : Prop := CollisionFree q (*$\wedge$*) (*$\exists$*) (lam : (*$\mathbb{R}$*)) (c : (*$\mathbb{C}$*)), (*$\forall$*) i, ((lam * m i : (*$\mathbb{R}$*)) : (*$\mathbb{C}$*)) * (q i - c) = (*$\sum$*) j (*$\in$*) univ.erase i, ((m i * m j / (*$\|$*)q i - q j(*$\|$*) ^ 3 : (*$\mathbb{R}$*)) : (*$\mathbb{C}$*)) * (q i - q j) def Similar (q q' : Conf) : Prop := (*$\exists$*) a b : (*$\mathbb{C}$*), a (*$\neq$*) 0 (*$\wedge$*) (((*$\forall$*) i, q' i = a * q i + b) (*$\vee$*) ((*$\forall$*) i, q' i = a * starRingEnd (*$\mathbb{C}$*) (q i) + b)) def SimilarOP (q q' : Conf) : Prop := (*$\exists$*) a b : (*$\mathbb{C}$*), a (*$\neq$*) 0 (*$\wedge$*) (*$\forall$*) i, q' i = a * q i + b def FinitelyManyCC (m : Masses) : Prop := (*$\exists$*) F : Finset Conf, (*$\forall$*) q, IsCC m q (*$\to$*) (*$\exists$*) q' (*$\in$*) F, Similar q' q def MainTheorem : Prop := (*$\forall$*) m : Masses, ((*$\forall$*) i, 0 < m i) (*$\to$*) FinitelyManyCC m theorem MainTheorem_holds : MainTheorem := MainTheorem_of_interface_holds Interface_holds \end{lstlisting} \subsection{Line by line} In Table~\ref{tab:fidelity} we match each part of Theorem~\ref{thm:main}, and of equation~\eqref{eq:cc}, which defines central configurations, with its counterpart in Listing~\ref{lst:statement}. \begin{table}[tp] \caption[]{Theorem~\ref{thm:main} and equation~\eqref{eq:cc} against the formal definitions.}\label{tab:fidelity} \centering \footnotesize \begin{tabular}{@{}>{\raggedright}p{0.36\textwidth}>{\raggedright\arraybackslash}p{0.57\textwidth}@{}} \toprule Theorem~\ref{thm:main} and \eqref{eq:cc} & Listing~\ref{lst:statement}\\ \midrule five bodies $1,\dots,5$ & the elements \texttt{0}, \dots, \texttt{4} of \texttt{Fin 5}\\ masses $m\in(\R_{>0})^5$ & \texttt{m : Masses}, a function \texttt{Fin 5}~$\to\R$, with the hypothesis \mbox{\texttt{$\forall$ i, 0 < m i}} of \lean{MainTheorem}\\ a configuration $q$ in the plane $\R^2$ & \texttt{q : Conf}, a function \texttt{Fin 5}~$\to\C$\\ of distinct points & \texttt{CollisionFree q}\\ there are $\lambda\in\R$ and $c\in\R^2$ & \texttt{$\exists$ (lam : $\R$) (c : $\C$)}\\ $\lambda m_i(q_i-c)$ & \texttt{((lam * m i : $\R$) : $\C$) * (q i - c)}\\ $\sum_{j\ne i}m_im_j(q_i-q_j)/|q_i-q_j|^3$ & \texttt{$\sum$ j $\in$ univ.erase i, ((m i * m j / $\|$q i - q j$\|$ \^{} 3 : $\R$) : $\C$) * (q i - q j)}\\ for $i=1,\dots,5$ & \texttt{$\forall$ i}\\ $q$ is similar to $q'$ & \texttt{Similar q' q}: $q=aq'+b$ or $q=a\bar q'+b$ for some $a,b\in\C$, $a\ne0$\\ finitely many central configurations up to similarity & \texttt{FinitelyManyCC m}: a finite set \texttt{F} of configurations such that each \texttt{q} with \texttt{IsCC m q} is similar to a member of \texttt{F}\\ for every $m$ & \lean{MainTheorem}: \texttt{$\forall$ m : Masses}, under the hypothesis above\\ \bottomrule \end{tabular} \end{table} \subsection{Conventions}\label{ss:conv} Apart from conventions, the two statements agree. We discuss each convention in turn. \begin{enumerate}[label=(\alph*), leftmargin=*] \item \emph{Indices.} Body $k$ of \Tom\ is \texttt{k-1} in \texttt{Fin 5}. \item \emph{The plane.} The plane is $\C$, with $q=x+iy$. The norm on $\C$ is the Euclidean norm. Real numbers act on $\C$ through the cast $\R\to\C$. Equation~\eqref{eq:cc} in $\R^2$ is therefore the equation of \lean{IsCC} in $\C$. \item \emph{The multiplier and the centre.} As in~\eqref{eq:cc}, $\lambda\in\R$ and $c\in\C$ are existentially quantified, with no further condition. For positive masses the equation forces $\lambda>0$ and makes $c$ the centre of mass. We prove $\lambda\ne0$ (\lean{lam_ne_zero_of_isCC}, \file{Theory/CorU/SlicePoint.lean}) and $\lambda>0$ (\lean{lam_pos}, \file{Core/E3/Norm.lean}), as in the proof of \cite[Lemma~2.1]{Tom26a}, but the statement does not need these facts. \item \emph{Collisions.} Division in Lean is total, with $x/0=0$. Since \lean{IsCC} requires \texttt{CollisionFree q}, the denominators $\|q_i-q_j\|^3$ are nonzero and this convention never applies. \item \emph{Reflections.} \lean{Similar} admits all plane similarities, $z\mapsto az+b$ and $z\mapsto a\bar z+b$ with $a\ne0$. If \lean{SimilarOP} replaces \lean{Similar} in \lean{FinitelyManyCC}, only orientation-preserving similarities are admitted. This variant is formally the stronger statement: it implies the formal one at once. Conversely, suppose that a finite set $F$ represents all central configurations up to similarity. Then $F$ together with the complex conjugates of its members represents them up to orientation-preserving similarity, since $a\bar q'+b=aq''+b$ with $q''=\bar q'$. We have not formalized this one-line argument. Thus the formal theorem is the version with reflections, from which the version without them follows by this argument. \item \emph{Representatives.} \lean{FinitelyManyCC} asks for a finite set of representatives, which need not be central configurations themselves. Since similarity is an equivalence relation, such a set exists if and only if the central configurations fall into finitely many similarity classes: distinct classes are similar to distinct members of the set. \item \emph{Masses.} The only hypothesis on $m$ is $m_i>0$ for all $i$, as in Theorem~\ref{thm:main}, and the statement does not normalize, order or scale the masses. Internally, the proof passes to sorted masses as in \cite[Lemma~8.1]{Tom26a}, since settledness and finiteness are invariant under scaling and relabelling (\lean{Settled_invariant_holds} and \lean{Lem_slice_c_holds}, \file{Core/Reduction.lean}). \end{enumerate} \subsection{The trusted base}\label{ss:trust} To accept Theorem~\ref{thm:main} from the formal proof, a reader has to accept three things. \begin{enumerate}[label=(\roman*), leftmargin=*] \item The definitions of Listing~\ref{lst:statement}, read with Mathlib's definitions of $\R$, $\C$, the norm of $\C$, complex conjugation, finite sets and finite sums, express Theorem~\ref{thm:main}. This is the comparison above. \item The axioms \texttt{propext}, \texttt{Classical.choice} and \texttt{Quot.sound}, the standard axioms of Lean and Mathlib, are acceptable. For \lean{CC5Full.Core.Compose.MainTheorem_holds}, the command \texttt{\#print axioms} lists exactly these. \item A Lean kernel checks proofs correctly. The development is built with the toolchain \texttt{v4.35.0-rc3}, a release candidate. Lean's own kernel uses the GMP library for arithmetic on natural-number literals. A declaration is checked when its module is built (\S\ref{sec:repro}). No file sets the option \texttt{debug.skipKernelTC}, which would skip this check (Table~\ref{tab:checks}). Since Lean does not check imported modules again and accepts modules built on other machines by their build traces, this route also trusts the build products. From exports of these products, Lean's kernel checks the closure with the certificate theorems assumed, while two independent kernels check it in full. That route trusts the exporter and the scripts that join the parts instead (\S\ref{sec:kernels}). \end{enumerate} Beyond these points and the infrastructure of item (iii), nothing needs to be trusted. Indeed, the elaborator and the tactics only produce terms for the kernel to check, and Mathlib's proofs are checked in the same way. All other definitions in the project, including the files that state the intermediate results of \Tom, belong to the proof: if one of them did not mean what its docstring says, \lean{MainTheorem_holds} would still prove \lean{MainTheorem}. Docstrings and names are not checked by the kernel. Finally, the certificate generators and the computer algebra systems behind them only produce data, and the kernel checks those too. \subsection{What the formal proof does not state}\label{ss:notstated} Theorems~10.1 and~10.2 of \Tom\ count $306$ and $294$ central configurations up to orientation-preserving similarity on the two rays ($183$ and $177$ up to similarity). They also state that these central configurations are nondegenerate, count them by shape, and give the numbers $612$ and $588$ of positive normalized central configurations. Theorem~10.7 states the same, with the numbers of Theorem~10.1, at the point $P_1=(9,36,36,36,4)$. These statements enter the formal proof only through their finiteness. At each of the three mass points and in each of its five search regions, we prove the exact number of chart points of normalized central configurations in the search box. For instance, \lean{CC5Full.Core.E3.Run.A.count0} gives $168$ (\file{Core/E3/Run/A/Final.lean}). These numbers add up to $306$, $294$ and $306$, but we do not identify them formally with the numbers of central configurations up to orientation-preserving similarity. Besides these statements and the argument of \S\ref{ss:conv}(e), the formal proof leaves out the cross-checks of \cite[\S12.3]{Tom26a}. It also bypasses the statements replaced by other arguments in \S\ref{ss:departures}: Propositions~5.34 and~5.35, the decomposition in the proof of Proposition~8.7(a), and the results of \cite{AK12} on singular sequences, none of which the formal proof of Theorem~\ref{thm:main} needs. \section{From the informal to the formal proof}\label{sec:arch} \subsection{The informal proof}\label{ss:outline} We recall the argument of \Tom\ in the terms used in the formalization. Normalized central configurations, the solutions of~\eqref{eq:cc} with $\lambda=1$ and $c=0$, correspond to zeros of a polynomial system in $\C^{18}$. The coordinates are $u_1,\dots,u_4$ and $v_1,\dots,v_4$ for the positions in the two colours $z=x+iy$ and $w=x-iy$, and $p_{kl}=r_{kl}^{-1}$ for the inverse distances, and a central configuration gives a zero with $v=\bar u$ and $p>0$. On this system the potential $U=\sum_{k=Stealth] \node[box] (main) at (0,0) {Theorem 1.1\\ \texttt{MainTheorem\_holds}}; \node[box] (rays) at (-4.6,-1.8) {Theorems 10.1, 10.2, 10.7\\ (finiteness)\\ branch and bound, \file{Core/E3}}; \node[box] (coru) at (-0.6,-1.8) {Corollary 2.5\\ \file{Theory/CorU}}; \node[box] (cors) at (3.6,-1.8) {Corollary 8.3\\ \file{Core/Strata}, \file{Core/Curves}}; \node[box] (thms) at (-0.6,-3.8) {Theorem 8.2\\ flats and certificates}; \node[box, right=4mm of thms] (fam) {point and family\\ certificates, \cite[\S\S6, 9]{Tom26a}}; \node[box, right=4mm of fam] (theory) {\texttt{TheoryForCore}\\ places, types, \cite[\S5]{Tom26a}}; \node[box, below=7mm of thms] (lex) {lexicographic\\ certificates}; \node[box, below=7mm of theory] (cores) {algebraic cores\\ \file{Core/E2}, \file{Core/E4}, \file{Core/VN}}; \draw[->] (rays) -- (main); \draw[->] (coru) -- (main); \draw[->] (cors) -- (main); \draw[->] (thms) -- (cors); \draw[->] (fam) -- (cors); \draw[->] (theory) -- (cors); \draw[->] (lex) -- (thms); \draw[->] (cores) -- (theory); \end{tikzpicture} \caption[]{The main dependencies of the formal proof. An arrow points from a result to a result that uses it.}\label{fig:deps} \end{figure} \subsection{Informal and formal statements}\label{ss:table} In Table~\ref{tab:corr} we link the main results of \Tom\ to the formal statements and to the theorems that prove them. Most formal statements are propositions defined in the statement files. The theorem that proves a proposition \lean{Foo} is usually named \lean{Foo_holds}. Docstrings in the Lean files cite these results by number and by \LaTeX\ label. \begin{table}[tp] \caption[]{Results of \Tom\ and the theorems that prove them. Lean names are relative to the namespace \lean{CC5Full} or \lean{CC5Full.Core}. Paths are relative to \file{CC5Full/}. The theorems in \file{Core/Compose} combine theorems of the two parts.}\label{tab:corr} \centering \footnotesize \begin{tabular}{@{}>{\raggedright}p{0.19\textwidth}>{\raggedright}p{0.25\textwidth}>{\raggedright\arraybackslash}p{0.505\textwidth}@{}} \toprule \Tom & formal statement & proof (file, line)\\ \midrule Theorem 1.1 & \lean{MainTheorem} & \lean{Compose.MainTheorem_holds} (\file{Core/Compose/Main.lean},~48)\\ \S11, proof of \mbox{Theorem 1.1} & \lean{MainTheorem_of_interface} & \lean{Compose.MainTheorem_of_interface_holds} (\file{Core/Compose/MainAssembly.lean},~18)\\ Corollary 2.5 & \lean{Cor_U} & \lean{Theory.Cor_U_holds} (\file{Theory/CorU/CorU.lean},~24)\\ Lemma 2.4(b) & \lean{Lem_U_b} & \lean{Theory.Lem_U_b_holds} (\file{Theory/ConstU.lean},~58)\\ balancing (2.3), (3.1) & \lean{Balancing}, \lean{BalancingTypes} & \lean{Theory.Balancing_holds}, \lean{Theory.BalancingTypes_holds} (\file{Theory/FunctionField/Divisor.lean},~255, 340)\\ classification of \cite[\S7]{AK12} & \lean{Classification} & \lean{Theory.Types.Classification_holds} (\file{Theory/Types/Residual.lean},~626)\\ Proposition 3.5 (Table 1) & \lean{TypesTable} & \lean{Theory.Types.TypesTable_holds} (\file{Theory/Types/Table.lean},~32)\\ Theorem 3.12 & \lean{Thm_types} & \lean{Compose.Thm_types_holds} (\file{Core/Compose/Theory.lean},~59)\\ Lemma 4.1 & \lean{LexLemma} & \lean{Sep.LexLemma_holds} (\file{Core/Sep/LexLemma.lean},~44)\\ Corollary 5.19 & \lean{Cor_nod15} & \lean{Theory.Cor_nod15_holds} (\file{Theory/D15/Nod15.lean},~22)\\ Theorem 5.21 & \lean{Thm_D14} & \lean{Compose.Thm_D14_holds} (\file{Core/Compose/Theory.lean},~54)\\ Theorem 5.37 & \lean{Thm_D9} & \lean{Theory.Types.Thm_D9_holds} (\file{Theory/Types/D9.lean},~15)\\ Theorem 6.2 (for K14) & \lean{Thm_KA} & \lean{K14.Thm_KA_holds} (\file{Core/K14/Torus.lean},~172)\\ Proposition 7.1 & \lean{Prop_nod2} & \lean{Compose.Prop_nod2_holds} (\file{Core/Compose/Theory.lean},~48)\\ Lemma 8.1 & \lean{Lem_R} & \lean{Reduction.Lem_R_holds} (\file{Core/Reduction.lean},~635)\\ Theorem 8.2 & \lean{Thm_S} & \lean{Strata.Thm_S_holds} (\file{Core/Strata/Final.lean},~20)\\ Corollary 8.3 (settledness part) & \lean{Cor_S} & a conjunct of \lean{Compose.CoreStatements_holds} (\file{Core/Compose/Assembly.lean},~39)\\ Proposition 9.6 & \lean{Prop_d14a} & \lean{Compose.Prop_d14a_holds} (\file{Core/Compose/D14a.lean},~42)\\ Theorems 10.1, 10.2 (finiteness) & \lean{Finite_specialRays} & \lean{E3.Finite_specialRays_holds} (\file{Core/E3/Run/Final.lean},~23)\\ Theorem 10.7 (finiteness) & \lean{Finite_P1} & \lean{E3.Finite_P1_holds} (\file{Core/E3/Run/Final.lean},~28)\\ Theorem B.1 and Remark~4.5 & \lean{V2_valid}, \lean{VN_valid} & \lean{Compose.V2_valid_holds}, \lean{Compose.VN_valid_holds} (\file{Core/Compose/Theory.lean}, 66, 70)\\ \bottomrule \end{tabular} \end{table} \subsection{Departures from the informal proof}\label{ss:departures} We follow \Tom, with the following differences. In (2)--(5) we prove its statement by another route. In (6) and (7) the formal statement is weaker than the informal one but suffices for the proof, and in (1) and (8) it differs from the informal one, as described there. \begin{enumerate}[label=(\arabic*), leftmargin=*] \item \emph{The inputs from \cite{AK12}.} In \Tom, the rules on limit diagrams, the classification into sixteen diagrams \cite[\S7, Fig.~11]{AK12} and the mass conditions of \cite[\S8]{AK12} are taken from \cite{AK12}, all for singular sequences. We prove the parts of these inputs that the proof needs at singular places of curves (\S\ref{ss:classif}). Among these results is the reduction of \cite[pp.~577--578]{AK12} to the system of \cite[\S5.4]{AK12} (\lean{FigData.kite_core}, \file{Theory/Types/LabelR.lean}), which \Tom\ cites. \item \emph{Corollary 2.5.} We choose the curve so that $U$ is not identically zero on it. The proof then does not use Lemma~2.4(b) (\S\ref{ss:coru}). \item \emph{Theorem 5.21.} At a place whose type lies in a piece $\mathsf{d14b}$, a parameter $\sigma\in(1,2)$ fixes the type. Our proof does not use Proposition~5.11, and it replaces Propositions~5.34 and~5.35 by two similar arguments, one for $\sigma<5/3$ (\file{Theory/D14/CaseLow.lean}) and one for $\sigma>11/7$ (\file{Theory/D14/CaseHigh.lean}). Together these ranges cover the range $(1,2)$ of $\sigma$, so the resonant values of $\sigma$ play no role. We prove Proposition~5.11 itself, which excludes diagram~$15$ through Corollary~5.19, by the second proof in the remarks after it: a resultant and the positivity of a polynomial $P_{11}$ (\file{Theory/CC5Alg/}). \item \emph{Relation (R2).} Relation (R2) of \cite[\S3.3]{Tom26a} is one of three relations that cut out a smaller hull $V_N$ of diagram~$5$. We derive it from one polynomial identity and $36$ factorizations (the norm over the signs of a branch, \file{Theory/VN/}), instead of $36$ eliminations by standard bases. These factorizations are checked by the kernel (\S\ref{ss:arith}). \item \emph{The zero-dimensional flats} of \cite[Proposition~8.6(d)]{Tom26a} need no prime decomposition and no real root isolation. For $75$ of the $77$ flats, an element of the ideal of the flat is positive on the stratum, by a positivity certificate (\S\ref{ss:strata}). The other two flats contain $\mathbf q_*$ and $\mathbf p_*$, one each. We treat the flat of $\mathbf p_*$ by membership certificates and that of $\mathbf q_*$ by the definition of $\mathbf q_*$. The certificates at $\mathbf q_*$ of Proposition~8.7(b) and~(c), however, are checked at an explicit point given by isolating intervals. In the proof of Corollary~8.3 we show that the point defined by the labels is this point. For this we use certificates for $630$ auxiliary polynomial systems, the branches of sixteen label sets (\file{Core/ResidualCert/}). Here $503$ systems contain a nonzero integer, so they have no zero. We treat the other $127$ by derivations with exact real root isolation. To identify the point, the informal proof instead uses a prime ideal with $48$ zeros \cite[Proposition~8.7(a)]{Tom26a}. \item \emph{Lemma 10.3(b).} We use the gaps between the projections of the bodies on a body of largest norm instead of the components of the graph $r_{ij}\le\varepsilon$, with the same constants (\lean{gap_lemma}, \file{Core/E3/Bounds.lean}). The bound holds with $\le$ in place of $<$ (\lean{sq_le_bound}). \item \emph{The branch and bound of \cite[\S10]{Tom26a}.} Where a test of the search program of \Tom\ fails in the kernel's arithmetic, the checked tree uses another test, bisections or a local search instead (\S\ref{ss:hints}). The counts are unchanged. The formal proof proves them as numbers of chart points, not as the statements of \cite[\S10]{Tom26a} about central configurations, and uses only their finiteness (\S\ref{ss:notstated}). \item \emph{The pieces of diagrams $2$ and $9$.} In the statement files, the label set $S(m)$ of Theorem~3.12 also contains labels not used in \Tom, $\mathsf L$, $\mathsf{D2K}$, $\mathsf{D2P}$ and $\mathsf N$ (\file{CC5Full/Labels.lean}). The piece $\mathsf{d2}[T]$ is present only under $\mathsf L(T)$, $\mathsf{D2K}(T)$ or $\mathsf{D2P}(T)$, and $\mathsf{d9}(T;ax,by)$ only under $\mathsf N(T;ax,by)$, whereas \cite[Table~3]{Tom26a} lists both pieces as always present. The formal Theorem~3.12 is therefore stronger than the informal one, and its proof uses Proposition~7.1 and Theorem~5.37, which exclude diagrams $2$ and $9$ at all positive masses. In \Tom\ these two results remove the same pieces after Theorem~3.12. \end{enumerate} \subsection{Generated modules}\label{ss:generated} We generate most certificates by programs outside Lean, from the data of \Tom\ and its supplementary material, and write them as Lean modules. Including Lean's and Mathlib's declarations, the main theorem depends on $2{,}831{,}937$ declarations in $90{,}536$ modules. In the library, that is, \file{CC5Full.lean} and the Lean files of \file{CC5Full/} outside its \file{scripts} directories, we store $2{,}715$ files with $420{,}540$ lines. Generators wrote about $2{,}170$ of these files, nearly all of them certificate data; the other files, about $540$ with about $129{,}000$ lines, hold the statements, the theory, the checkers and their soundness proofs. Four further families of generated modules used by the proof, with $85{,}756$ files and $3.0$~GB of Lean source, are too large to store in the repository (Table~\ref{tab:families}). For each of them, a script in the repository regenerates the files byte for byte and checks them against a manifest of SHA-256 hashes. To regenerate the generic face of Theorem~8.2 and the $630$ auxiliary systems of \S\ref{ss:departures}(5) one needs Singular~4.4.1 \cite{DGPS}, and the generic face also needs data from the supplementary material. For the branch and bound, a C++ program writes the search tree of \cite[\S10]{Tom26a} with one code per node. An exact Python mirror of the kernel's arithmetic then replays the tree (\S\ref{ss:hints}). The four families are archived in the supplementary material, with the hashes listed in \S\ref{sec:availability}. Since the kernel checks every module (\S\ref{ss:trust}), a wrong generator can only produce a module that fails to build, or a certificate for a statement that the assembly cannot use. \begin{table}[tp] \caption[]{The generated families not stored in the repository. Scripts are under \file{CC5Full/Core/scripts/}.}\label{tab:families} \centering \footnotesize \begin{tabular}{@{}>{\raggedright}p{0.4\textwidth}rr>{\raggedright\arraybackslash}p{0.22\textwidth}@{}} \toprule family (directory) & files & bytes & regenerated by\\ \midrule branch and bound of \cite[\S10]{Tom26a} (\file{Core/E3/Run}) & 83,454 & 1,560,918,323 & \mbox{\texttt{e3/run/regen.sh}}\\ generic face $1|2|3|4|5$ of Theorem 8.2 (\file{Core/Strata/Big/F1_2_3_4_5}) & 324 & 1,128,965,013 & \mbox{\texttt{strata/gen\_big.py}}\\ the $630$ auxiliary systems of \S\ref{ss:departures}(5) (\file{Core/ResidualCert/All}) & 630 & 230,621,594 & \mbox{\texttt{residual/gen\_unit.py}}, \mbox{\texttt{gen\_all.py}}\\ core of Proposition 9.6 (\file{Core/D14a/B}) & 1,348 & 83,578,754 & \mbox{\texttt{d14a/}}\\ \bottomrule \end{tabular} \end{table} \section{Curves, places and the inputs from Albouy and Kaloshin}\label{sec:places} The argument of \cite{AK12} studies \emph{singular sequences}: sequences of normalized central configurations along which some mutual distances degenerate, and how the dominant terms of the equations balance along them. Although \Tom\ works with places of curves, it takes the classification of limit diagrams from \cite{AK12}. We work only with places; each result of \cite{AK12} that the proof uses is proved at places. Mathlib has the algebra this needs (valuations, Dedekind domains, Noether normalization, ramification indices, Hahn series), but not the theory of places of curves. In this section we describe how we build that theory and how we use it. \subsection{Curves and places without a projective model}\label{ss:curves} We show the definitions in Listing~\ref{lst:curve}. Let $\C[u,v,p]$ be the ring of polynomials in the eighteen coordinates. A curve in $Y_m$ is a prime ideal of $\C[u,v,p]$ that contains the ideal of $Y_m$ and whose quotient has Krull dimension one. By the Nullstellensatz these are the irreducible closed curves of $\C^{18}$ inside $Y_m$. The function field of a curve is the fraction field of its coordinate ring. A place is a discrete valuation of the function field with values in $\Z$, trivial on the nonzero constants and taking the value~$1$. Curves and places do not occur in the formal statement of Theorem~\ref{thm:main}. They enter through Corollary~2.5, which turns settledness, a statement about all curves in $Y_m$, into finiteness. \begin{lstlisting}[float=tp,caption={[Curves and places]Curves, nontrivial curves, settledness (\file{System.lean}) and places (\file{Places.lean}). \texttt{Poly} is \texttt{MvPolynomial Coord}~$\C$, the polynomials in the eighteen coordinates. \texttt{r2P e} is $r_{kl}^2=u_{kl}v_{kl}$, and \texttt{Upoly m} is the potential $U$.},label=lst:curve] structure Curve (m : Masses) where ideal : Ideal Poly isPrime : ideal.IsPrime le_ideal : idealY m (*$\le$*) ideal dim_one : ringKrullDim (Poly (*$\diagup$*) ideal) = 1 def Curve.Nontrivial {m : Masses} (C : Curve m) : Prop := ((*$\exists$*) e, (*$\neg$*) C.IsConst (r2P e)) (*$\wedge$*) Upoly m (*$\notin$*) C.ideal def Settled (m : Masses) : Prop := (*$\forall$*) C : Curve m, (*$\neg$*) C.Nontrivial structure Place (C : Curve m) where ord : AddValuation C.FunctionField (WithTop (*$\mathbb{Z}$*)) ord_const : (*$\forall$*) c : (*$\mathbb{C}$*), c (*$\neq$*) 0 (*$\to$*) ord (C.fn (MvPolynomial.C c)) = 0 exists_ord_eq_one : (*$\exists$*) f : C.FunctionField, ord f = 1 \end{lstlisting} The proof in \Tom\ uses the smooth projective model of a curve, its places at infinity, and the fact that a nonconstant function has as many zeros as poles. We prove the facts we need directly from the definitions (\file{Theory/FunctionField/}). \begin{itemize}[leftmargin=*] \item By Noether normalization the coordinate ring of a curve is integral over $\C[t_0]$ for some transcendental $t_0$ (\lean{curve_noether}), and so the function field has transcendence degree one (\lean{trdeg_eq_one}). \item The integral closure of $\C[t_0]$ in the function field is a Dedekind domain. The maximal ideals of this closure give places centred on the curve, as adic valuations (\lean{exists_place_centred}). \item The residue field of each place is $\C$ (\lean{exists_residue_place}). \item For a transcendental function $x$, the places with $\operatorname{ord}_Px>0$ are the primes above $(x)$ in the integral closure of $\C[x]$, and their residue degrees are one. Thus the identity $\sum e_if_i=[K:\C(x)]$ of Mathlib gives $\sum_{\operatorname{ord}_Px>0}\operatorname{ord}_Px=[K:\C(x)]$ (\lean{degree_pos_places}). Applied to $x$ and to $x^{-1}$, it shows that a nonconstant function has finitely many zeros and poles, and that its orders sum to zero. Balancing follows (\lean{Balancing_holds}). \item At a place with uniformizer $t$, expanding functions digit by digit embeds the function field into $\C((t))$ as a ring and turns $\operatorname{ord}_P$ into the $t$-adic order (\lean{Expansion_exists_holds}). \end{itemize} In \cite[\S5]{Tom26a} the expansions have rational exponents, after the substitution $t=\tau^{4/d}$. We model them in Hahn series $\mathrm{HahnSeries}\ \Q\ (\C[[\delta]])$ over a ring of formal power series in the deviations $\delta$ from the leading coefficients (\file{Expansion.lean}). For the weighted systems of \cite[\S5]{Tom26a} we prove a formal implicit function theorem (\lean{FormalIFT_holds}, \file{Theory/FormalIFT/}). \subsection{Two arguments without geometry}\label{ss:coru} Two steps of \Tom\ use geometric facts about curves. We replace them by algebra. \emph{Corollary 2.5.} Suppose that $m$ has infinitely many central configurations up to similarity. Then the set $T=Y_m\cap\{U\ne0\}$ is infinite (\file{Theory/CorU/SlicePoint.lean}). Since $T$ is covered by the zero sets of the finitely many minimal primes of its vanishing ideal, one of them contains infinitely many points of $T$. This minimal prime contains the ideal of $Y_m$, it does not contain $U$, and it is not maximal, since a maximal ideal has only one zero. By Noether normalization, lying over and the fact that integral extensions of $\C[X]$ have dimension at most one, some prime of dimension one above it still does not contain $U$ (\file{Theory/CorU/Algebra.lean}). This prime is a curve on which $U$ is not identically zero. If all squared distances were constant on it, its zeros would lie in a fibre of the map $(r^2_{kl})_{k{\raggedright}p{0.25\textwidth}>{\raggedright}p{0.4\textwidth}rr@{}} \toprule family & certificate and checker & theorems & modules\\ \midrule branch and bound of \cite[\S10]{Tom26a} & one code per search-tree node, replayed in fixed-point interval arithmetic (\lean{checkTree}, \file{Core/E3/Defs.lean}) & 621,675 & 81,545\\ Propositions G.1, G.2 and the test in Proposition 9.14 & Krawczyk tests and lifting recursions in complex ball arithmetic (\file{Core/Ball/}, \file{Core/GPts/}) & 31,104 & 972\\ Proposition 9.6 & complex balls and Lyapunov--Schmidt series at special points of the families $T_3$ and $T_7$ (\file{Core/D14a/}) & 13,579 & 1,157\\ the $630$ auxiliary systems of \S\ref{ss:departures}(5) & cofactor identities over $\Z$, and derivations with root isolation (\file{Core/ResidualCert/}) & 9,560 & 630\\ Theorem 8.2, generic face & membership, positivity and chain certificates for the flats (\file{Core/Strata/}) & 1,022 & 128\\ all others & lexicographic certificates (\file{Core/LexBatch/}), runs of K14 modulo primes (\file{Core/K14Cert/}), \cite[\S9]{Tom26a} (\file{Core/Curves/}, \file{Core/Lem95/}), the cores of Theorems 5.28, 5.29 and~7.3 and of (R2) (\file{Core/E2/}, \file{Core/E4/}, \file{Core/VN/}), the other faces of Theorem 8.2, and the theory & 3,172 & 869\\ \midrule all & & 680,112 & 85,301\\ \bottomrule \end{tabular} \end{table} \subsection{Theorem 8.2: certificates for real algebraic sets}\label{ss:strata} Theorem~8.2 of \Tom\ concerns all sorted positive mass vectors. A face $F$ of the sorted cone, one of sixteen, prescribes which consecutive sorted masses are equal, and the masses are scaled to $m_5=1$. On the stratum $\Sigma_F$ put $x_i=m_i^{-1/2}$. The values $y_1>\dots>y_n$ of $x_i$ on the blocks of equal masses, other than the last block, where $x_i=1$, identify $\Sigma_F$ with the open cone $\{y_1>\dots>y_n>1\}$ \cite[\S8.4]{Tom26a}. In these coordinates a label becomes a union of algebraic sets, the zero sets of its branch ideals. On every face, the computation of \cite[\S8]{Tom26a} gives a tree of ideals, called flats, with $2206$ flats in total. We replay this tree (\file{Core/Strata/Descent.lean}) and check three kinds of certificates. \begin{itemize}[leftmargin=*] \item \emph{Membership}: an identity $\sum_jc_jg_j=d\,r\,k^N$ with $d\ne0$ in integer polynomials. It shows that $r$ or $k$ vanishes at each common zero of the $g_j$. \item \emph{Positivity}: an element $s$ of an ideal, possibly after multiplication by a power of $\prod_jy_j\prod_j(y_j-y_{j+1})\,(y_n-1)$, such that $s\circ\varphi$ is a nonzero polynomial with coefficients of one sign, where $\varphi(z)_j=1+z_j+\dots+z_n$. Since $\varphi$ maps the open positive orthant onto the cone, $s$ has no zero on the stratum (\lean{posOK_sound}, \file{Core/Strata/Pos.lean}). In the kernel, $s\circ\varphi$ is a composition of shifts $x_k\mapsto x_k+x_{k+1}$, with binomial rows by Pascal's rule. \item \emph{Chains}: residual chains of ideals, which show that a zero of an ideal in the cone lies on one of its children. \end{itemize} A descent by strong induction on the number of labels that are not attached to a flat then gives Theorem~8.2 face by face (\lean{face_sound}). Positivity certificates of degree at most~$8$, which we find by linear programming, settle $75$ of the $77$ zero-dimensional flats of case (d) of \cite[Proposition~8.6]{Tom26a}. In \Tom\ these flats are treated by prime decompositions, filters and, for four of them, real root isolation (\S\ref{ss:departures}(5)). No positivity certificate exists, of course, for a flat with a zero in the open cone, such as the flat that contains $\mathbf q_*$. For that flat we use the definition of $\mathbf q_*$ in the statement of Theorem~8.2. The certified label sets are those of the $1840$ lexicographic certificates of \Tom, checked by the kernel in $147$ declarations (\file{Core/LexBatch/ThmS/}). \subsection{The branch and bound: replaying a search}\label{ss:hints} Theorems~10.1, 10.2 and~10.7 of \Tom\ count central configurations at the mass points $(1,4,4,4,4)$, $(1,1,4,4,4)$ and $P_1$. By scaling and relabelling \cite[Lemma~2.2(c)]{Tom26a}, these three points cover the two rays and the multiples of the permutations of $P_1$. After a similarity a central configuration is normalized, with $\lambda=1$ and $c=0$ in~\eqref{eq:cc}. For fixed tie-breaking constants $c_i$, it lies in region $k$ if body $k$ maximizes $|q_i|^2+c_i$. In region $k$ we rotate the configuration so that $q_k$ lies on the positive real axis and drop one body, whose position the centre of mass determines. The remaining seven real coordinates form its \emph{chart point}. In region $k$ the chart points lie in a box $B_k$ of $\R^7$ and are zeros of a reduced system of seven equations \cite[\S10]{Tom26a}. A branch and bound tiles each box. Each leaf is either excluded by a test or certified by Krawczyk's test \cite{Kra69,Moo77} to contain exactly one zero, in its interior. The tests are the region conditions, the virial identity, cluster identities for subsets of bodies, mean-value forms of the equations, and disjointness of a box from its Krawczyk image. The checker rests on two pieces of analysis. The first, \lean{krawczyk_box} (\file{Core/E3/KrawBox.lean}), is a Krawczyk theorem on rectangular boxes, for maps with partial derivatives along coordinate lines and interval bounds on them: if the Krawczyk image lies in the open box, the map has exactly one zero in the box. The second, \lean{tiling_count} (\file{Core/E3/Tiling.lean}), counts the zeros of a tiling whose excluded leaves contain none and whose Krawczyk leaves contain one each. In \Tom\ the search ran in floating point with outward rounding. Our checker, however, uses its own arithmetic (\S\ref{ss:arith}), so a test that passes in floating point can fail in the kernel. For this reason we record one code per tree node as a hint: bisect along a given coordinate, contract, or apply a given test. The Python mirror of \S\ref{ss:generated} replays the tree, checks the hinted tests, and replaces a test that fails by another test (once after a contraction), by bisections or by a local branch and bound. The kernel checks the final tree, so the floating-point search and the replay by the mirror stay outside the trusted base of \S\ref{ss:trust}. The search of \Tom\ is split into $44$ jobs, whose boxes tile the boxes $B_k$. Altogether the final trees of the jobs have $447{,}097{,}359$ nodes. For all $44$ search jobs, the kernel's count equals the number of zeros in region $k$ recorded in the log of the job, and these logs are part of \cite{Tom26b} (Table~\ref{tab:checks}). \subsection{Encodings for the kernel}\label{ss:arith} All checkers compute with natural numbers. We choose encodings that turn the kernel's work into GMP operations on large literals. \begin{itemize}[leftmargin=*] \item \emph{Intervals.} In the branch-and-bound checker, a natural number $X$ stands for the real number $(X-2^{512})/2^{64}$. Intervals are pairs of such numbers with outward rounding. A magnitude bound certifies that no truncated subtraction underflows (\file{Core/E3/Defs.lean}). Since \texttt{Nat.sqrt} is not among the operations accelerated by the kernel, we compute integer square roots by Newton's iteration and check them by $s^2\le n<(s+1)^2$. Complex balls in a biased fixed-point format serve the Krawczyk tests of Propositions G.1 and G.2 (\file{Core/Ball/}). \item \emph{Polynomials.} A sparse polynomial is a list of terms whose exponent vectors are packed into one natural number, so that adding keys multiplies monomials (\file{Core/Sparse.lean}). A cofactor identity $\sum_jh_jG_j=g$ with millions of products does not fit in one declaration. We split the products by a label, check the intervals of labels in separate declarations, and prove that the parts add up to the identity for any choice of labels (\lean{identity_of_parts}, \file{Core/K14Cert/Sound.lean}; \lean{Ident.sound_of_parts}, \file{Core/Strata/Ext.lean}). Thus the labels affect only the cost of the check, not its soundness. \item \emph{Identities by one evaluation.} We check a polynomial identity in $\Z[t,k,d]$ with degree bounds $D_1$, $D_2$ by one evaluation at $(2^B,2^{BD_1},2^{BD_1D_2})$, where $2^B$ exceeds twice a bound on the $\ell^1$ norm of the coefficients (\lean{evC_eq_zero_of_check}, \file{Core/E2/Kron.lean}). Since the $36$ factorizations of \S\ref{ss:departures}(4) are weighted homogeneous, we may set one variable to $1$ and use this three-variable test. Together, the $36$ identities take $40.3$~s of kernel time. \item \emph{Lexicographic certificates.} A lexicographic certificate \cite[Definition~4.2]{Tom26a} is a list of integer functionals that must be nonnegative and separating on the attained faces of all pieces present for a label set. Our checker \lean{LexCert.checkFast} (\file{Core/FastLex/}) packs vertex coordinates into $48$-bit fields of one natural number and evaluates a functional on many vertices with a few multiplications and masks. The soundness theorem \lean{LexCert.checkFast_sound} reduces it to the exact check \lean{lexCheck} in the statement files. We generate the packed tables of the pieces by evaluation in Lean and check them in the kernel against the definitions in the statement files (\file{Core/FastLex/Valid.lean}). \item \emph{Rationals.} The rationals of Lean's core library are normalized fractions, whose arithmetic the kernel can evaluate. Two checkers compare rationals by their numerators and denominators (\lean{qeqb}, \file{Core/QEqb.lean}) rather than through the derived decision procedure for equality; we will explain why in \S\ref{ss:nanoda}. \end{itemize} \subsection{Writing checkers for the kernel}\label{ss:kernelstyle} The cost of a check in the kernel depends on how the checker is written. For an interval multiply-add of the branch-and-bound arithmetic we measured $79\,\mu$s of kernel time when its case distinctions are written with \texttt{Bool.rec}, $117\,\mu$s with \texttt{cond}, $155\,\mu$s with \texttt{if}, and $310\,\mu$s with integers instead of biased natural numbers. Since the kernel unfolds \texttt{Nat.sqrt} and \texttt{Nat.log2}, they are slow: $2.1$~ms and $1.7$~ms on $200$-bit numbers. In the enumeration of diagrams we write the functions with the recursors \texttt{Nat.rec} and \texttt{List.rec} on primitive operations. Functions defined by structural recursion, which go through \texttt{brecOn}, are evaluated more slowly. The cost also depends on the size of a declaration. In the branch and bound, the kernel time per leaf grows from $5.4$~ms in a declaration of $81$ leaves to $9.7$~ms in one of $2000$ leaves. We therefore cut the trees of the jobs into parts, and the parts into subtrees of weight at most $2048$, eight to a module, where a cheap leaf weighs $1$ and a node with a mean-value form, a contraction or a Krawczyk test $12$ to $30$. Batches of lexicographic certificates stay below about $5\cdot10^5$ kernel unfoldings per declaration. For Theorem~8.2 a declaration needs about $80$~KB of memory per product of terms in its identities, so the generator cuts the declarations to at most $8\cdot10^4$ products each, counted in advance. A different problem arises when the kernel checks the soundness proofs, in which the functions of the checker are applied to variables. A definitional unfolding of a conditional over a symbolic argument can send the kernel into the well-founded recursion behind \texttt{Nat.div} and \texttt{Nat.mod}, where the check ends in deep recursion. We avoid this by rewriting with equation lemmas before such a step. \subsection{Statements of certificate formats}\label{ss:formats} The hypotheses of a soundness theorem, which states what a certificate format proves, must exclude degenerate data. To show that these hypotheses are needed, we prove in the development that several soundness statements without them are false. For example, a lifting lemma for polynomial systems modulo a prime needs all polynomials in the system to be nonzero, since a zero polynomial makes one of its hypotheses vacuous (\lean{not_LiftingLemma_noP9}, \file{Core/K14/Counter.lean}). A certificate that identifies a root of an eliminant with a known point must check that the coordinate of the point is that root, not only that it lies in the isolating box of the root (\lean{not_ZeroCert_sound}, \file{Core/ResidualCert/Counter.lean}). Similarly, the replay of a tree that defers subtrees to other declarations is sound only if the deferred boxes are nondegenerate (\lean{checkTree_sound_as_requested_is_false}, \file{Core/E3/Replay.lean}). All statements used in the proof carry these hypotheses. \section{Independent kernels}\label{sec:kernels} \begin{table}[tp] \caption[]{The checks of the formal proof and their costs. Unless its row says otherwise, a check was run at a commit at which the Lean files of the library are those of the release.}\label{tab:checks} \centering \footnotesize \scriptsize \begin{tabular}{@{}>{\raggedright}p{0.40\textwidth}>{\raggedright}p{0.33\textwidth}>{\raggedright\arraybackslash}p{0.21\textwidth}@{}} \toprule check & result & cost\\ \midrule keyword scan of \file{CC5Full.lean} and \file{CC5Full/}, generated modules included & none of \texttt{sorry}, \texttt{admit}, \texttt{axiom}, \texttt{native\_decide}, \texttt{implemented\_by}, \texttt{extern}, \texttt{ofReduceBool}, \texttt{unsafe} in $90{,}136$ files & 9 s\\ \addlinespace search for the option \texttt{debug.skipKernelTC} in the archives listed in \S\ref{sec:availability}, which hold the project at \texttt{52858e1} and the four families & no occurrence & --\\ \addlinespace regeneration of the four families of Table~\ref{tab:families} and of the generated modules stored in \file{Core/GPts} & byte-identical to the hash lists and to the stored modules & 22.61 CPU-h for the branch and bound\\ \addlinespace regeneration, and build of all project modules by Lean's kernel, Mathlib prebuilt, in the first run of \S\ref{sec:repro}, at a commit that differs from the release in three Lean files of the library & all targets built & about 863 CPU-h; 2.34 h of wall-clock time\\ \addlinespace rebuild of these three files and of the $794$ modules that import them, in the second run & all targets up to date & 2.97 CPU-h for the $748$ built on the cluster\\ \addlinespace closure of \lean{MainTheorem_holds} exported from that build, against the state checked by the kernels & byte-identical, $7{,}410{,}727{,}737$ bytes & 0.82 CPU-h\\ \addlinespace kernel counts of the $44$ jobs of the branch and bound, against the zeros in region $k$ recorded in their logs in \cite{Tom26b} & equal & --\\ \addlinespace \texttt{\#print axioms} of \lean{MainTheorem_holds}, and the $29$ runs of the axioms scripts & \texttt{propext}, \texttt{Classical.choice}, \texttt{Quot.sound} only & 14 s for \texttt{\#print axioms}\\ \addlinespace part A, Lean's kernel (\texttt{leanchecker}) & accepted & 1,493 CPU-s\\ \addlinespace part A, nanoda & accepted & 546 CPU-s\\ \addlinespace part A, lean4lean & accepted & 1,853 CPU-s\\ \addlinespace part B, nanoda (\S\ref{ss:method}) & all $6{,}731$ exports accepted & 575.4 CPU-h at an earlier commit\\ \addlinespace part B, lean4lean (\S\ref{ss:method}) & all $6{,}731$ exports accepted, $36$ of them with ten times the default fuel & 980.2 CPU-h at an earlier commit\\ \addlinespace glue; cross-check against lean4export & no problem & 18 s; 16 s\\ \addlinespace control: one certificate claims \texttt{false} & rejected by both kernels; the glue reports exactly that declaration & 145 s\\ \bottomrule \end{tabular} \end{table} The certificates rely on evaluation by the kernel far more than ordinary proofs do. We therefore checked the closure of \lean{MainTheorem_holds} again with two independent Lean kernels: nanoda~0.4.17 \cite{nanoda}, and lean4lean \cite{Car24} in export mode, both in the versions shipped with the toolchain. Table~\ref{tab:checks} collects the results. \subsection{Method}\label{ss:method} Evaluating the certificates dominates the cost of the check, which in one process would take weeks. We therefore split the check into parts that run in parallel. Part~A is the closure with the $680{,}112$ certificate theorems replaced by assumptions with the same names and types, an export of $7.0$~GB. Part~B consists of the certificate theorems with their full closures on the three standard axioms, grouped by modules into $6{,}731$ exports of $54.8$~GB in all. We ran part~B at an earlier commit. Ten of its exports have closures that differ from those of the released library, and we ran these ten again on the released library. A Python script, the glue, then checks that part~A assumes exactly the certificate theorems and the three axioms, that part~B proves the certificate theorems with the types assumed in part~A, that the declarations shared by the parts are identical, and that the exports of part~B agree with each other and declare no other axioms. Here declarations are compared by SHA-256 hashes of a canonical form. A cross-check compares our exports, written by \file{tools/kernel2/kexport3}, with those written by the toolchain's exporter lean4export \cite{lean4export}. As a control, we changed one certificate in one export to claim \texttt{false} instead of \texttt{true}. Both kernels rejected the changed export, and the glue reported exactly that declaration. Both kernels accepted the closure. lean4lean bounds its reduction loops by a configurable fuel and reports running out of fuel as a timeout, not as an error in the proof. With the default fuel it stopped on $36$ of the $6{,}731$ exports of part~B. With ten times the default it accepted all of them. \subsection{An issue in nanoda}\label{ss:nanoda} With the decision procedure derived by Lean for the structure \texttt{Rat}, nanoda~0.4.17 overflows its stack on four certificate theorems of two of our checkers, \lean{IdentData.check} and \lean{Sep.eqCert}, for the curve families of \cite[\S9]{Tom26a}. Evaluating this procedure makes the kernel compare the unevaluated numerators and denominators on the two sides. These are different expressions with the same value. They contain proofs of divisibility facts from the normalization of fractions. When two proofs of propositions that are not definitionally equal meet, Lean's kernel and lean4lean conclude at once that the proofs are not equal. nanoda instead goes on to unfold the proofs, down to the well-founded recursion of \texttt{Nat.gcd.induction} on numbers of $20$ to $37$ digits. A product of two fractions with $22$-digit numerators over $2^{100}$, compared by \texttt{decide +kernel}, reproduces the overflow in a few lines of core Lean (\file{CC5Full/Core/scripts/kernel2/diag/}). This is why the two checkers of \S\ref{ss:arith} use \texttt{qeqb a b := a.num == b.num \&\& a.den == b.den}, with \lean{qeqb_iff}. With this comparison, nanoda accepts all certificate theorems. \section{Reproduction}\label{sec:repro} The supplementary material \cite{Tom26b} holds the source of the project at the released commit \texttt{52858e1} and the four families of generated modules (\S\ref{sec:availability}). In the file \file{README.md} of the project, the commands are given at three levels: \file{check.sh}, which scans the sources for forbidden keywords, builds the default target and prints the axioms of $29$ theorems; the theory; and Theorem~\ref{thm:main} with the generated families. We reproduced the build in two runs from fresh copies of the sources, with Mathlib and the other packages prebuilt, on a main machine with at most $16$ Lean processes and on a cluster of machines. The first run, of a commit that differs from the release in three Lean files of the library, regenerated the families and built all project modules from source. The second run, of the released library, compiled from source only these three files and the $794$ modules that import them, and took the build products of the other modules from a separate build of the first run's commit. Each run also executed the axioms scripts ($29$ runs) and \texttt{\#print axioms CC5Full.Core.Compose.MainTheorem\_holds} from a new file, which printed \texttt{[propext, Classical.choice, Quot.sound]}. Table~\ref{tab:checks} lists the checks with their costs. The file \file{README_records.md}, which accompanies this paper, gives the commit at which each check ran, the records of the project from which we take our figures, and further details of the two runs and of the deposited archive. \section{Discussion}\label{sec:discussion} \subsection{Comparison with other formal proofs} Several formal proofs check large computations. Gonthier's proof of the four colour theorem in Coq \cite{Gon08} runs its case analysis by reflection in the evaluator of the proof assistant. In the formal proof of the Kepler conjecture \cite{HAB17}, which combines HOL Light and Isabelle, the verification of more than $23{,}000$ nonlinear inequalities took about $5000$ processor-hours. Immler \cite{Imm18} verified the computer-assisted part of Tucker's proof \cite{Tuc02} that the Lorenz attractor exists, Smale's fourteenth problem, with an ODE solver verified in Isabelle/HOL. Proofs of numerical bounds by computation inside a proof assistant include Melquiond's work in Coq \cite{Mel08,MDM16}. Solovyev and Hales verified the nonlinear inequalities of the Kepler proof with Taylor intervals in HOL Light \cite{SH13}. In SAT-based proofs in combinatorics, such as that of the Boolean Pythagorean triples theorem \cite{HKM16}, an untrusted solver produces a proof that a small checker validates. For the empty hexagon theorem, the encoding was verified in Lean \cite{SNG24}. The uniqueness proof for convex four-body central configurations in \cite{Tom26c} is also formalized in Lean, with its branch and bound checked by the kernel, on a much smaller computation. Like the formal proof of the Kepler conjecture, our development formalizes the mathematical framework of its computations, here the theory of \cite{AK12} at places, together with the computations. All of its computations are evaluated by the Lean kernel itself, without compiled code or any checker outside the proof assistant, at the cost of a build of about $863$ CPU-hours. The certificates are of several kinds at once: exact algebra over $\Q$ and modulo primes, ball and interval arithmetic, linear algebra, and positivity on cones. \subsection{Concluding remarks} Two observations may be useful for other proofs by reflection of this size. First, the cost of evaluation by the kernel depends on how a checker is written and on how the certificates are cut into declarations (\S\ref{ss:kernelstyle}). Second, an independent kernel may fail on declarations that Lean's kernel accepts: nanoda failed on four certificate theorems of two of our checkers until these compared rationals by their numerators and denominators (\S\ref{ss:nanoda}). Among the points that stay outside the formal proof (\S\ref{ss:notstated}) are the version of Theorem~\ref{thm:main} without reflections, which follows from the formal one by the argument of \S\ref{ss:conv}(e), and the identification of the counts of the branch and bound with numbers of central configurations. \section{Availability}\label{sec:availability} The formalization is part of the supplementary material of \Tom, deposited on Zenodo \cite{Tom26b} (\url{https://doi.org/10.5281/zenodo.23202861}). The archive \file{cc50-rung2-lean_full.tar.xz} holds \texttt{git archive} of commit \texttt{52858e1c7e831f226c306d7b3bdf8d02c16f38da} of the project, without build products and without the generated families, and with three docstring phrases reworded in two files. The generated families are in four archives, which unpack at the root of the project: \begin{itemize}[leftmargin=*] \item \file{cc50-rung2-lean_full-E3-Run-modules.tar.xz}, SHA-256\newline \texttt{b490708b\allowbreak aaffd932\allowbreak 08a3ef1c\allowbreak 0adb0b1a\allowbreak 3ed9869d\allowbreak 1c0df43e\allowbreak 94233455\allowbreak ac49ac68}; \item \file{cc50-rung2-lean_full-strata-F1_2_3_4_5-modules.tar.xz}, SHA-256\newline \texttt{ae4af072\allowbreak 8b757a85\allowbreak e31c2907\allowbreak e5025686\allowbreak d2d8e571\allowbreak 06440efe\allowbreak 8c8addbe\allowbreak d34fc1e1}; \item \file{cc50-rung2-lean_full-ResidualCert-All-modules.tar.xz}, SHA-256\newline \texttt{ba1f6676\allowbreak 99944838\allowbreak e7b959b5\allowbreak f13e5595\allowbreak 867e5a8a\allowbreak 1dbb1df0\allowbreak 1c8ab6f4\allowbreak 2b8a596c}; \item \file{cc50-rung2-lean_full-D14a-B-modules.tar.xz}, SHA-256\newline \texttt{211cb529\allowbreak c6ab8c12\allowbreak 2681206e\allowbreak 6ead8c69\allowbreak 635ff72e\allowbreak ffc564fe\allowbreak 5d6a9881\allowbreak 24461f1e}. \end{itemize} The toolchain is \texttt{leanprover/lean4:v4.35.0-rc3}. The file \file{lake-manifest.json} pins Mathlib at commit \texttt{c55e6e786f49471c72fbddbec5415808896aec1e}. \section*{Acknowledgements} Generative AI tools were used to write code, run analyses and draft text; the author directed the work and takes full responsibility for its content. \section*{Funding} This work received no external funding. \begin{thebibliography}{99} \bibitem{AK12} A.~Albouy and V.~Kaloshin, \emph{Finiteness of central configurations of five bodies in the plane}, Ann. of Math. (2) \textbf{176} (2012), 535--588. \bibitem{BB02} H.~Barendregt and E.~Barendsen, \emph{Autarkic computations in formal proofs}, J. Automat. Reason. \textbf{28} (2002), 321--336. \bibitem{BCH26} A.~Bastounis, F.~Circelli and A.~C.~Hansen, \emph{Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs}, arXiv:2610.08144 (2026). \bibitem{Bou97} S.~Boutin, \emph{Using reflection to build efficient and certified decision procedures}, in: Theoretical Aspects of Computer Software (TACS 1997), Lecture Notes in Comput. Sci. \textbf{1281}, Springer, 1997, 515--529. \bibitem{Car24} M.~Carneiro, \emph{Lean4Lean: Verifying a typechecker for Lean, in Lean}, arXiv:2403.14064v3 (2025). \bibitem{CT26} Z.~Chen and Z.~Tong, \emph{Finiteness of planar central configurations of five bodies for all positive masses: On Smale's sixth problem}, arXiv:2610.16107 (2026). \bibitem{DGPS} W.~Decker, G.-M.~Greuel, G.~Pfister and H.~Sch\"onemann, \emph{Singular 4-4-1 --- A computer algebra system for polynomial computations}, \url{https://www.singular.uni-kl.de} (2025). \bibitem{dMU21} L.~de~Moura and S.~Ullrich, \emph{The Lean~4 theorem prover and programming language}, in: Automated Deduction (CADE 28), Lecture Notes in Comput. Sci. \textbf{12699}, Springer, 2021, 625--635. \bibitem{Gon08} G.~Gonthier, \emph{Formal proof---the four-color theorem}, Notices Amer. Math. Soc. \textbf{55} (2008), 1382--1393. \bibitem{HAB17} T.~Hales, M.~Adams, G.~Bauer, T.~D.~Dang, J.~Harrison, L.~T.~Hoang, C.~Kaliszyk, V.~Magron, S.~McLaughlin, T.~T.~Nguyen, Q.~T.~Nguyen, T.~Nipkow, S.~Obua, J.~Pleso, J.~Rute, A.~Solovyev, T.~H.~A.~Ta, N.~T.~Tran, T.~D.~Trieu, J.~Urban, K.~Vu and R.~Zumkeller, \emph{A formal proof of the Kepler conjecture}, Forum Math. Pi \textbf{5} (2017), e2. \bibitem{HM06} M.~Hampton and R.~Moeckel, \emph{Finiteness of relative equilibria of the four-body problem}, Invent. Math. \textbf{163} (2006), 289--312. \bibitem{HKM16} M.~J.~H.~Heule, O.~Kullmann and V.~W.~Marek, \emph{Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer}, in: Theory and Applications of Satisfiability Testing (SAT 2016), Lecture Notes in Comput. Sci. \textbf{9710}, Springer, 2016, 228--245. \bibitem{Imm18} F.~Immler, \emph{A verified ODE solver and the Lorenz attractor}, J. Automat. Reason. \textbf{61} (2018), 73--111. \bibitem{Kra69} R.~Krawczyk, \emph{Newton-Algorithmen zur Bestimmung von Nullstellen mit Fehlerschranken}, Computing \textbf{4} (1969), 187--201. \bibitem{lean4export} lean4export, an exporter of Lean~4 environments, version 3.1.0, \url{https://github.com/leanprover/lean4export}. \bibitem{MDM16} \'E.~Martin-Dorel and G.~Melquiond, \emph{Proving tight bounds on univariate expressions with elementary functions in Coq}, J. Automat. Reason. \textbf{57} (2016), 187--217. \bibitem{mC20} The mathlib Community, \emph{The Lean mathematical library}, in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020, 367--381. \bibitem{Mel08} G.~Melquiond, \emph{Proving bounds on real-valued functions with computations}, in: Automated Reasoning (IJCAR 2008), Lecture Notes in Comput. Sci. \textbf{5195}, Springer, 2008, 2--17. \bibitem{Moo77} R.~E.~Moore, \emph{A test for existence of solutions to nonlinear systems}, SIAM J. Numer. Anal. \textbf{14} (1977), 611--615. \bibitem{nanoda} nanoda, a type checker for Lean~4, version 0.4.17, \url{https://github.com/ammkrn/nanoda_lib}. \bibitem{Sma98} S.~Smale, \emph{Mathematical problems for the next century}, Math. Intelligencer \textbf{20} (1998), no.~2, 7--15. \bibitem{SH13} A.~Solovyev and T.~C.~Hales, \emph{Formal verification of nonlinear inequalities with Taylor interval approximations}, in: NASA Formal Methods (NFM 2013), Lecture Notes in Comput. Sci. \textbf{7871}, Springer, 2013, 383--397. \bibitem{SNG24} B.~Subercaseaux, W.~Nawrocki, J.~Gallicchio, C.~Codel, M.~Carneiro and M.~J.~H.~Heule, \emph{Formal verification of the empty hexagon number}, in: 15th International Conference on Interactive Theorem Proving (ITP 2024), LIPIcs \textbf{309}, 2024, 35:1--35:19. \bibitem{Tom26a} T.~S.~Tomar, \emph{Smale's sixth problem for five bodies in the plane, with a proof formalized in Lean}, version~2, Zenodo (2026), \url{https://doi.org/10.5281/zenodo.23406010}; version~1: arXiv:2610.13100 (2026), titled \emph{Finiteness of planar central configurations of five bodies for all positive masses}. \bibitem{Tom26b} T.~S.~Tomar, \emph{Supplementary material for ``Smale's sixth problem for five bodies in the plane, with a proof formalized in Lean''}, Zenodo (2026), \url{https://doi.org/10.5281/zenodo.23202861}. \bibitem{Tom26c} T.~S.~Tomar, \emph{Uniqueness of four-body convex central configurations for all masses}, arXiv:2609.35632 (2026). \bibitem{Tuc02} W.~Tucker, \emph{A rigorous ODE solver and Smale's 14th problem}, Found. Comput. Math. \textbf{2} (2002), 53--117. \end{thebibliography} \end{document}