\documentclass[11pt]{amsart}
\pdfsuppressptexinfo=-1
\usepackage[margin=1.1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{booktabs,enumitem,array,alltt,upquote}
\usepackage{tikz}
\usepackage[hidelinks]{hyperref}
\hypersetup{pdftitle={Smale's sixth problem for six bodies in the plane: finiteness of central configurations for generic masses, with a proof formalized in Lean},
  pdfauthor={Tejasvi Singh Tomar}}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}
\numberwithin{equation}{section}
\setlength{\emergencystretch}{2em}
\raggedbottom

\newcommand{\R}{\mathbb{R}}
\newcommand{\C}{\mathbb{C}}
\newcommand{\Q}{\mathbb{Q}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\F}{\mathbb{F}}
\newcommand{\cZ}{\mathcal{Z}}
\newcommand{\cW}{\mathcal{W}}
\newcommand{\cN}{\mathcal{N}}
\newcommand{\cO}{\mathcal{O}}
\newcommand{\val}{\operatorname{val}}
\newcommand{\Res}{\operatorname{Res}}
\newcommand{\rank}{\operatorname{rank}}
\newcommand{\meet}{\operatorname{meet}}
\newcommand{\lean}[1]{\nolinkurl{#1}}
\newcommand{\lc}[2]{[#1]_{#2}}
\newcommand{\cert}{\ensuremath{^{\dagger}}}
\newcommand{\repocommit}{\texttt{84bbcf276d029fdf31375c4a21c6a7e136955e51}}

\begin{document}

\title[Smale's sixth problem for six bodies]{Smale's sixth problem for six bodies in the plane:\\ finiteness of central configurations for generic masses,\\ with a proof formalized in Lean}
\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]{70F10, 70F15, 14Q20, 65G40, 68V20}
\keywords{Central configurations, relative equilibria, six-body problem, Smale's sixth problem, valuations, Gr\"obner bases, interval arithmetic, Lean}

\input{sec/abstract}

\maketitle
\enlargethispage{2pt}

\input{sec/s1_intro}
\input{sec/s2_setup}
\input{sec/s3_diagrams}
\input{sec/s4_cells}
\input{sec/s5_exclusion}
\input{sec/s6_ak50}
\input{sec/s7_k4}
\input{sec/s8_proof}
\input{sec/s_hand}
\input{sec/s9_verification}

\section*{Data availability}
The supplementary material, with the programs, the Lean projects, the certificates, the data and the logs, is available at \url{https://doi.org/10.5281/zenodo.23472605}. The programs are also in the repository \url{https://github.com/tejasvi/smale6-six-bodies-generic}, at commit \repocommit. The DOIs \url{https://doi.org/10.5281/zenodo.23433406} (paper) and \url{https://doi.org/10.5281/zenodo.23433409} (supplementary material) refer to all versions and resolve to the latest one.

\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.

\input{sec/refs}

\end{document}