% =====================================================================
\section{The feasible world: bounded arithmetic, TFNP and proof systems}\label{sec:feasible}
% =====================================================================

Second-order arithmetic measures infinitary content. For finite optimization problems the right yardstick is
complexity, and the logical counterpart is bounded arithmetic, where Cook's program of \emph{bounded reverse
mathematics} pairs complexity classes with weak theories and propositional proof systems
\cite{CN10,Ngu08}. The correspondences in this section are tighter than in second-order arithmetic: they identify
classes of search problems with exactly the existence principles that a theory can prove.

\subsection{Local optimality is the strength of \texorpdfstring{$T^1_2$}{T12}}\label{subsec:pls}

A local search problem asks for a local optimum of a cost function over a neighbourhood structure, both given by
polynomial-time algorithms. Johnson, Papadimitriou and Yannakakis \cite{JPY88} collected these problems into the
class $\PLS$. The principle ``every finite optimization problem has a local optimum'' is a $\forall\Sigma^b_1$
statement provable in Buss's theory $T^1_2$, which has induction for $\NP$ properties, and Buss and Kraj\'i\v{c}ek
proved the converse: the $\Sigma^b_1$-definable multifunctions of $T^1_2$ are exactly the projections of $\PLS$
problems \cite{BK94}; equivalently, the $\NP$ search problems provably total in $T^1_2$ are exactly those reducible
to $\PLS$. Beckmann and Buss extended this up the hierarchy, characterizing, for $1\le i\le k+1$, the
$\Sigma^b_i$-definable multifunctions of $T^{k+1}_2$ by local search over $\Pi^p_k$-definable feasible sets
\cite{BB09}, and
Ko\l{}odziejczyk, Nguyen and Thapen characterized the $\NP$ search problems provably total in the weak second-order
theory $V^1_2$ by an exponentially blown-up local improvement principle \cite{KNT11}. In this precise sense, \emph{local optimality is the
existence principle of $T^1_2$}, just as compactness is the existence principle of $\WKL$. A global optimum, by
contrast, cannot in general be recognized in polynomial time, so, unless $\mathsf P=\NP$, finding one is not an $\NP$
search problem.

Feasible versions of real analysis exist as well. Ferreira's theory $\mathsf{BTFA}$ and its extension by a form of
weak K\H{o}nig's lemma for trees given by bounded formulas have the polynomial-time functions as their provably total
functions \cite{Fer94}, and $\mathsf{BTFA}$ proves the intermediate value theorem, so that its real numbers form a
real closed field \cite{FF02}.

\subsection{Continuous local search and gradient descent}\label{subsec:cls}

The continuous analogue of $\PLS$ is the class $\CLS$ of Daskalakis and Papadimitriou \cite{DP11}, designed to
capture problems solvable by gradient-type local improvement, such as finding stationary points of smooth
functions. Fearnley, Goldberg, Hollender and Savani proved that $\CLS=\PPAD\cap\PLS$, and that finding an
$\eps$-KKT point of a $C^1$ function with Lipschitz gradient on $[0,1]^2$, given by arithmetic circuits, is complete
for this class, as are the problems of finding approximate fixed points of gradient descent
\cite[Theorems 5.1 and 6.1]{FGHS21}. Even KKT points of quadratic programs over $[0,1]^n$ are $\CLS$-complete
\cite{FGHS24}. Two neighbouring results calibrate the surroundings: approximate local min-max points of
nonconvex--nonconcave smooth functions on polytopes are $\PPAD$-complete \cite{DSZ21}, like Brouwer fixed points and
Nash equilibria \cite{Pap94,DGP09,CDT09}; and approximate second-order stationary points are $\PLS$-complete on the
square according to a recent preprint \cite{KPP26}.

The finite and the computable worlds agree in dimension one, where KKT points are found by bisection on the
derivative. In the computable world the analogue of the KKT problem is exact rather than approximate, and in dimension
one it is as easy as finding a zero:
$\KKT_1\seqv\IVT$ (\cref{prop:kkt1}). Whether the exact KKT problem stays strictly below the Brouwer problem in higher
dimensions, as $\CLS$ is believed to stay strictly below $\PPAD$, is \cref{prob:kkt}.

\subsection{Proof systems as optimization methods}\label{subsec:proofsystems}

Most classical $\TFNP$ classes now have characterizations by propositional proof systems in the black-box (query)
model, the main exceptions being $\mathsf{PPP}$ and $\mathsf{UEOPL}$: $\PLS$ corresponds to Resolution (of
polylogarithmic width), $\PPA$ to Nullstellensatz over $\mathbb F_2$, $\PPAD$ to unary Nullstellensatz, $\PPADS$ to
unary Sherali--Adams, and $\mathsf{EOPL}=\PLS\cap\PPAD$ to Reversible Resolution with Terminals, whose power is that of
Resolution and unary Nullstellensatz together \cite{GHJMPRT22,GHJMPRT-CCC22,BKT14,GKRS19}. Since gradient descent is
complete for $\CLS=\PLS\cap\PPAD$ in the white-box model \cite{FGHS21}, Reversible Resolution with Terminals is the
natural proof-system counterpart of gradient descent, with the caveat that the two results live in different models.
In the other direction, optimization algorithms \emph{are} proof systems:
\begin{itemize}[nosep,leftmargin=1.5em]
\item \emph{Cutting planes.} Chv\'atal's closure of a polytope under rounded linear combinations \cite{Chv73} is a
proof system for integer infeasibility \cite{CCT87}. Pudl\'ak proved exponential lower bounds for it by
interpolation with monotone real circuits \cite{Pud97}.
\item \emph{Branch and cut.} The Stabbing Planes system formalizes branch-and-cut \cite{BFIKPPR18}. Dadush and Tiwari
showed that Tseitin formulas have quasi-polynomial cutting-plane refutations and bounded the coefficients needed in
branching proofs \cite{DT20}, and Fleming et al.\ proved the first exponential lower bounds for Stabbing Planes with
bounded coefficients \cite{FGIPRTW21}. The proof system that certifies the dominance reasoning of pseudo-Boolean
optimization solvers simulates the quantified propositional proof system $G_1$ \cite{KT24dominance}.
\item \emph{Sum of squares.} The Positivstellensatz proof system of Grigoriev and Vorobjov \cite{GV01} is the proof
system behind the Lasserre and Parrilo hierarchies for polynomial optimization \cite{Las01,Par03}; its degree lower
bounds \cite{Gri01,Sch08} yield integrality gaps for the sum-of-squares hierarchy, and its bit complexity is subtle
\cite{ODo17,RW17,BS14}.
\end{itemize}

The last item closes a circle with \cref{sec:proofmining}. Artin's solution of Hilbert's 17th problem is
non-constructive; Kreisel's analysis of it, which gave primitive recursive degree bounds, is one of the founding
examples of his program of ``unwinding'' proofs, from which proof mining descends, and Daykin gave another
constructive proof. Lombardi, Perrucci and Roy pushed this line to an elementary recursive bound (a tower of five
exponentials) for the Positivstellensatz \cite{LPR20}, explicitly by turning proofs into certificates. Effective
degree bounds for certificates of positivity are the logical side of a question that is central for sum-of-squares
hierarchies: how high a level is needed to certify a given bound.

Finally, weak theories prove the correctness of classical optimization algorithms. Le and Cook formalized in the
polynomial-time theory $\mathsf{VPV}$ Hall's and Berge's theorems, weak duality for weighted bipartite matching, the
min-max characterization of maximum-weight matchings, and a version of the Hungarian algorithm \cite{LC12};
Fern\'andez and Soltys proved K\H{o}nig's min-max theorem, and with it the finite theorems of Menger, Hall and
Dilworth, in a weak theory of linear algebra \cite{FernandezSoltys2013}. We found no formalization of general linear
programming duality in bounded arithmetic; \cref{thm:lp-rca} suggests that a theory able to reason about
determinants, such as those of Soltys and Cook \cite{SoltysCook2004} or of Tzameret and Cook \cite{TC21}, is the
natural candidate.