Optimization

Motivation

Generalized pattern search (GPS) is a class of derivative-free methods for minimizing a function that can only be evaluated, not differentiated. Such objectives arise in engineering design, where one evaluation is an expensive simulation that may fail and return no value at all. The helicopter rotor design problem of Booker et al. is one example: no value was returned for roughly 66% of the trial points (Booker et al., 1999). A method for such problems has to tolerate objectives that are discontinuous or take the value $+\infty$.

Earlier convergence theory for GPS assumed continuous differentiability of the objective on a neighbourhood of the level set. Torczon established it for unconstrained problems (SIAM J. Optim. 7, 1997), and Lewis and Torczon extended it to bound constraints (1999) and to finitely many linear constraints (SIAM J. Optim. 10, 2000). Audet and Dennis (SIAM J. Optim. 13, 2003) replaced these analyses with a single argument. Its conclusions are local and are graded by the smoothness of the objective at the limit point only, through Clarke's generalized directional derivative. That paper is the source of this mission. Its analysis is the basis of the later mesh adaptive direct search (MADS) theory (Audet, Dennis, SIAM J. Optim. 17, 2006).

Setting

The problem is

$$\min_{x\in\Omega} f(x),\qquad f:\mathbb R^n\to\mathbb R\cup\{+\infty\},\qquad \Omega=\{x\in\mathbb R^n:\ell\le Ax\le u\},$$

with $A\in\mathbb R^{m\times n}$ and $\ell\le u$ in $(\mathbb R\cup\{\pm\infty\})^m$. The algorithm works with the barrier function $f_\Omega$, equal to $f$ on $\Omega$ and to $+\infty$ elsewhere.

The algorithm uses a finite set of directions $D=G\bar Z$, the columns $d_j=G\bar z_j$ of the product of a nonsingular $G\in\mathbb R^{n\times n}$ and an integer matrix $\bar Z\in\mathbb Z^{n\times p}$. The directions form a positive spanning set: their nonnegative combinations give all of $\mathbb R^n$. At iteration $k$, with iterate $x_k$ and mesh size parameter $\Delta_k>0$, the mesh is $M_k=\{x_k+\Delta_k Dz: z\in\mathbb Z_+^{p}\}$. A poll set $\{x_k+\Delta_k d: d\in D_k\}$ is drawn from a positive spanning subset $D_k\subseteq D$. Each iteration ends in one of two ways:

1. Improved mesh point. Some $x_{k+1}\in M_k\cap\Omega$ with $f_\Omega(x_{k+1})<f_\Omega(x_k)$ was found, by the free SEARCH step or by the poll. Then $\Delta_{k+1}=\tau^{w_k}\Delta_k$ with $0\le w_k\le w^+$.
2. Mesh local optimizer. $f_\Omega(x_k)\le f_\Omega(x_k+\Delta_k d)$ for every $d\in D_k$. Then $x_{k+1}=x_k$ and $\Delta_{k+1}=\tau^{w_k}\Delta_k$ with $w^-\le w_k\le-1$.

Here $\tau>1$ is rational and $w^-\le-1\le 0\le w^+$ are integers. The assumptions are A1 $f_\Omega(x_0)<\infty$, A2 $A$ is rational, and A3 all iterates lie in a compact set. A refining subsequence is an infinite set of mesh local optimizers $\{x_k\}_{k\in K}$ along which $\Delta_k\to 0$ (Definition 3.5). For $f$ Lipschitz near $\hat x$, Clarke's derivative is

$$f^\circ(\hat x;d)=\limsup_{y\to\hat x,\ t\downarrow 0}\frac{f(y+td)-f(y)}{t}.$$

Formalization targets

Goal: Theorem 3.7

Assume A1–A3. Let $\hat x$ be the limit of a refining subsequence, and let $d\in D$ be a direction polled at a feasible point $x_k+\Delta_k d$ for infinitely many $k$ in the subsequence. If $f$ is Lipschitz near $\hat x$, then

$$f^\circ(\hat x;d)\ \ge\ 0 .$$

Milestones on the way

• Theorem 3.1: the iterates have a limit point, $\lim_k f(x_k)$ exists and dominates $f$ at lower semicontinuity limit points, and all continuity limit points share one value.
• Lemma 3.2: $\min_{u\ne v\in M_k}\|u-v\|\ge\Delta_k/\|G^{-1}\|$ for every norm giving nonzero integer vectors norm at least $1$.
• Lemma 3.3: $\Delta_k\le\Delta_0\tau^{r^+}$ for some positive integer $r^+$.
• Proposition 3.4: $\liminf_{k\to\infty}\Delta_k=0$.
• Theorem 3.6: a convergent refining subsequence exists.

Corollaries

• Theorem 3.9: if $\Omega=\mathbb R^n$ and $f$ is strictly differentiable at $\hat x$, then $\nabla f(\hat x)=0$.
• Theorem 3.14: if the poll sets conform to the boundary of $\Omega$ (Definition 3.13) and $f$ is strictly differentiable at $\hat x$, then $\nabla f(\hat x)^Tw\ge 0$ on the tangent cone $T_\Omega(\hat x)$ and $-\nabla f(\hat x)\in N_\Omega(\hat x)$. So $\hat x$ is a KKT point.

Significance

Theorem 3.7 gives a first-order conclusion at a limit point from a local hypothesis at that point alone. It does not require smoothness elsewhere, finiteness of $f$ elsewhere, or continuity. It turns the heuristic "the method stopped improving on ever finer meshes" into a statement about generalized derivatives. The unconstrained stationarity result (Theorem 3.9) and the linearly constrained KKT result (Theorem 3.14) follow from it, and they recover the Torczon and Lewis–Torczon theorems under weaker smoothness assumptions. The chain Lemma 3.2 → Lemma 3.3 → Proposition 3.4 → Theorem 3.6 shows that the goal's hypothesis is always met. Every run satisfying A1 and A3 has a refining subsequence, which rests on the rationality of $\tau$ and on the integer structure of $D$.

All results in this mission are proved in the source paper. None of them has, to the best of our knowledge, a machine-checked proof. The mission contributes a formal model of the GPS algorithm class as a class of runs, a formal Clarke directional derivative, and checked proofs of the mesh-refinement chain and the main theorem.

Difficulty

Given a refining subsequence, the goal is a comparison of limsups: the poll inequalities give nonnegative difference quotients at the points $(x_k,\Delta_k)$, which converge to $(\hat x,0^+)$. The difficulty lies in two places. First, the objective is extended-valued, and the barrier hides $f$ at infeasible poll points, where the poll inequality $f_\Omega(x_k)\le+\infty$ says nothing. The hypothesis on $d$ has to supply feasibility, and the Lipschitz hypothesis has to supply finiteness near $\hat x$. Second, the existence of refining subsequences is not a compactness argument alone. Coarsening is allowed, so $\Delta_k$ need not decrease, and with an irrational $\tau$ or a direction set that is not an integer lattice image (for instance $D=[-1,+\pi]$ in $\mathbb R$) the meshes can be dense and $\liminf\Delta_k$ can be positive. The lattice argument behind Proposition 3.4 is where the integrality hypotheses are used.

Formalization scope

Points of $\mathbb R^n$ are Fin n → ℝ, $f$ takes values in WithTop ℝ, and the bounds $\ell,u$ are EReal-valued, so $m=0$ gives $\Omega=\mathbb R^n$. The barrier is defined by cases, never by extended addition. Directions are the columns of G * Zbar indexed by Fin p, and $D_k$ is a Finset (Fin p). A GPS run is a structure of sequences $x_k,\Delta_k,D_k,w_k$ and a per-iteration predicate "mesh local optimizer", subject to exactly the two update rules above, $\Delta_0>0$, rational $\tau>1$ and the exponent bounds. The SEARCH step, the choice of $D_k$ and the exponents are left free, since the paper allows any strategy. A subsequence is a strictly increasing map $K:\mathbb N\to\mathbb N$. The Clarke derivative of a real function is an EReal-valued limit superior along $y\to\hat x$, $t\to 0^+$. "$f$ Lipschitz near $\hat x$" means that $f$ agrees near $\hat x$ with a real function Lipschitz there, and the conclusions are stated for every such function. Strict differentiability is the directional notion of Section 3.4 of the paper.

The goal is not trivialized by an empty run class: Theorem 3.6, on the same class, asserts that refining subsequences exist. The mesh-local-optimizer branch requires the complete poll inequality over $D_k$. The Clarke limit superior cannot take a default value. The direction $d$ must be polled at feasible points infinitely often, which is the paper's "$f$ was evaluated".

Contributions welcome: proofs of any milestone, and reusable lemmas on positive spanning sets, lattice points in compact sets, and the Clarke derivative (for instance, that it equals $\nabla f(\hat x)^Td$ under strict differentiability).

Selected references

• C. Audet, J. E. Dennis Jr., Analysis of Generalized Pattern Searches, SIAM J. Optim. 13(3):889–903, 2003. https://doi.org/10.1137/S1052623400378742
• V. Torczon, On the Convergence of Pattern Search Algorithms, SIAM J. Optim. 7(1):1–25, 1997. https://doi.org/10.1137/S1052623493250780
• R. M. Lewis, V. Torczon, Pattern Search Methods for Linearly Constrained Minimization, SIAM J. Optim. 10(3):917–941, 2000. https://doi.org/10.1137/S1052623497331373
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983; reprinted SIAM Classics in Applied Mathematics 5, 1990. https://doi.org/10.1137/1.9781611971309
• A. J. Booker, J. E. Dennis Jr., P. D. Frank, D. B. Serafini, V. Torczon, M. W. Trosset, A rigorous framework for optimization of expensive functions by surrogates, Structural Optimization 17:1–13, 1999. https://doi.org/10.1007/BF01197559
• C. Audet, J. E. Dennis Jr., Mesh Adaptive Direct Search Algorithms for Constrained Optimization, SIAM J. Optim. 17(1):188–217, 2006. https://doi.org/10.1137/040603371

Motivation

Maximizing a submodular set function without constraints contains Max Cut, Max Directed Cut, maximum facility location and several graph and hypergraph cut problems as special cases, and it appears in operations research wherever a value exhibits diminishing returns but is not monotone (profit that combines coverage with a cost, for example). These problems are NP-hard, so the question is which fraction of the optimum an efficient algorithm can guarantee when the function is accessible only through a value oracle that returns $f(S)$ for a queried set $S$.

Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave the first constant-factor approximation algorithms for maximizing a general nonnegative submodular function. The simplest of them returns a uniformly random set and achieves $1/4$ of the optimum; this mission is about the next one, a nonadaptive algorithm: it decides all of its oracle queries before seeing any answer, then computes a set from the answers. Such an algorithm can be run in one round of parallel queries. The paper shows that this restricted access already beats $1/4$ and reaches $1/3$.

Timeline. For Max Directed Cut, a random cut achieves $1/4$. Feige, Mirrokni and Vondrák (FOCS 2007; journal version 2011) proved $1/4$ for a random set and $1/3$ nonadaptively for general nonnegative submodular functions, $1/3$ and $2/5$ by adaptive local search, and that $1/2$ requires exponentially many queries. Buchbinder, Feldman, Naor and Schwartz (FOCS 2012, SIAM J. Comput. 2015) later reached the optimal $1/2$ with a randomized double-greedy algorithm.

Setting

Let $X$ be a finite ground set with $n = |X| \ge 1$ elements. A function $f : 2^X \to \mathbb{R}$ is submodular (Definition 1.1) if

$$f(S \cup T) + f(S \cap T) \le f(S) + f(T) \qquad \text{for all } S, T \subseteq X .$$

Throughout, $f$ is nonnegative, the paper's standing assumption, and $OPT = \max_{S \subseteq X} f(S)$.

For $p \in [0,1]$, $X(p)$ denotes the random subset of $X$ containing each element independently with probability $p$; $R = X(1/2)$ is a uniformly random subset. For a set $A \subseteq X$, $A(p)$ is the analogous random subset of $A$. The averaged marginal value of an element (Definition 2.4) is

$$\omega(x) = \mathbf{E}\big[f(R \cup \{x\}) - f(R \setminus \{x\})\big], \qquad R = X(1/2).$$

Algorithm NA (p. 1139):

1. by random sampling, compute estimates $\tilde\omega(x)$ with $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ for all $x$, with high probability;
2. independently, sample $R = X(1/2)$;
3. with probability $8/9$ return $R$;
4. with probability $1/9$ return $A = \{x \in X : \tilde\omega(x) > 0\}$.

Given the estimates, the expected value NA returns is $\tfrac89\,\mathbf{E}[f(X(1/2))] + \tfrac19 f(A)$.

Formalization targets

Goal: Theorem 2.6 in the explicit form of its proof

For every nonnegative submodular $f$ and every estimate $\tilde\omega$ with $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ for all $x$,

$$\frac89\,\mathbf{E}[f(X(1/2))] + \frac19\, f\big(\{x : \tilde\omega(x) > 0\}\big) \ \ge\ \Big(\frac13 - \frac{4}{9n}\Big)\, OPT .$$

The printed theorem says "at least $(1/3 - o(1))\,OPT$"; the term $4/(9n)$ is what the proof establishes (p. 1140, last display).

Milestones

1. Lemma 2.2: $\mathbf{E}[g(A(p))] \ge (1-p)\,g(\emptyset) + p\,g(A)$ for submodular $g$.
2. Lemma 2.3: $\mathbf{E}[f(A(p) \cup B(q))] \ge (1-p)(1-q) f(\emptyset) + p(1-q) f(A) + (1-p)q f(B) + pq f(A \cup B)$ for independently sampled, possibly overlapping $A, B$.
3. For $B = X \setminus A$ and any $C$: $f(A) + f(B \cap C) + f(B \cup C) \ge f(C)$.
4. If $\omega \le OPT/n^2$ on $B$: $\mathbf{E}[f(R \cup (B \cap C))] \le \mathbf{E}[f(R)] + OPT/(2n)$.
5. $\mathbf{E}[f(R \cup (B \cap C))] \ge \tfrac14 f(B \cap C) + \tfrac14 f(C)$.
6. If $\omega \ge -OPT/n^2$ on $A$ and $B = X \setminus A$: $\mathbf{E}[f(R)] \ge \mathbf{E}[f(R \cap (B \cup C))] - OPT/(2n)$.
7. $\mathbf{E}[f(R \cap (B \cup C))] \ge \tfrac14 f(C) + \tfrac14 f(B \cup C)$.

Milestones 3–7 are the displayed steps of the proof of Theorem 2.6, stated for arbitrary sets where the page's argument does not use the optimality of $C$.

Significance

The theorem shows that nonadaptive access, a fixed batch of polynomially many value queries followed by a computation, suffices for a $1/3$-approximation of unconstrained nonnegative submodular maximization, strictly better than the $1/4$ of any algorithm that must return one of its queried sets (the paper shows $1/4$ is optimal in that class, §4.2). The quantity $\omega$ generalizes the in-degree/out-degree test for Max Directed Cut to arbitrary submodular functions, and Lemmas 2.2 and 2.3 are general sampling inequalities for submodular functions that the paper reuses for its adaptive smooth local search.

Formalizing it produces machine-checked versions of Lemmas 2.2 and 2.3 as statements about exact finite averages, a reusable expectation operator on product-distributed random subsets, and a checked version of the $1/3$ argument with its explicit error term. The result is proved in the paper; to our knowledge none of it has been formalized in a proof assistant.

Difficulty

The two regimes the proof separates, "$A$ is already good" and "one of $f(B \cap C)$, $f(B \cup C)$ is large", must be tied to the value of a uniformly random set, whereas the elements of $A$ and $B$ are chosen from estimated averages, not from the optimal set $C$. The natural attempt, comparing $f(R)$ with $f(C)$ element by element, fails because $f$ is not monotone: adding elements of $C$ to $R$ can decrease the value. The accuracy $OPT/n^2$ of the estimates must also be propagated through a sum over up to $n$ elements, which is where the error term $4/(9n)$ comes from. The sampling lemmas require handling expectations over pairs of independent random subsets of possibly overlapping sets.

Formalization scope

• The ground set is a Fintype X with DecidableEq, assumed Nonempty, so $n = |X| \ge 1$ and the divisions by $n$ and $n^2$ are genuine; sets are Finset X; $f$ is real valued with nonnegativity $\forall S,\ 0 \le f(S)$ as an explicit hypothesis. Lemmas 2.2 and 2.3 are stated for real $f$ with no sign condition, as printed.
• $OPT$ is Finset.univ.sup' _ f, the true maximum over all subsets.
• Every expectation over an independently sampled random set is the exact finite sum $F(x) = \sum_{S} f(S)\prod_{i \in S} x_i \prod_{i \notin S}(1 - x_i)$; $X(1/2)$ is $x \equiv 1/2$. Expectations over two independent samples (Lemma 2.3) are the corresponding iterated sums. Sampling probabilities carry the hypotheses $0 \le p, q \le 1$.
• The goal quantifies over every estimate $\tilde\omega$ satisfying the printed accuracy $|\tilde\omega(x) - \omega(x)| < OPT/n^2$ (strict), with $A = \{x : \tilde\omega(x) > 0\}$ (strict). The "with high probability" of NA's first step is this hypothesis; the sampling estimate that makes it likely (Lemma 2.5, a Chernoff-bound argument) is not part of the goal. When $OPT = 0$ the hypothesis is unsatisfiable, but then $f \equiv 0$ and nothing is lost.
• The left-hand side is exactly the mixture $\tfrac89\,\mathbf{E}[f(X(1/2))] + \tfrac19 f(A)$. A statement with the maximum of the two terms, with exact values $\tilde\omega = \omega$, or with the $o(1)$ replaced by an existential constant or a limit, is a different (and weaker or stronger) theorem and does not close this mission.
• Printed slip corrected: in the second display on p. 1140, the "$=$" before $-|A \setminus C|\,OPT/(2n^2)$ should be "$\ge$"; milestone 6 states the inequality.

Welcome contributions: proofs of Lemmas 2.2 and 2.3 (reusable for mission IV of this series), the identity $\mathbf{E}[f(R \cup \{x\}) - f(R)] = \tfrac12\omega(x)$, and general lemmas about the operator $F$ (splitting a uniform random set along a partition).

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205

Motivation

Many problems in optimization and equilibrium modelling reduce to a system of equations $F(x) = 0$ whose map $F : \mathbb R^n \to \mathbb R^n$ is Lipschitz but not differentiable: reformulations of nonlinear complementarity problems through the componentwise minimum or the Fischer–Burmeister function, Karush–Kuhn–Tucker systems of constrained programs, and gradients of augmented Lagrangians all have kinks. Newton's method, $x^{k+1} = x^k - F'(x^k)^{-1}F(x^k)$, is the standard fast local solver for smooth systems, but it needs a derivative at every iterate.

Qi and Sun (Math. Programming 58, 1993) replaced the Jacobian by an arbitrary element of Clarke's generalized Jacobian and showed that the resulting method converges locally superlinearly under a regularity condition they called semismoothness, extending Mifflin's notion for functionals (Mifflin, SIAM J. Control Optim. 15, 1977) to vector-valued maps. This theorem is the foundation of the family of semismooth Newton methods used in complementarity, variational inequalities and PDE-constrained optimization.

Timeline. Robinson (1988) and Pang (Math. OR 15, 1990) studied Newton methods built on B-derivatives, with convergence proved under a strong Fréchet derivative at the solution; Kummer (1988) gave an abstract framework for Newton methods for nonsmooth equations; Qi and Sun (1993) proved local superlinear convergence for the generalized-Jacobian iteration under semismoothness and nonsingularity of $\partial F(x^*)$, with order $1+p$ under $p$-order semismoothness.

Setting

Let $F : \mathbb R^n \to \mathbb R^m$ be locally Lipschitz. By Rademacher's theorem $F$ is differentiable on a set $D_F$ of full measure; write $JF(y)$ for the Jacobian at $y \in D_F$. The generalized Jacobian is

$$\partial F(x) = \mathrm{co}\Big\{\lim_{i\to\infty} JF(x_i) : x_i \to x,\ x_i \in D_F\Big\},$$

the convex hull of all limits of Jacobians along sequences of differentiability points converging to $x$. The one-sided directional derivative is $F'(x;h) = \lim_{t\downarrow 0}(F(x+th)-F(x))/t$.

$F$ is semismooth at $x$ if it is Lipschitz near $x$ and, for every $h$, the limit of $Vh'$ over $V \in \partial F(x+th')$, $h' \to h$, $t \downarrow 0$ exists. For $0 < p \le 1$, $F$ is $p$-order semismooth at $x$ if in addition $Vh - F'(x;h) = O(\|h\|^{1+p})$ for $V \in \partial F(x+h)$, $h \to 0$.

For $m = n$, the nonsmooth Newton method is

$$x^{k+1} = x^k - V_k^{-1}F(x^k), \qquad V_k \in \partial F(x^k), \tag{3.2}$$

where any element of $\partial F(x^k)$ may be chosen at each step. A run is a pair of sequences $(x^k)$, $(V_k)$ with $V_k \in \partial F(x^k)$ and $V_k(x^{k+1}-x^k) = -F(x^k)$ for all $k$. A root $x^*$ ($F(x^*) = 0$) is regular when every $V \in \partial F(x^*)$ is nonsingular.

Formalization targets

Goal: Theorem 3.2, local superlinear convergence

Let $F$ be locally Lipschitz, $F(x^*) = 0$, $F$ semismooth at $x^*$, and every $V \in \partial F(x^*)$ nonsingular. Then there is $\delta > 0$ such that every $V \in \partial F(y)$ with $\|y - x^*\| < \delta$ is nonsingular, a Newton step from such a $y$ stays within $\delta$ of $x^*$, and every run with $\|x^0 - x^*\| < \delta$ satisfies

$$x^k \to x^*, \qquad \|x^{k+1} - x^*\| = o(\|x^k - x^*\|).$$

The goal asserts only the shape of the convergence (superlinear) and fixes no constants.

Stronger: Theorem 3.2, order $1 + p$

If moreover $F$ is $p$-order semismooth at $x^*$, $0 < p \le 1$, there are $\delta > 0$ and $C$ with

$$\|x^{k+1} - x^*\| \le C\|x^k - x^*\|^{1+p}$$

for every run started within $\delta$ of $x^*$.

Milestones

The milestones follow the paper's route: Proposition 2.1 (the limit in the definition of semismoothness is the directional derivative), Lemma 2.2 (Lipschitz continuity of $F'(x;\cdot)$ and its realisation by an element of $\partial F(x)$), Theorem 2.3 (semismoothness is equivalent to $Vh - F'(x;h) = o(\|h\|)$ and to the corresponding condition at differentiability points), the Remark's expansion (2.17), Proposition 3.1 (uniform invertibility near a regular point), the order-$(1+p)$ sentence of Theorem 3.2, and Corollary 2.5 (strong Fréchet differentiability implies semismoothness).

Significance

The theorem gives a locally superlinearly convergent method for Lipschitz equations with no smoothness beyond semismoothness at the root. Convex, smooth and subsmooth functions are semismooth, as are sums and scalar products of semismooth functions (the paper, citing Mifflin), and later work showed that the complementarity and KKT reformulations on which semismooth Newton solvers are built are semismooth as well; the order-$(1+p)$ variant gives local quadratic convergence for strongly semismooth maps. Mission II of this series treats the paper's global convergence theorem on a ball, and Mission III the semismoothness of augmented Lagrangian gradients, which supplies the application.

The results are proved in the paper. No machine-checked version of the generalized Jacobian, of semismoothness or of the nonsmooth Newton method is known to exist in Mathlib or on this platform; the platform's formalized Newton results concern one-dimensional $C^2$ functions (MetodosNumericos.newton_local_convergence) and smooth convex minimization. A complete development would provide the first formal library for Clarke's generalized Jacobian and semismooth maps.

Difficulty

The classical Newton proof compares $F(x^k)$ with its linearization $JF(x^*)(x^k - x^*)$ and uses continuity of the Jacobian at $x^*$. Here neither is available: $F$ need not be differentiable at $x^*$ or at any iterate, the element $V_k$ is chosen arbitrarily from a set, and $V_k$ need not be close to any fixed linear map. The comparison has to go through the directional derivative $F'(x^*; \cdot)$, which is only positively homogeneous, not linear. The analytic content therefore sits in Section 2: showing that semismoothness, defined through a limit over a set-valued map, controls $Vh - F'(x;h)$ uniformly in the direction, and that $F(x+h) - F(x) - F'(x;h)$ is small. Both rest on Clarke's mean-value inclusion and on compactness and upper semicontinuity of $\partial F$, none of which is in Mathlib. The superlinear rate also requires a uniform bound on $\|V^{-1}\|$ in a whole neighbourhood, not just at $x^*$.

Formalization scope

Everything lives in the namespace NonsmoothNewton.Local. Section 2 results are stated for maps between finite-dimensional real normed spaces $E \to G$ (the paper's $\mathbb R^n \to \mathbb R^m$ is the Euclidean instance); Section 3 results use EuclideanSpace ℝ (Fin n). Conventions fixed by the Lean statements:

• $JF$ is fderiv; the generalized Jacobian is the convex hull (no closure) of limits of fderiv along sequences $x_i \to x$ of differentiability points.
• $F'(x;h)$ is the one-sided limit over $t \downarrow 0$, never the two-sided lineDeriv; its value is a limUnder, used only where existence is a hypothesis or a consequence.
• Nonsingular means IsUnit in the ring of continuous linear endomorphisms; $\|V^{-1}\| \le C$ is a two-sided inverse of operator norm at most $C$.
• A run of (3.2) is encoded by the linear equation $V_k(x^{k+1} - x^k) = -F(x^k)$ with $V_k \in \partial F(x^k)$; all choices of $V_k$ are quantified, and $\delta$ is chosen before the run.
• Pinned asymptotics. The goal's rate is the proof's display (3.3), stated as IsLittleO along atTop; the printed Theorem 3.2 states only well-definedness and convergence. "Order $1+p$" is pinned as $\|x^{k+1}-x^*\| \le C\|x^k-x^*\|^{1+p}$ with $\delta$ and $C$ uniform over runs. Every $o(\|h\|)$ in (2.8), (2.9) and (2.17) is its $\varepsilon$–$\delta$ form with a non-strict inequality $\le \varepsilon\|h\|$, and every $O(\|h\|^{1+p})$ is an explicit constant and radius.
• The standing assumptions "$F$ locally Lipschitzian" of Sections 2 and 3 are hypotheses of every statement.
• The strong Fréchet derivative of Corollary 2.5 is Mathlib's HasStrictFDerivAt, which corrects the misprint $F(x)$ for $F(z)$ in the paper's display (2.16).

A trivializing formalization is ruled out: the update is not written with a junk inverse (which would make a singular step "well defined"), the generalized Jacobian is the paper's nonempty set rather than one that could be empty, and the theorem quantifies over every run rather than asserting that some run converges.

A complete development needs Clarke's mean-value inclusion (2.2), compactness and upper semicontinuity of $\partial F$ for locally Lipschitz maps (via Rademacher's theorem, available in Mathlib), and perturbation bounds for inverses of linear maps. The generalized-Jacobian and semismoothness layer is reusable beyond this mission, in particular for Missions II and III of this series. Contributions of proofs of any milestone, and of general lemmas about $\partial F$, are welcome.

Selected references

• L. Qi, J. Sun, A nonsmooth version of Newton's method, Mathematical Programming 58 (1993) 353–367. https://doi.org/10.1007/BF01581275
• F. H. Clarke, Optimization and Nonsmooth Analysis, Wiley, 1983 (SIAM reprint 1990). https://doi.org/10.1137/1.9781611971309
• R. Mifflin, Semismooth and semiconvex functions in constrained optimization, SIAM Journal on Control and Optimization 15 (1977) 959–972. https://doi.org/10.1137/0315061
• J.-S. Pang, Newton's method for B-differentiable equations, Mathematics of Operations Research 15 (1990) 311–341. https://doi.org/10.1287/moor.15.2.311
• J. M. Ortega, W. C. Rheinboldt, Iterative Solution of Nonlinear Equations in Several Variables, Academic Press, 1970 (SIAM reprint 2000). https://doi.org/10.1137/1.9780898719468

Motivation

Connecting a set of terminals by a network of direct links of least total length is one of the oldest problems of combinatorial optimization. R. C. Prim's 1957 paper in the Bell System Technical Journal (DOI) was motivated by the rate structure for Bell System leased-line services, in which the charge for connecting a set of terminals depends on the length of a shortest network connecting them. The paper states two local construction principles, P1 and P2, and shows that any sequence of their applications produces a shortest network, first for points in the plane and then for arbitrary connected labelled graphs with arbitrary real edge lengths. The paper's §V specialization of the principles, growing a single fragment, is what is now called Prim's algorithm, and its §IV statement is the form of the minimum spanning tree theorem used throughout network design, clustering and approximation algorithms.

Timeline. O. Borůvka (1926) solved the problem for an electrical network in Moravia; V. Jarník (1930) gave the single-fragment procedure; J. B. Kruskal (1956, Proc. AMS 7, 48–50) proved that adding globally shortest links avoiding cycles yields a shortest spanning tree; Prim (1957) gave the more permissive principles P1 and P2, which contain both the Jarník procedure and Kruskal's rule as special orders of application; E. W. Dijkstra (1959) rediscovered the single-fragment procedure.

Setting

Let $V$ be a finite set of $N$ terminals and $G$ a simple graph on $V$, the labelled graph whose edges are the possible links. Each edge $e$ carries a real length $w(e)$; lengths may be negative, zero, or tie. For a finite set $F$ of links, $H(F)$ denotes the graph on $V$ whose edges are the links of $F$.

• A spanning subtree of $G$ is a set $F$ of edges of $G$ such that $H(F)$ is a tree on $V$. Its length is $\ell_w(F) = \sum_{e \in F} w(e)$.
• A shortest spanning subtree (SSS) is a spanning subtree of least length among all spanning subtrees of $G$. Prim's dictionary is "shortest connection network (SCN) ↔ shortest spanning subtree (SSS)". $L(G,w)$ denotes that least length.
• Given the links $F$ made so far, the connected components of $H(F)$ are the isolated terminals (one terminal) and isolated fragments (two or more terminals).
• Principle 1: any isolated terminal $t$ can be connected to a nearest neighbor, a $G$-neighbor $n$ with $w(\{t,n\}) \le w(\{t,m\})$ for all $G$-neighbors $m$ of $t$.
• Principle 2: any isolated fragment $C$ can be connected to a nearest neighbor $n \notin C$ by a shortest available link $\{u,n\}$, $u \in C$; equivalently $\{u,n\}$ is a shortest edge of $G$ with one end in $C$ and the other outside.
• A construction is a sequence of links $e_0, e_1, \dots$, each an application of P1 or P2 with respect to the links before it. It is complete when it has $N-1$ links.

Only edges of $G$ are possible links; in Prim's distance table a missing edge has length $\infty$.

Formalization targets

Goal (§IV, p. 1396)

For every finite connected graph $G$ and every $w$,

$$\Bigl(\exists\ \text{a complete construction}\Bigr) \ \wedge\ \Bigl(\forall\ \text{complete constructions } e_0,\dots,e_{N-2}:\ \{e_0,\dots,e_{N-2}\} \text{ is a SSS of } G\Bigr).$$

This is the sentence "P1 and P2 will provide a SSS for any connected labelled graph with any set of real edge lengths." It fixes nothing about the order of applications, the component chosen, or the tie-breaking.

Milestones

1. Counting (§II, p. 1392): after any construction with $k$ links, $H(F)$ is acyclic with $N-k$ components; a complete construction is a spanning subtree; a construction with fewer than $N-1$ links can be extended.
2. Necessary Condition 1 (p. 1392): every terminal of a SSS is linked in it to at least one nearest neighbor.
3. Necessary Condition 2 (p. 1392): every fragment $S$ of a SSS, $\emptyset \ne S \ne V$, is linked in it to a nearest neighbor by a shortest available link.
4. Distinct lengths (§III, p. 1393): if the edge lengths are pairwise distinct, every link of every construction belongs to every SSS.
5. Continuity (§III, p. 1394): $w \mapsto L(G,w)$ is continuous.

Significance

The goal is the correctness theorem of a whole family of greedy minimum spanning tree procedures at once: Jarník–Prim (one growing fragment), Kruskal (globally shortest link first) and Borůvka-style interleavings all produce sequences of P1/P2 applications. Because lengths are arbitrary reals, it also covers maximum spanning trees by a sign change (p. 1397) and graphs that are not complete.

The result is classical and fully proved in the literature. What this mission adds is a machine-checked statement in exactly Prim's generality. Mathlib has spanning trees of connected graphs (SimpleGraph.Connected.exists_isTree_le) and the edge count of trees, but no minimum spanning tree theory. Existing Prove2Me items on minimum spanning trees are either restricted to complete graphs with distance matrices or state a cut property in existence form at a single vertex; none states Prim's principles or his necessary conditions.

Difficulty

The obvious argument, "each link P1 or P2 adds belongs to the shortest network", uses a unique shortest network, and that fails with ties: when two links tie, a P1/P2 link need not lie in a given SSS. Prim's own treatment of ties (§III) is an informal perturbation argument; the formal statement must hold for every tie-breaking choice made during a construction, not only for a generic perturbed instance. Negative lengths remove the easy reading "shortest connected spanning subgraph": the minimum must range over trees only. The statements also involve the component structure of $H(F)$ as it changes during a construction, and tree paths in an arbitrary, not necessarily complete, graph.

Formalization scope

Namespace ShortestConnection.Principles, Mathlib SimpleGraph. Conventions:

• $V$ is a Fintype with decidable equality; $G$ is a SimpleGraph V (at most one link per pair, no loops, which is Prim's setting). Lengths are w : Sym2 V → ℝ; only values on edges of $G$ matter.
• Link sets are Finset (Sym2 V); linkGraph F is SimpleGraph.fromEdgeSet F. A spanning subtree requires ↑F ⊆ G.edgeSet and (linkGraph F).IsTree.
• An isolated fragment is a whole connected component of linkGraph F; the P2 condition is a single inequality against every $G$-edge leaving it, which is equivalent to "nearest neighbor and shortest link" in Prim's sense.
• A construction is a List (Sym2 V) checked entrywise against l.take i; complete means length Fintype.card V - 1 (natural subtraction, used only for nonempty $V$).
• $L$ is sInf of the lengths of spanning subtrees; continuity is in the product topology.

Implicit hypotheses made explicit: $G$ connected (hence $V \ne \emptyset$) wherever an SSS or a complete construction is involved; at least two terminals for Necessary Condition 1; $S$ nonempty and $S \ne V$ for Necessary Condition 2; pairwise distinct edge lengths only in milestone 4, as in the paper's temporary assumption.

The goal's existence clause rules out a vacuous formalization in which no complete construction exists; the step predicates are defined from lengths and components only, never through shortest spanning subtrees, and they are not restricted to one growing fragment or to the globally shortest link.

Needed infrastructure: tree exchange (adding an edge to a spanning tree creates one cycle; removing any other cycle edge yields a spanning tree), component counts under edge addition, and minima of finitely many continuous functions. The exchange and counting lemmas are reusable for any matroid-greedy or spanning-tree mission. Contributions of intermediate lemmas, and proofs of the milestones in any order, are welcome.

Selected references

• R. C. Prim, Shortest Connection Networks And Some Generalizations, Bell System Technical Journal 36 (1957), 1389–1401. https://doi.org/10.1002/j.1538-7305.1957.tb01515.x
• J. B. Kruskal, On the shortest spanning subtree of a graph and the traveling salesman problem, Proceedings of the AMS 7 (1956), 48–50. https://doi.org/10.1090/S0002-9939-1956-0078686-7
• V. Jarník, O jistém problému minimálním, Práce Moravské Přírodovědecké Společnosti 6 (1930), 57–63.
• O. Borůvka, O jistém problému minimálním, Práce Moravské Přírodovědecké Společnosti 3 (1926), 37–58.
• R. L. Graham, P. Hell, On the history of the minimum spanning tree problem, Annals of the History of Computing 7 (1985), 43–57. https://doi.org/10.1109/MAHC.1985.10011

Motivation

Quasi-Newton methods minimize a smooth function $f$ on $\mathbb{R}^n$ by moving along $d_k = -H_k g_k$, where $g_k$ is the gradient and $H_k$ is an approximation of the inverse Hessian built from observed gradient differences. The BFGS update is the most widely used way of building $H_k$, but it stores a dense $n \times n$ matrix, which is prohibitive for large $n$.

Nocedal's 1980 paper (Math. Comp. 35, 773–782) proposed keeping only the last $m$ correction pairs and rebuilding the matrix from a simple initial matrix $H_0$ at every step. The resulting method, called SQN in the paper, is now known as L-BFGS, and it is the default large-scale unconstrained optimizer in many numerical libraries and in machine learning. The paper's main theoretical claim is that this truncation does not destroy the finite termination of BFGS on quadratics.

Timeline:

• 1970: Broyden, Fletcher, Goldfarb and Shanno introduce the BFGS update (references [1] and [5] of the paper).
• 1977: Nazareth relates BFGS to conjugate gradients (Argonne Tech. Memo 282, reference [7]); his form of preconditioned conjugate gradients is the one the paper uses.
• 1977–1978: Shanno studies the memoryless BFGS update, the case $m = 1$ (reference [11]; journal version Math. Oper. Res. 3, 1978).
• 1980: Nocedal defines the special BFGS matrices and the SQN method and states that on quadratics with exact line searches SQN is identical to preconditioned conjugate gradients, hence has quadratic termination.
• 1989: Liu and Nocedal (Math. Programming 45) study the method, now called L-BFGS, for large-scale problems.
• 1998: Kolda, O'Leary and Nazareth (SIAM J. Optim. 8) treat limited-memory and update-skipping BFGS variants with exact line searches on quadratics.

Setting

Let $A$ be a symmetric positive definite $n \times n$ matrix and $b \in \mathbb{R}^n$, and let $f(x) = \tfrac12 x^T A x + b^T x$, a strictly convex quadratic with gradient $g(x) = Ax + b$ and unique minimizer $x^\ast = -A^{-1} b$.

Exact line search. Along a direction $d \neq 0$ from $x$, the step $\alpha = -g(x)^T d / d^T A d$ minimizes $f(x + \alpha d)$.

BFGS update. For a pair $(s, y)$ with $\rho = 1/y^T s$ and $v = I - \rho y s^T$, the BFGS update of $H$ is

$$\bar H = v^T H v + \rho s s^T .$$

Special BFGS matrices. Fix $H_0$ symmetric positive definite and a number $m \ge 1$ of stored corrections. Given pairs $(s_j, y_j)$, the special matrix $H_K$ is $H_0$ updated by the pairs $j = K - \min(K, m), \dots, K-1$, oldest first (the paper's (4)–(5)). Only the $m$ most recent pairs enter, and the matrix is rebuilt from $H_0$.

SQN. Starting from $x_0$, with $g_i = g(x_i)$:

$$d_i = -H_i g_i, \qquad x_{i+1} = x_i + \alpha_i d_i, \qquad s_i = x_{i+1} - x_i,\quad y_i = g_{i+1} - g_i,$$

with $\alpha_i$ the exact step and $H_{i+1}$ the special matrix built from the last $\min(i+1, m)$ pairs.

PCG with fixed preconditioner $H_0$. $d_0 = -H_0 g_0$, $x_{i+1} = x_i + \alpha_i d_i$, $d_{i+1} = -H_0 g_{i+1} + \beta_{i+1} d_i$ with $\beta_{i+1} = y_i^T H_0 g_{i+1} / y_i^T d_i$.

Formalization targets

Goal: quadratic termination of SQN

For every $n$, every symmetric positive definite $A$ and $H_0$, every $b$, $x_0$ and every $m \ge 1$,

$$\exists\, k \le n : \quad A x_k + b = 0 ,$$

where $x_k$ are the SQN iterates. The statement fixes no constant beyond the dimension bound $n$.

Milestones

1. Property (a): the special matrices are positive definite whenever $y_i^T s_i > 0$ for all $i$.
2. Eq. (7): along conjugate steps, $v_i y_i = 0$ and $v_i y_j = y_j$ for $i > j$.
3. Eq. (6): along conjugate steps, $H_k y_j = s_j$ for the $m$ most recent $j$ (when $k > m$).
4. Eq. (10): the special matrix equals $m$ sum-form BFGS corrections applied to $H_0$.
5. Eq. (15): the PCG directions satisfy $d_i^T y_j = 0$ for $i \neq j$.
6. Eq. (16): $g_i^T H_0 g_j = 0$ for $i \neq j$ and $g_i^T d_j = 0$ for $j < i$.
7. The PCG with fixed preconditioner $H_0$ reaches the minimizer in at most $n$ steps.
8. SQN and this PCG produce identical iterates and directions at every step.

Significance

The result shows that storing only $m$ correction pairs costs nothing on quadratics: for any $m \ge 1$, SQN terminates in at most $n$ steps, like full BFGS and conjugate gradients. It explains why L-BFGS with small $m$ is competitive, and it is the model case for later analyses of limited-memory methods (their linear convergence on uniformly convex functions, and their relation to Krylov methods). Property (b) is the reason one expects efficiency to grow with $m$: the matrix satisfies the secant equation on the $m$ most recent directions.

The claims are classical and generally accepted, but the paper argues them in a few lines ("it is straightforward to show"), deferring the PCG facts (15)–(16) to a reference. No machine-checked proof of the termination of BFGS, L-BFGS or preconditioned conjugate gradients is known to this mission. A formalization would provide a verified model of L-BFGS on quadratics and a reusable development of conjugate-direction methods with a preconditioner.

Difficulty

The obvious route, "SQN is BFGS and BFGS terminates", fails: SQN discards old corrections, so the classical BFGS argument (hereditary secant conditions on all past directions) does not apply once more than $m$ steps have been taken. The paper asserts the identity of SQN with preconditioned conjugate gradients in one sentence ("using a similar argument as for the SCG"), and the PCG relations it relies on are quoted from a technical report. The other difficulty is bookkeeping: the window of stored pairs shifts, the matrix is a nested product, and the runs must remain meaningful after the minimizer is reached.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, $x^T y$ is dotProduct, and $s y^T$ is Matrix.vecMulVec. Symmetric positive definiteness is Matrix.PosDef. Indices are 0-based, as in the paper. The exact line search is the closed-form step $-g^T d / d^T A d$. The iterations have no stopping rule: once the gradient vanishes the direction and step are zero and the iterate stays at the minimizer (Lean's $0/0 = 0$). Past that point the zero pair stored by SQN leaves the BFGS step unchanged. The hypotheses are exactly the paper's: $A \succ 0$, $H_0 \succ 0$, $m \ge 1$ and exact line searches. $H_0$ need not be diagonal.

Two misprints are corrected and flagged in the items: the denominator of $\beta$ in (13) is $y_{i-1}^T d_{i-1}$ (as in (12) and p. 778), and the second relation of (16) is stated for $j < i$ (as used on p. 778), since it fails for $i < j$.

Ruled out: SQN is defined through its own matrices (4)–(5), rebuilt from $H_0$ and the last $m$ pairs. It is not defined through the PCG recurrence, not by one BFGS update of the previous matrix, and not with a stop rule that returns $-A^{-1}b$. The standing assumption $y_k^T s_k > 0$ is not a hypothesis of any statement about a run (it fails after termination and would make the goal vacuous). With $m = 0$ SQN is steepest descent and the goal is false, so $m \ge 1$ is required.

Needed infrastructure: algebra of rank-one updates and of Matrix.PosDef under congruence, conjugate-direction lemmas for quadratics, and the fact that $n+1$ mutually $H_0$-orthogonal vectors in $\mathbb{R}^n$ include a zero vector. The PCG results (milestones 5–7) are reusable beyond this mission. Proofs of any milestone, or of the goal directly, are welcome.

Selected references

• J. Nocedal, Updating Quasi-Newton Matrices with Limited Storage, Mathematics of Computation 35(151), 1980, 773–782. https://doi.org/10.1090/s0025-5718-1980-0572855-7
• D. F. Shanno, Conjugate gradient methods with inexact searches, Mathematics of Operations Research 3(3), 1978, 244–256. https://doi.org/10.1287/moor.3.3.244
• L. Nazareth, A Relationship Between the BFGS and Conjugate Gradient Algorithms, ANL-AMD Tech. Memo 282 (rev.), Argonne National Laboratory, 1977 (reference [7] of Nocedal 1980; no online copy located).
• T. G. Kolda, D. P. O'Leary, L. Nazareth, BFGS with update skipping and varying memory, SIAM Journal on Optimization 8(4), 1998, 1060–1083. https://doi.org/10.1137/S1052623496306450
• D. C. Liu, J. Nocedal, On the limited memory BFGS method for large scale optimization, Mathematical Programming 45, 1989, 503–528. https://doi.org/10.1007/BF01589116

Motivation

Newton's method is the standard second-order algorithm for unconstrained minimization, but without safeguards it has no global guarantee: far from a minimizer the Newton step can increase the objective, and at a point where the Hessian is indefinite the step can head for a saddle point or a maximum. The usual repairs (line search, trust regions, Levenberg–Marquardt damping) come with convergence proofs, but for nonconvex objectives those proofs typically give no rate at all, or only the rate of the gradient method.

Nesterov and Polyak (Math. Program. 108 (2006) 177–205) proposed to regularize the second-order Taylor model of the objective with a cubic term and to take as the next iterate a global minimizer of the regularized model. They showed that the resulting method has a global worst-case rate of convergence to points satisfying the second-order necessary conditions, for every objective with a Lipschitz continuous Hessian and without any convexity. That rate, $O(k^{-2/3})$ for the gradient norm, is better than the $O(k^{-1/2})$ of the gradient method. It became the reference point for the complexity theory of nonconvex second-order optimization: adaptive variants (Cartis, Gould and Toint, Math. Program. 127 (2011) 245–295) and lower bounds showing that $O(\epsilon^{-3/2})$ iterations are optimal among second-order methods (Carmon, Duchi, Hinder and Sidford, Math. Program. 184 (2020) 71–120) are stated against it.

This mission formalizes the general convergence result of that paper, Theorem 1 of Section 3, together with the properties of the cubic step from Section 2 on which it rests.

Setting

Let $F \subseteq \mathbb{R}^n$ be a closed convex set with nonempty interior, and let $f$ be twice differentiable on $F$ with gradient $f'(x)$ and Hessian $f''(x)$. A starting point $x_0 \in \operatorname{int} F$ is fixed, and $F$ is assumed to contain the level set $\mathcal{L}(f(x_0)) = \{x \in \mathbb{R}^n : f(x) \le f(x_0)\}$ in its interior. Assumption 1: the Hessian is Lipschitz continuous on $F$ in the spectral norm, $\|f''(x) - f''(y)\| \le L\|x - y\|$ for all $x, y \in F$, with $L > 0$.

For a parameter $M > 0$ the cubic model of $f$ at $x$ is

$$m_{M,x}(y) = \langle f'(x), y - x\rangle + \tfrac12 \langle f''(x)(y - x), y - x\rangle + \tfrac{M}{6}\|y - x\|^3 .$$

The cubic-regularized Newton step $T_M(x)$ is any global minimizer of $m_{M,x}$ over $\mathbb{R}^n$; it exists because the model is continuous and coercive. Write $r_M(x) = \|x - T_M(x)\|$ and $\bar f_M(x) = f(x) + \min_y m_{M,x}(y)$.

The cubic regularization of Newton method (3.3) fixes $L_0 \in (0, L]$, starts at $x_0$ and, for $k \ge 0$, chooses $M_k \in [L_0, 2L]$ such that $f(T_{M_k}(x_k)) \le \bar f_{M_k}(x_k)$, then sets $x_{k+1} = T_{M_k}(x_k)$. The choice $M_k = L$ always passes the test.

Write $\lambda_n(A)$ for the smallest eigenvalue of a symmetric matrix $A$. The measure of local optimality is

$$\mu_M(x) = \max\Big\{ \sqrt{\tfrac{2}{L + M}\,\|f'(x)\|},\ -\tfrac{2}{2L + M}\,\lambda_n(f''(x)) \Big\}.$$

It is nonnegative and vanishes exactly when $f'(x) = 0$ and $f''(x) \succeq 0$.

Formalization targets

Goal: Theorem 1, inequality (3.4)

If $f(x) \ge f^*$ for all $x \in F$, then every run of method (3.3) satisfies, for every $k \ge 1$,

$$\min_{1 \le i \le k} \mu_L(x_i) \le \frac{8}{3}\cdot\left(\frac{3\,(f(x_0) - f^*)}{2k\cdot L_0}\right)^{1/3}.$$

The constant $8/3$ and the exponent $1/3$ are the paper's; the statement holds for every admissible choice of the parameters $M_k$ and of the global minimizers $x_{k+1}$.

Milestones, in attack order

1. Lemma 1 (2.2): $\|f'(y) - f'(x) - f''(x)(y - x)\| \le \tfrac12 L\|y - x\|^2$ on $F$.
2. Eq. (2.5): $f'(x) + f''(x)(T - x) + \tfrac12 M\|T - x\|(T - x) = 0$ for $T = T_M(x)$.
3. Proposition 1 (2.7): $f''(x) + \tfrac12 M r_M(x) I \succeq 0$.
4. Lemma 2 (2.8): $\langle f'(x), x - T_M(x)\rangle \ge 0$ when $f(x) \le f(x_0)$.
5. Lemma 4 (2.11): $f(x) - \bar f_M(x) \ge \tfrac{M}{12} r_M(x)^3$.
6. Lemma 4 (2.12): for $M \ge L$, $T_M(x) \in F$ and $f(T_M(x)) \le \bar f_M(x)$.
7. Lemma 3 (2.9): $\|f'(T_M(x))\| \le \tfrac12(L + M) r_M(x)^2$ when $T_M(x) \in F$.
8. Lemma 5: $\mu_M(T_M(x)) \le r_M(x)$.
9. Theorem 1, first claim: $\sum_{i \ge 0} r_{M_i}(x_i)^3 \le \tfrac{12}{L_0}(f(x_0) - f^*)$.
10. Theorem 1, second claim: $\lim_{i\to\infty} \mu_L(x_i) = 0$.

Significance

Inequality (3.4) is a global, dimension-free complexity bound for reaching approximate second-order stationarity. It controls both the gradient norm, $\min_{1\le i\le k}\|f'(x_i)\| = O(k^{-2/3})$, and the most negative curvature, $\max\{0, -\lambda_n(f''(x_i))\} = O(k^{-1/3})$, along the best iterate, from a single scalar potential $f(x_0) - f^*$. The second claim of Theorem 1 gives the asymptotic counterpart: every limit point satisfies the second-order necessary conditions. Section 4 of the paper derives its faster rates for star-convex and gradient-dominated functions from the same Section 2 lemmas.

The result is proved on paper and widely cited; to our knowledge no machine-checked proof of it or of the Section 2 lemmas exists. A formalization adds a checked statement of the method with its exact constants, and reusable facts about global minimizers of cubic models (Proposition 1 in particular) that the companion missions on star-convex, gradient-dominated and locally quadratic convergence also rely on.

Difficulty

Most steps are short inequalities, but two are not. Proposition 1 is a statement about a global minimizer of a nonconvex function: the first- and second-order conditions of a local minimizer give only $f''(x) + \tfrac12 M r I + \tfrac{M}{2r}(T - x)(T - x)^\top \succeq 0$, which is weaker. The natural first attempt, "take the second-order optimality condition of the model at $T$", therefore fails. The paper proves it in Section 5.1 through a one-dimensional dual characterization of the minimizer.

The second is Lemma 2's second claim, used for (2.12): showing that $T_M(x)$ stays in $F$ requires a boundary argument along the segment from $x$ to $T_M(x)$, since the Taylor bounds are only available inside $F$. The remaining work is calculus in $\mathbb{R}^n$: the integral form of Taylor's theorem for the gradient under a Lipschitz Hessian, and eigenvalue perturbation for the second entry of $\mu$.

Formalization scope

The space is EuclideanSpace ℝ (Fin n) for arbitrary n : ℕ. The gradient and Hessian are maps g and H with HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every x ∈ F. At boundary points of $F$ this asks for two-sided derivatives, a mild strengthening of "twice differentiable on $F$". The Lipschitz condition uses the operator norm, which is the spectral norm. $T_M(x)$ is represented by the predicate IsCubicStep (global minimizer of cubicModel), and every lemma is stated for every such minimizer. The run predicate IsCubicNewtonRun is 0-based. It writes $\bar f_{M_k}(x_k)$ as $f(x_k)$ plus the model value at $x_{k+1}$, which is the minimum because $x_{k+1}$ attains it. $\lambda_n$ is lamMin, the Rayleigh-quotient infimum over the unit sphere, which equals the smallest eigenvalue for the (symmetric) Hessian. The lower bound $f^*$ is required on $F$ only. The minimum over $1 \le i \le k$ is written as the existence of an index attaining the bound.

A stationary point of the cubic model is not an admissible step, and the run must keep the test $M_k \in [L_0, 2L]$ and the acceptance test. Replacing the step by any point with $f(x_{k+1}) \le f(x_k)$ makes the goal false, and dropping the square root in $\mu_M$ makes Lemma 5 false. The statements rule out all three. Lemma 5 carries the hypothesis $T_M(x) \in F$, which its printed proof uses and which holds at every iterate.

A complete development needs the Taylor bounds (2.2)–(2.3) for vector-valued derivatives on convex sets, and first- and second-order optimality for the cubic model. It also needs a proof of Proposition 1 (Section 5.1 or any other correct argument) and eigenvalue perturbation via Rayleigh quotients. The cubic-model lemmas and Proposition 1 are reusable across the whole series. Proofs of any milestone, alternative proofs of Proposition 1, and general Mathlib-level lemmas about Rayleigh quotients are welcome.

Selected references

• Yu. Nesterov and B. T. Polyak, Cubic regularization of Newton method and its global performance, Mathematical Programming, Ser. A 108 (2006) 177–205. https://doi.org/10.1007/s10107-006-0706-8
• C. Cartis, N. I. M. Gould and Ph. L. Toint, Adaptive cubic regularisation methods for unconstrained optimization. Part I: motivation, convergence and numerical results, Mathematical Programming 127 (2011) 245–295. https://doi.org/10.1007/s10107-009-0286-5
• Y. Carmon, J. C. Duchi, O. Hinder and A. Sidford, Lower bounds for finding stationary points I, Mathematical Programming 184 (2020) 71–120. https://doi.org/10.1007/s10107-019-01406-y
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9