\documentclass[11pt]{amsart}
\usepackage[margin=1.1in]{geometry}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{graphicx,booktabs,enumitem,longtable}
\usepackage[hidelinks]{hyperref}
\hypersetup{pdftitle={Smale's sixth problem for five bodies in the plane, 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}

%
%
\newif\ifpendingfatal
\ifdefined\PENDINGFATAL\pendingfataltrue\fi
\newcommand{\pending}[1]{\ifpendingfatal\errmessage{PENDING TEXT LEFT IN THE PAPER}\fi\textbf{[PENDING: }#1\textbf{]}}

\newcommand{\R}{\mathbb{R}}
\newcommand{\C}{\mathbb{C}}
\newcommand{\Q}{\mathbb{Q}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\cA}{\mathcal{A}}
\newcommand{\cC}{\mathcal{C}}
\newcommand{\cD}{\mathcal{D}}
\newcommand{\cP}{\mathcal{P}}
\newcommand{\cZ}{\mathcal{Z}}
\newcommand{\cW}{\mathcal{W}}
\newcommand{\cN}{\mathcal{N}}
\newcommand{\one}{\mathbb{1}}
\newcommand{\jj}{\mathrm{j}}
\newcommand{\val}{\operatorname{val}}
\newcommand{\ord}{\operatorname{ord}}
\newcommand{\Res}{\operatorname{Res}}
\newcommand{\rank}{\operatorname{rank}}
\newcommand{\relint}{\operatorname{relint}}
\newcommand{\conv}{\operatorname{conv}}
\newcommand{\cl}{\operatorname{cl}}
\newcommand{\lab}[1]{\mathsf{#1}}
\newcommand{\pc}[1]{\mathsf{#1}}
\newcommand{\bone}{\mathbf{b}_1}
\newcommand{\btwo}{\mathbf{b}_2}
\newcommand{\hone}{\mathbf{h}_1}
\newcommand{\htwo}{\mathbf{h}_2}
\newcommand{\hthree}{\mathbf{h}_3}
\newcommand{\Vtwo}{V_2}
\newcommand{\VN}{V_N}

\begin{document}

\title[Smale's sixth problem for five bodies in the plane]{Smale's sixth problem for five bodies in the plane,\\ with a proof formalized in Lean}
\author{Tejasvi Singh Tomar}
\address{Independent researcher}
\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}
\keywords{Central configurations, relative equilibria, five-body problem, Smale's sixth problem, singular sequences, Puiseux series, computer-assisted proof}

\input{sec/abstract}

\maketitle

\input{sec/s1_intro}
\input{sec/s2_setup}
\input{sec/s3_types}
\input{sec/s4_lex}
\input{sec/s5_energy}
\input{sec/s5_points}
\input{sec/s6_near}
\input{sec/s8_curves}
\input{sec/s9_rays}
\input{sec/s10_proof}
\input{sec/s11_verification}

\appendix
\input{sec/a_appendix}

\section*{Use of AI tools}
Generative AI tools were used to find and prove the results, to write the programs and the Lean formalization, and to draft the text.

\input{sec/refs}

\end{document}