\section{Introduction}\label{sec:intro}

A configuration $q=(q_1,\dots,q_n)$ of $n$ distinct points in the plane, carrying 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 the homographic solutions of the $n$-body problem, and in particular of its relative equilibria \cite{Moe14}. A configuration similar to a central configuration is again one. Smale's sixth problem \cite{Sma98} (Problem~9 of \cite{ACS12}) asks whether, for every choice of positive masses, the number of central configurations up to similarity is finite.

For $n=3$ there are five, the two equilateral triangles of Lagrange and the three collinear configurations of Euler. Moulton \cite{Mou10} counted the collinear central configurations for all $n$. Hampton and Moeckel \cite{HM06} proved finiteness for four bodies and all positive masses, and Albouy and Kaloshin \cite{AK12} for five bodies in the plane when the masses lie outside a closed algebraic subset of codimension two of the mass space. Jensen and Leykin \cite{JL25} gave a tropical method for generic masses and completed its computation for $n\le5$. Moczurad and Zgliczy\'nski \cite{MZ26} counted the central configurations at several mass vectors of the exceptional set of \cite{AK12}. For five bodies, finiteness for all positive masses was proved in \cite{Tom26}. Chen and Tong \cite{CT26} state the same theorem and give a different proof.

For six bodies, Moczurad and Zgliczy\'nski counted the planar central configurations of equal masses with a computer-assisted proof \cite{MZ19}. The prevariety of Jensen and Leykin, computed for one choice of mass valuations, had recession cones that were not all pointed \cite[\S4.3]{JL25}. Chang and Chen \cite{CC23,CC24,CC25} mechanized the method of \cite{AK12} for six bodies. Their first algorithm reduces the problem to $117$ diagrams, their second excludes $31$ of them, and their third excludes one more at all positive masses and $61$ others outside explicit hypersurfaces of masses. They left $24$ diagrams unresolved, together with the question of a dominant polynomial bounded on all of them \cite[\S11, pp.~54--55]{CC23}. Aquino-Michaels \cite{AM26} then excluded four of the $24$ diagrams (numbers $52$, $63$, $65$ and $67$) for masses outside proper algebraic subsets, excluded diagram~$6$ on components that come from real configurations, and reduced the remaining question to $11$ diagrams. Our main result is the following.

\begin{theorem}\label{thm:main}
There is a nonzero polynomial $F\in\Z[m_1,\dots,m_6]$ with the following property. For every $m\in(\R_{>0})^6$ with $F(m)\ne0$, the planar six-body problem with masses $m$ has finitely many central configurations up to similarity.
\end{theorem}

The proof produces $F$ as a product of finitely many nonzero polynomials, most of which are known only to exist, so we do not compute $F$ and describe its zero set only in part. This zero set contains every mass vector at which the polynomial $P_{93}$ of Theorem~\ref{thm:d93} vanishes at the masses of three of the bodies, in particular every mass vector in which three masses are equal (Remark~\ref{rem:P98set}), and every mass vector in which one mass is the sum of two others (Remark~\ref{rem:BEsums}). Theorem~\ref{thm:main} says nothing about such masses, among them six equal masses. Finiteness for all positive masses remains open.

\subsection*{The method}
We use the framework of \cite{AK12} in the form of \cite{Tom26}. If there are infinitely many central configurations, the complex solutions of the normalized equations contain an irreducible curve $C$ on which the potential $U$ is a nonzero constant and some mutual distance is not constant. At each singular place $P$ at infinity of $C$ the exponents $x_{kl}(P)$ of the mutual distances form the \emph{type} $x(P)\in\Q^{15}$, and the types balance: $\sum_Pd_P\,x(P)=0$ with $d_P>0$, the sum running over the singular places, of which there is at least one. Summing the fifteen coordinates shows that some singular place has $\ell(x(P))=\sum_{k<l}x_{kl}(P)\le0$ (Corollary~\ref{cor:sum}), that is, the product $\Delta=\prod_{k<l}r_{kl}^2$ of the squared distances does not tend to zero there. It therefore suffices to show that at generic masses no singular place has $\ell(x(P))\le0$. This single inequality already disposes of eleven of the $24$ diagrams that Chang and Chen left open (Section~\ref{sec:exclusion}). The unit $\Delta$, or its inverse, is also used in \cite[Thms.~6.1 and~6.3]{AM26} and in the global argument of \cite[\S4]{CT26} for five bodies.

The exponents at a singular place are constrained by combinatorial data: the diagram of the place in the sense of \cite{AK12}, the way the six bodies and the centre of mass cluster, recorded by two ultrametric trees of the exponents, and the terms of least exponent in the equations of the bodies and in two identities for $U$. These data take one of finitely many values, the \emph{cells}, and each cell confines the exponents to a relatively open polyhedron. We enumerate the cells whose polyhedron meets the half-space $\ell\le0$, for every diagram allowed by the rules of \cite[\S3]{AK12} that we use (Sections~\ref{sec:diagrams} and~\ref{sec:cells}), and exclude all but $43$ of them at generic masses (Section~\ref{sec:exclusion}). In most of the excluded cells an identity has a single term of least exponent, which cannot happen at a place. In the others the leading coefficients satisfy equations that are inconsistent over the field of rational functions of the masses (in some cells after one mass is set to $1$), as Gr\"obner bases show, so the cell can occur only where a nonzero polynomial in the masses vanishes.

The $43$ remaining cells lie in seven diagrams, which we treat at the level of places (Sections~\ref{sec:ak50} and~\ref{sec:k4}). In five of them two clusters of bodies decouple at leading order, and the torque of one cluster, as in \cite[\S5.0]{AK12} and with a rewriting from \cite[\S8.6]{AK12} where needed, either excludes the diagram or gives a condition on the leading configurations of the clusters. These are complex central configurations of three or four bodies, or solutions of a related four-body system, and they are finite in number up to rotation at generic masses; the condition fails at one mass point and is therefore a nonzero polynomial condition on the masses. In the other two diagrams the cluster is a complete graph of $z$-strokes on four bodies, and its leading system must have a solution. For one diagram it is the system $E_4$ of complex equilibria of four bodies in both colours, whose mass condition Albouy and Kaloshin mention \cite[\S5.5]{AK12} and which Aquino-Michaels showed to have no solution outside a proper algebraic subset of masses, where he meets it as the core of diagrams $63$, $65$ and $67$ \cite[Thm.~5.6]{AM26}; for the two diagrams treated here he confined only the collinear case \cite[Rem.~5.7]{AM26}. As far as we know, the observation that $E_4$ is a leading system here is new, and for the other diagram the leading system is a new system $C_4$ of a four-body cluster with a centre. We show that neither system has a solution outside a proper algebraic subset of masses, for $E_4$ by hand, up to resultants of integer polynomials, and for $C_4$ by a certified computation at one mass point.

Every linear program found infeasible has a certificate of infeasibility checked in exact rational arithmetic, and each cell excluded by Gr\"obner bases also has an explicit identity with integer polynomials that gives the hypothesis of Lemma~\ref{lem:core}. Section~\ref{sec:verification} describes the computations, their checks and the formal proof in Lean~4 with Mathlib, which follows Sections~\ref{sec:setup}--\ref{sec:proof} with a few departures.

\subsection*{Organization}
Section~\ref{sec:setup} sets up the equations, the curves and their places, and proves the rules of \cite{AK12} at places. Sections~\ref{sec:diagrams}--\ref{sec:exclusion} enumerate the diagrams and the cells and exclude the cells at generic masses, Sections~\ref{sec:ak50} and~\ref{sec:k4} treat the seven diagrams, numbered $64$, $66$, $88$, $89$, $93$, $94$ and $98$ in \cite{CC23}, and Section~\ref{sec:proof} proves Theorem~\ref{thm:main}. Section~\ref{sec:hand} explains the exclusion of most cells by lemmas proved by hand, independently of the computations by which Section~\ref{sec:exclusion} excludes them. Theorem~\ref{thm:main} needs neither that section nor the treatment of diagrams $81$, $82$ and $90$ in Section~\ref{sec:ak50}, so a reader may skip both. Section~\ref{sec:verification} describes the verification.