All missions

Motivation

A set function $f : 2^{\mathcal N} \to \mathbb R$ on a finite ground set $\mathcal N$ is submodular if it has diminishing returns, equivalently if $f(A) + f(B) \ge f(A \cup B) + f(A \cap B)$ for all $A, B \subseteq \mathcal N$. Cut functions of graphs and hypergraphs, coverage functions, entropy, and many facility-location and welfare objectives are submodular. Unconstrained Submodular Maximization (USM) asks, given a nonnegative submodular $f$ through a value oracle, for a set $S \subseteq \mathcal N$ of maximum value. It contains Max-Cut, Max-DiCut and Max Facility Location as special cases, and it is a subroutine in algorithms for constrained submodular maximization.

Timeline:

• Feige, Mirrokni and Vondrák (FOCS 2007; SIAM J. Comput. 2011) gave a uniformly random set achieving $1/4$ of the optimum, a deterministic local search achieving $1/3 - \varepsilon/n$, a randomized local search achieving $2/5$, and proved that no algorithm making polynomially many value queries achieves $1/2 + \varepsilon$.
• Oveis Gharan and Vondrák (SODA 2011) improved the ratio to about $0.41$ by simulated annealing; Feldman, Naor and Schwartz (ICALP 2011) to about $0.42$.
• Buchbinder, Feldman, Naor and Schwartz (FOCS 2012; SIAM J. Comput. 2015) gave the double greedy algorithms: a deterministic linear-time $1/3$-approximation (this mission) and a randomized linear-time $1/2$-approximation, matching the query lower bound.

Setting

Let $\mathcal N$ be a finite ground set and $f : 2^{\mathcal N} \to \mathbb R_{\ge 0}$ a nonnegative submodular function. Write $f(OPT) = \max_{S \subseteq \mathcal N} f(S)$, and let $OPT$ denote a set attaining it.

Algorithm 1 (DeterministicUSM) fixes an arbitrary order $u_1, \dots, u_n$ of $\mathcal N$ and maintains two solutions, starting from $X_0 = \emptyset$ and $Y_0 = \mathcal N$. In iteration $i = 1, \dots, n$ it computes

$$a_i = f(X_{i-1} \cup \{u_i\}) - f(X_{i-1}), \qquad b_i = f(Y_{i-1} \setminus \{u_i\}) - f(Y_{i-1}).$$

If $a_i \ge b_i$ it sets $X_i = X_{i-1} \cup \{u_i\}$, $Y_i = Y_{i-1}$; otherwise $X_i = X_{i-1}$, $Y_i = Y_{i-1} \setminus \{u_i\}$. A tie adds $u_i$. After $n$ iterations $X_n = Y_n$, which is the output.

The analysis uses the hybrid sets $OPT_i = (OPT \cup X_i) \cap Y_i$, which agree with $X_i$ and $Y_i$ on $u_1, \dots, u_i$ and with $OPT$ on $u_{i+1}, \dots, u_n$. In Lean, the run is state f l i, the state $(X_i, Y_i)$ after the first $i$ entries of the order l, and $OPT_i$ is optI O (state f l i).

Formalization targets

Goal: Theorem I.1

For every nonnegative submodular $f$ and every order of $\mathcal N$,

$$X_n = Y_n \qquad\text{and}\qquad f(OPT) \le 3\, f(X_n).$$

Milestones

1. Lemma II.1. For every $1 \le i \le n$, $a_i + b_i \ge 0$.
2. The hybrid sequence. $OPT_i$ agrees with $X_i, Y_i$ on $u_1, \dots, u_i$ and with $OPT$ on the rest; $OPT_0 = OPT$ and $OPT_n = X_n = Y_n$.
3. Lemma II.2. For every $1 \le i \le n$,

$$f(OPT_{i-1}) - f(OPT_i) \le [f(X_i) - f(X_{i-1})] + [f(Y_i) - f(Y_{i-1})].$$

4. The telescoped display. $f(OPT_0) - f(OPT_n) \le [f(X_n) - f(X_0)] + [f(Y_n) - f(Y_0)] \le f(X_n) + f(Y_n)$.
5. Theorem II.3 (tightness). For every $\varepsilon > 0$ there is a nonnegative submodular $f$ with $f(OPT) > 0$ and an order on which $f(X_n) \le (1/3 + \varepsilon)\, f(OPT)$.

Significance

The result. Algorithm 1 is the deterministic member of the double greedy family. It makes one pass over the ground set with four value queries per element, and it guarantees $1/3$ of the optimum for every order, without the polynomial-but-large running time and the $\varepsilon/n$ loss of local search. Its analysis, which charges the decrease of $f(OPT_i)$ to the increases of $f(X_i)$ and $f(Y_i)$, is the template the paper then refines into the randomized $1/2$-approximation (Theorem I.2) and its continuous counterpart on the multilinear extension. Theorem II.3 shows that $1/3$ is the exact ratio of this algorithm, so the improvement to $1/2$ requires randomization (or a different deterministic rule) rather than a sharper analysis.

Formalizing it. The theorem is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a formal statement of the algorithm as printed, a checked proof of its guarantee for every order, and a checked tight instance. The definitions of the run and of $OPT_i$ are the same objects the randomized and fractional analyses reason about, so a complete development here is the first step toward the paper's main theorem.

Difficulty

The individual inequalities are short; the difficulty lies in the bookkeeping. Each step needs the invariants $X_{i-1} \subseteq Y_{i-1}$ and $u_i \in Y_{i-1} \setminus X_{i-1}$, which follow from the order being an enumeration (no repetitions, every element present), and the identification of $OPT_i$ from $OPT_{i-1}$ in each branch of the algorithm. Summing Lemma II.2 needs a telescoping over the run defined as a fold. The naive idea of comparing $f(X_n)$ with $f(OPT)$ directly, without the hybrid sets, gives no bound: the greedy choices are made against $X$ and $Y$, not against $OPT$. For Theorem II.3 the difficulty is producing an explicit instance, checking that it is submodular and nonnegative, and tracing the run, including the ties, which the algorithm resolves by adding.

Formalization scope

• The ground set is a finite type X with decidable equality; subsets are Finset X; $f$ is real valued, Finset X → ℝ, and nonnegativity is the hypothesis ∀ S, 0 ≤ f S where the page uses it (the goal, the telescoped display and the tight example). Lemma II.1, Lemma II.2 and the hybrid-sequence milestone do not assume it.
• Submodularity is the lattice form $f(A) + f(B) \ge f(A \cup B) + f(A \cap B)$ of the paper's footnote 1, through the published definition NonmonotoneSubmod.Shared.Submodular. The paper's main-text sentence ("for every $A \subseteq B \subseteq \mathcal N$ and $u \in \mathcal N$") would force monotonicity when $u \in B \setminus A$ and is read as the footnote. $f(OPT)$ is the published NonmonotoneSubmod.Shared.OPT f, the maximum of $f$ over all subsets.
• The order $u_1, \dots, u_n$ is a list l with l.Nodup and ∀ x, x ∈ l; $u_i$ is l[i - 1]. Every statement quantifies over all such lists. No nonemptiness of $\mathcal N$ is assumed: for an empty ground set the goal reads $f(\emptyset) \le 3 f(\emptyset)$.
• The tie rule is line 5's $a_i \ge b_i$: ties add $u_i$.
• Where a milestone mentions an optimal solution, it takes a set O with ∀ S, f S ≤ f O.
• The goal is stated multiplied out, $f(OPT) \le 3 f(X_n)$, because $f(OPT)$ may be $0$.
• Trivializing formalizations ruled out. The paper's Theorem I.1 reads "there exists a deterministic linear time $(1/3)$-approximation algorithm"; without the running time that existential is satisfied by exhaustive search, so the goal is the guarantee of the printed Algorithm 1 for every order. Running time is not formalized: the algorithm evaluates $f$ on four sets per element, $n$ elements in all. Theorem II.3 requires $f(OPT) > 0$, without which $f \equiv 0$ would satisfy it.
• Needed infrastructure: elementary lemmas on List.foldl over List.take, on membership in the states of the run, and on telescoping sums over $1 \le i \le n$. A reusable lemma "the run keeps $X_i \subseteq Y_i$ and decides exactly $u_1, \dots, u_i$" would serve all three missions of this paper. Contributions of proofs of any milestone, of the goal from the milestones, and of the tight instance (e.g. the paper's five-vertex directed cut function) are welcome.

Selected references

• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, FOCS 2012. https://doi.org/10.1109/FOCS.2012.73 (journal version: SIAM J. Comput. 44(5), 2015, https://doi.org/10.1137/130929205)
• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-monotone Submodular Functions, SIAM J. Comput. 40(4), 2011. https://doi.org/10.1137/090779346
• S. Oveis Gharan, J. Vondrák, Submodular Maximization by Simulated Annealing, SODA 2011. https://doi.org/10.1137/1.9781611973082.83
• M. Feldman, J. Naor, R. Schwartz, Nonmonotone Submodular Maximization via a Structural Continuous Greedy Algorithm, ICALP 2011. https://doi.org/10.1007/978-3-642-22006-7_29

Motivation

Weighted sums of dependent random variables occur when the weights change with the observation horizon. Even if each random variable is bounded and centered, allowing the weights in row $n$ to be chosen anew makes an almost-sure statement about all large $n$ different from a bound on a single finite sum. Kazuo Azuma's 1967 paper treats this situation under a finite-product moment condition called class [M]. Its first main theorem bounds every row of an arbitrary real triangular array at the scale given by that row's Euclidean norm and $\log n$.

The condition is useful because it allows dependence. The paper notes that bounded martingale differences provide examples, but Theorem 1 is stated directly for class [M], without introducing a filtration in the result. The conclusion therefore records the property of the random variables actually used by this part of the paper, rather than restricting the mission to one familiar source of examples. Azuma, §1 and Theorem 1.

Setting

Fix a probability space $(\Omega,\mathcal A,P)$. Let $x_1,x_2,\ldots$ be real measurable random variables. They form a bounded multiplicative system with unit bounds if $|x_k|\le1$ almost surely for every $k\ge1$, and

$$E\!\left[\prod_{k\in S}x_k\right]=0 \quad\text{for every nonempty finite }S\subseteq\{1,2,\ldots\}.$$

The indices in $S$ are distinct. Taking a singleton shows $E[x_k]=0$; taking sets of two, three, or more indices imposes the full condition used in the paper. Pairwise zero correlations by themselves do not state class [M]. All bounds and moment conditions are for the positive indices, so $x_0$ is outside the mathematical sequence. Azuma, p. 357, property [M].

For each $n\ge1$, choose real coefficients $a_{n1},\ldots,a_{nn}$. There is no relation required between different rows. Define the weighted sum $T_n$ and its weight norm $B_n$ by

$$T_n=\sum_{k=1}^{n}a_{nk}x_k, \qquad B_n=\left(\sum_{k=1}^{n}a_{nk}^{2}\right)^{1/2}.$$

Both definitions use the source's 1-based indices. A row of zero weights has $B_n=0$ and $T_n=0$ almost surely; such rows remain within the theorem. Azuma, p. 359, §3.

Formalization targets

The goal is Theorem 1, display (3.1): for every bounded multiplicative system and every real triangular array,

$$\limsup_{n\to\infty} \frac{|T_n|}{\sqrt{2B_n^2\log n}}\le1 \qquad P\text{-almost surely}.$$

The normalizing constant is exactly $2$, and the upper bound is exactly $1$. The mission does not assume that $B_n$ grows, converges, or stays positive. In Lean, the target is stated as the equivalent operational bound: for each $\delta>0$, almost every outcome eventually satisfies $|T_n|\le(1+\delta)\sqrt{2B_n^2\log n}$. This includes zero-weight rows without assigning a meaning to a real quotient $0/0$.

The milestone list follows results displayed in the paper: the corrected convexity inequality (2.2), Lemma 1's exponential moment estimate (2.1), the exponential estimate in the proof of Theorem 1 with its factor $2$, and the almost-sure finite exponential series on the next page. Lemma 1 gives, for arbitrary real $b_1,\ldots,b_n$ and $t\in\mathbb R$,

$$E\exp\!\left(t\sum_{k=1}^{n}b_kx_k\right) \le \exp\!\left(\frac{t^2}{2}\sum_{k=1}^{n}b_k^2\right).$$

The paper prints (2.2) with a missing factor $b_{nk}$ in its linear term. The mission records the printed text as provenance and states the corrected inequality in Lean; the printed version fails already when $b_{nk}=2$ and $x_k=t=1$. Azuma, pp. 357–360.

Significance

Theorem 1 turns an exponential moment bound for each finite weighted sum into a single almost-sure assertion along an entire triangular array. It gives a scale that adapts to the actual coefficients in each row: two arrays with different row norms receive different bounds, while no regularity across rows is required. The result is also the starting point for the weighted strong-law corollaries that follow it in the paper. Azuma, Theorem 1 and Corollary 1.

The mathematical theorem has been proved since 1967. This mission's remaining work is a machine-checked Lean proof of the exact theorem and its listed intermediate statements. A complete development would add reusable formal statements for bounded multiplicative systems and for their finite exponential moments. Those objects could support later work on dependent sums without importing a filtration or a stronger independence assumption. The proposal statements compile as open goals; compilation alone does not supply proofs.

Difficulty

The usual first step for independent bounded variables is to factor the exponential moment into one-variable expectations. Class [M] does not assume independence, so that factorization is unavailable. The condition controls every product with distinct indices, while allowing other dependence. The almost-sure conclusion must also hold when the coefficients change arbitrarily with $n$: bounds that depend on one fixed row do not by themselves settle what happens for all sufficiently large rows. Finally, rows with $B_n=0$ require a statement that preserves the theorem rather than excluding them by an added positivity hypothesis.

Formalization scope

The Lean development represents the probability law by a measure $\mu$ with IsProbabilityMeasure μ, and a random sequence by $x:\mathbb N\to\Omega\to\mathbb R$. It uses measurable variables and states the unit bound almost surely at every positive index. The class [M] predicate quantifies over every nonempty finite set of positive indices; no conditional expectations, filtration, symmetry, or independence hypotheses enter Theorem 1. Finite products and finite weighted sums use ordinary real multiplication and Finset.Icc 1 n. The triangular weights have type $\mathbb N\to\mathbb N\to\mathbb R$, and only entries with $1\le k\le n$ contribute.

The norm $B_n$ is the nonnegative real square root of the sum of squared weights. Real.log is zero at $n=0$ and $n=1$ in Lean, but the target is eventually quantified, so its asymptotic content concerns large $n$. The exponential estimate is stated for $n\ge1$. If $B_n=0$, Lean's total division returns zero in the exponent's quotient; all weights in that row are zero, making this extension valid. In the almost-sure series, the term at index zero is set to zero. The source's limsup is represented by eventual inequalities for every positive excess, avoiding a real-valued limsup default on unbounded sequences.

The definition of class [M] includes every finite product, including singletons; replacing it by pairwise orthogonality would change the theorem. Measurability and the almost-sure unit bounds ensure that the finite products and the exponential functions in Lemma 1 are integrable, so their Lean integrals represent expectations. Contributions toward proofs of the corrected convexity bound, the moment estimate, the exponential series, and the final almost-sure step are all within scope. The finite-product predicate and the exponential estimate are reusable beyond this mission.

Selected references

• Kazuo Azuma, Weighted sums of certain dependent random variables, Tôhoku Mathematical Journal 19 (1967), 357–367. DOI: 10.2748/tmj/1178243286.

Motivation

A learning algorithm generalizes when its error on fresh data is close to its error on the training sample. Bousquet and Elisseeff (JMLR 2, 2002) showed that a single property of the algorithm, uniform stability, controls this gap with exponential concentration: if removing any one example from a training set of size $m$ changes the loss of the output at every point by at most $\beta$, the generalization error exceeds the empirical error by roughly $2\beta + (4m\beta + M)\sqrt{\ln(1/\delta)/(2m)}$ with probability $1-\delta$ (their Theorem 12). The bound is useful only when $\beta = O(1/m)$, and the second half of the paper identifies algorithms with that rate: Tikhonov regularization in a reproducing kernel Hilbert space (Theorem 22), and relative-entropy regularization of mixtures (Theorem 24), the subject of this mission.

Mixtures arise whenever a learner outputs a distribution over a parametric base class instead of a single hypothesis: Bayesian posterior averaging, Gibbs and randomized classifiers, exponential weights. Regularizing by the relative entropy to a prior is the maximum-a-posteriori reading of these procedures, and Theorem 24 is one of the earliest results showing that such posteriors are uniformly stable with rate $1/(\lambda m)$. The same mechanism (entropic regularization, stability through Pinsker's inequality) reappears in PAC-Bayesian analysis and in the stability of exponential-weights methods.

Setting

Let $\Theta$ be a measurable space with a reference measure $\nu$, and write $d\theta$ for integration against $\nu$. A base class $\mathcal H = \{h_\theta : \theta \in \Theta\}$ is indexed by $\Theta$, and $r(h_\theta, z) \in [0, M]$ is the loss of the base hypothesis $h_\theta$ at an example $z \in Z$.

The algorithm outputs a density $g$ with respect to $\nu$: a measurable, nonnegative, integrable $g : \Theta \to \mathbb R$ with $\int_\Theta g\,d\theta = 1$. $F$ denotes the set of all densities. A density is scored by the averaged loss

$$\ell(g, z) = \int_\Theta r(h_\theta, z)\, g(\theta)\, d\theta \qquad (28),$$

the expected loss of a randomized predictor that draws $h_\theta$ from $g$. The relative entropy of $g$ to $g'$ is

$$K(g, g') = \int_\Theta g(\theta) \ln \frac{g(\theta)}{g'(\theta)}\, d\theta \in [0, \infty],$$

with $K(g, g') = +\infty$ when $g\,\nu$ is not absolutely continuous with respect to $g'\,\nu$ or the integrand is not integrable.

Fix a prior $f_0 \in F$, a parameter $\lambda > 0$, and a training set $S = (z_1, \dots, z_m)$. The algorithm returns a minimizer over $F$ of

$$R_r(g) = \frac1m \sum_{j=1}^m \ell(g, z_j) + \lambda K(g, f_0) \qquad (29).$$

For an index $i$, the truncated objective is $R_r^{\setminus i}(g) = \frac1m \sum_{j \ne i} \ell(g, z_j) + \lambda K(g, f_0)$, and $f^{\setminus i}$ denotes one of its minimizers over $F$.

Formalization targets

Goal: Theorem 24

For every minimizer $f$ of (29), every minimizer $f^{\setminus i}$ of the truncated objective, and every example $z$,

$$|\ell(f, z) - \ell(f^{\setminus i}, z)| \le \frac{M^2}{\lambda m}.$$

Milestones

1. $M$-admissibility of (28) (§5.2.3, p. 518): $|\ell(g,z) - \ell(g',z)| \le M \int_\Theta |g - g'|\,d\theta$.
2. Pinsker's inequality, $L^1$ form (proof of Theorem 24): $\tfrac12 \bigl(\int_\Theta |g - g'|\,d\theta\bigr)^2 \le K(g, g')$ for densities $g, g'$.
3. Lemma 21 (p. 513): for a differentiable convex regularizer $N$ on a vector space and a $\sigma$-admissible loss,

$$d_N(f, f^{\setminus i}) + d_N(f^{\setminus i}, f) \le \frac{1}{\lambda m}\Bigl(\ell(f^{\setminus i}, z_i) - \ell(f, z_i) - d_{\ell(\cdot, z_i)}(f^{\setminus i}, f)\Bigr) \le \frac{\sigma}{\lambda m}|\Delta f(x_i)|.$$

4. Bregman divergence of the relative entropy (proof of Theorem 24): $d_{K(\cdot, f_0)}(g, g') = K(g, g')$.
5. $L^1$ displacement bound (proof of Theorem 24):

$$\int_\Theta |f - f^{\setminus i}|\,d\theta \le \frac{M}{\lambda m}.$$

Significance

Theorem 24 places entropy-regularized posteriors among the algorithms to which the paper's exponential generalization bound applies: combined with Theorem 12 it gives, for the averaged loss, a deviation of order $M^2/(\lambda m) + (M^2/\lambda + M)\sqrt{\ln(1/\delta)/m}$. The proof also yields the $L^1$ bound $\int |f - f^{\setminus i}| \le M/(\lambda m)$, which by itself gives classification stability $M/(\lambda m)$ for base hypotheses with values in $\{-1, 1\}$ (remark after Theorem 24, p. 518).

The result is proved in the paper; no machine-checked proof is known to exist. A formalization produces reusable pieces that Mathlib does not have: Pinsker's inequality for densities in $L^1$ form (Mathlib has the Kullback–Leibler divergence InformationTheory.klDiv, but not Pinsker), the Bregman identity for the relative entropy, and a stability statement for minimizers over a space of probability densities.

Difficulty

The paper derives Theorem 24 from Lemma 21, which is stated for a regularizer that is defined and differentiable on a vector space. The relative entropy $K(\cdot, f_0)$ is defined only on the convex set of densities and is not differentiable at densities that vanish on a set of positive measure, so the general lemma does not literally apply, and the identity $d_{K(\cdot,f_0)} = K$ needs integrability conditions that the page does not state. A complete proof of the goal must either justify that application on the set of densities, or work directly with the minimizers, which requires identifying them and handling the $+\infty$ values of $K$. Pinsker's inequality itself requires a separate argument at the level of general measures.

Formalization scope

• Densities are IsDensity ν g: measurable, nonnegative, integrable, total mass one, with respect to a σ-finite reference measure ν. The integral $d\theta$ is always against ν, never Lebesgue measure.
• The base loss is r : Θ → Z → ℝ, measurable in θ, with 0 ≤ r ≤ M; the paper's costs are nonnegative (p. 502).
• $K$ is InformationTheory.klDiv of the measures g · ν and g' · ν, in ℝ≥0∞. The objectives (29) and its truncation take values in ℝ≥0∞. A formalization that converts $K$ to a real number with toReal would send $K = +\infty$ to $0$ and make the worst densities minimizers; that reading is excluded.
• The minimizers are given as hypotheses: f minimizes (29) and f' minimizes the truncated objective over all densities, for the given S : Fin m → Z and i : Fin m.
• Corrected reading of the algorithm on $S^{\setminus i}$. The goal is stated in the pairwise form of the paper's proof: $f^{\setminus i}$ minimizes the truncated objective with factor $1/m$, the analogue of (20), not (29) run on the $m-1$ points of $S^{\setminus i}$ with factor $1/(m-1)$.
• Corrected display. The objective displayed before Theorem 24 has $\ell(g, z)$ inside the sum; (29) has $\ell(g, z_i)$, which is used.
• Lemma 21 is stated as printed, in its differentiable case, on a real normed space whose elements act as functions on $X$ through a linear map; the goal does not instantiate it. The Bregman identity is stated with the explicit gradient $\ln(g'/f_0) + 1$, for $f_0, g' > 0$, finite $K(g, f_0)$, $K(g', f_0)$, and integrable $g \ln(g'/f_0)$.

Contributions welcome: proofs of Pinsker's inequality for klDiv (reusable far beyond this mission), of the Bregman identity, of Lemma 21, and of the goal by any route.

Selected references

• O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
• T. M. Cover and J. A. Thomas, Elements of Information Theory, Wiley, 1991 (Pinsker's inequality). https://doi.org/10.1002/0471200611
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970 (Bregman divergences, Appendix C of the paper). https://doi.org/10.1515/9781400873173

Why finite-horizon reinforcement learning needs a variance-sensitive bound

An agent can learn to act in an unknown environment by repeatedly running a finite episode, observing the states reached after its actions, and updating its model of the environment. The agent must trade off rewards in the current episode against information that may improve later decisions. A regret bound measures the cumulative value lost relative to an optimal policy that knows the true transition probabilities. Its dependence on the number of states, actions, episode steps, and interactions says how much exploration that uncertainty can force.

Azar, Osband, and Munos study this question for a finite-horizon Markov decision process with known, bounded rewards and an unknown, stationary transition kernel. Their UCBVI algorithm estimates action values from observed transitions and adds an exploration bonus. Their second version, UCBVI-BF, uses the empirical variance of the next-state value in that bonus. Their Theorem 2 gives an explicit high-probability regret bound whose leading dependence on the horizon is smaller than the bound they give for the simpler UCBVI-CH bonus. The paper states that, in a sufficiently long-run regime, its leading order matches the cited lower-bound scale up to logarithmic factors. This mission targets the explicit theorem, including its lower-order terms, rather than only that asymptotic comparison.

The MDP, interaction, and algorithm

Let $\mathcal S$ and $\mathcal A$ be nonempty finite state and action sets with cardinalities $S$ and $A$. A stationary transition kernel $P(y\mid x,a)$ is a probability distribution on next states $y$ for every current state $x$ and action $a$. The reward $R(x,a)$ is deterministic, known to the learner, and lies in $[0,1]$. These are the conditions of Assumption 1 and §2. Episodes have $H\ge1$ steps; $K$ episodes comprise $T=KH$ interactions.

A policy $\pi$ chooses an action for each state and step. Its value $V_h^\pi(x)$ is the expected reward from step $h$ through the final step when the state at $h$ is $x$; the terminal value is $V_{H+1}^\pi=0$. The optimal value $V_h^*(x)=\sup_\pi V_h^\pi(x)$ ranges over all deterministic policies of this form. At the start of episode $k$, the environment may choose the initial state using the completed episodes. The learner then fixes a policy $\pi_k$, observes transitions during the episode, and updates counts for the next episode. Its regret is

$$\operatorname{Regret}(K)=\sum_{k=1}^{K}\bigl(V_1^*(x_{k,1})-V_1^{\pi_k}(x_{k,1})\bigr).$$

For each state-action pair, $N_k(x,a,y)$ counts transitions to $y$ in episodes before $k$, and $N_k(x,a)=\sum_yN_k(x,a,y)$. When the latter is positive, $\widehat P_k(y\mid x,a)=N_k(x,a,y)/N_k(x,a)$. The count $N'_{k,h}(y)$ records previous episodes whose state at step $h$ was $y$. Algorithms 2 and 4 compute optimistic $Q_{k,h}$ backward from zero terminal value, take a minimum with the previous episode's $Q$ estimate and with $H$, and choose a maximizing action at every state. Previously unseen pairs receive $Q_{k,h}=H$. The Bernstein–Freedman bonus uses the empirical variance of $V_{k,h+1}$ under $\widehat P_k$ and an additional term based on $N'_{k,h+1}$; the algorithm uses $L_{\rm alg}=\ln(5SAT/\delta)$.

Formalization targets

The goal is Theorem 2 on p. 5. For any MDP and interaction described above and every $\delta>0$, write $L=\ln(5HSAT/\delta)$. The target is the exact bad-event form of the printed high-probability bound:

$$\Pr\!\left\{\operatorname{Regret}(K)>30HL\sqrt{SAK}+2500H^2S^2AL^2+4H^{3/2}\sqrt{KL}\right\}\le\delta.$$

The milestone list contains three empirical-transition deviations from the proof of Lemma 1: Eq. (9) for a value-weighted transition error, the displayed count bound before Eq. (11), and Eq. (12) for the full transition row's $\ell_1$ error. It also contains Lemma 2's variance comparison and Eq. (26), which relates cumulative conditional next-value variance to the variance of an episode return. These are source-indexed targets, with their printed constants retained.

What the result and its formalization supply

The theorem gives a quantitative guarantee for a particular executable decision rule: its regret grows sublinearly in $K$ in the leading term, with explicit dependence on $S$, $A$, and $H$. The result lets one compare the horizon dependence of a variance-sensitive bonus with a value-agnostic bonus under the same finite-horizon model. It also fixes which logarithm belongs in the algorithm and which appears in the reported bound; replacing either changes the claim.

A formal proof would connect a fully specified adaptive interaction to its finite probability law, empirical counts, backward value iteration, and the stated high-probability conclusion. The local prior-art search found reusable transition-kernel vocabulary and general concentration tools, but no published formal statement of this exact UCBVI-BF algorithm or theorem. The mission's finite path and variance definitions can also support other episodic reinforcement-learning bounds that use conditional variance.

Where the difficulty lies

The bonus is computed using a value function that itself depends on earlier observations and the same episode's backward recursion. A concentration inequality for a fixed transition row and a fixed test function therefore does not directly control every value estimate encountered by the algorithm. The number of samples in a row is also random and changes with the learner's past actions. The regret compares a policy's value at an environment-chosen initial state with a supremum over all policies, while the learner's greedy action must be defined at states it never visits. These dependencies are the central obstacle to turning local concentration statements into the episode-level bound.

Formalization scope and conventions

The Lean model uses finite sums rather than measure theory. A published predicate supplies the stationary, real-valued transition kernel; a local MDP adds the known deterministic reward. State and action types are finite and nonempty. Policies are deterministic and depend on the step. The supremum defining $V^*$ ranges over their finite function type. A theorem quantifies over every maximizing tie-breaking rule and every initial-state rule that reads only completed episodes. The probability of an event is constructed as a sum over finite outcome sequences, each weighted by the product of true transition probabilities. Counts use all past transitions and no current or future outcomes. These choices rule out a trivialization that assumes the desired law or optimizes over an unbounded class of arbitrary functions.

Lean indexes the $H$ steps from zero, while the paper indexes them from one. The last observed next state is kept because Algorithm 4 counts states at the terminal index $H+1$. At $N'_{k,h+1}(y)=0$, Algorithm 4's quotient is interpreted as infinite and the capped term is $H^2$; Lean's ordinary division by zero would incorrectly produce zero. The algorithm uses $L_{\rm alg}=\ln(5SAT/\delta)$, while Theorem 2's bound uses $L=\ln(5HSAT/\delta)$. For Eq. (26), the appendix ends its sums at $H-1$ under a shifted terminal convention; the local statement includes all $H$ reward steps and the terminal value $V_{H+1}=0$ used by Algorithm 2. The milestone text remains the printed text. The count milestone is the display before Eq. (11), since Eq. (11) drops a factor of $2$ under the square root present in that display.

Theorem 2 retains its printed $2500H^2S^2AL^2$ term. The appendix's displayed Lemma 13 calculation does not reproduce that second-order constant when propagated to Lemma 14; this is a source proof gap, not a hypothesis of the theorem. Work on the probability normalization, random-count concentration, adaptive value estimates, variance identity, and a valid route to the printed explicit constants is welcome. A proof with altered constants or an asymptotic-only conclusion would be a different target.

Selected references

• M. G. Azar, I. Osband, and R. Munos, Minimax Regret Bounds for Reinforcement Learning, arXiv:1703.05449v2, 2017. Preprint.

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$:

• Schnirelmann (1930s): some finite $k$, by elementary methods.
• Vinogradov (1937): every sufficiently large odd integer is a sum of three primes.
• Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
• Tao (2014): at most five primes. (arXiv:1201.6656)
• Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's first proved value, $100\,001$, came from Schnirelmann's method with every constant written out. This entry records a sharper value, $351$, from the same elementary circle of ideas.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset of primes summing to $n$ with at most $k$ elements counted with multiplicity. The Schnirelmann density of $A \subseteq \mathbb{Z}_{\ge 0}$ is $\sigma(A) = \inf_{N \ge 1} |A \cap \{1, \dots, N\}|/N$ (Mathlib: schnirelmannDensity).

Formalization target

Goal

$$\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 351,\ \textstyle\sum s = n.$$

This is the campaign template with the value $351$ filled in. The source proves the stronger statement that every odd $n \ge 703$ is a sum of exactly $351$ primes; the at-most form for all odd $n > 1$ follows.

How the bound arises

It uses the same density estimate as the companion $485$ entry, $\sigma(A) \ge 1/175$ for $A = B + B$ with $B = \{(p-3)/2 : p \text{ odd prime}\}$ (explicit Selberg sieve, weighted first moment, eighth moment of the singular-series factor, Hölder). It then replaces Schnirelmann's sumset inequality by Mann's theorem, $\sigma(D + E) \ge \min\{1, \sigma(D) + \sigma(E)\}$ for sets containing $0$:

1. Mann's theorem gives $175A = \mathbb{Z}_{\ge 0}$, so $350B = \mathbb{Z}_{\ge 0}$.
2. For odd $n \ge 3K = 1053$, write $(n - 3K)/2$ as a sum of $350$ elements of $B$ and add one more $3$, giving $K = 351$ primes.
3. For $703 \le n < 1053$, use $n - 2K$ threes and $3K - n$ twos.

Significance

The bound is far weaker than Tao's $5$ or Helfgott's $3$, but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from $100\,001$. Reusable components:

1. Explicit Chebyshev-type lower bound for $\pi(y)$.
2. Explicit Selberg upper-bound sieve for $r(s)$ with threshold $e^{100}$.
3. The eighth-moment bound $\sum_{s \le x} C(s)^8 \le 800\,000\,x$.
4. Mann's theorem ($\alpha\beta$ theorem) on Schnirelmann density.

Formalization scope

The Lean statement is the campaign template verbatim with $351$ in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.

Selected references

• P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
• K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
• O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
• T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
• H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
• Explicit improvement of the $100\,001$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $351$; not peer reviewed.

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$:

• Schnirelmann (1930s): some finite $k$, by elementary methods.
• Vinogradov (1937): every sufficiently large odd integer is a sum of three primes.
• Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
• Tao (2014): at most five primes. (arXiv:1201.6656)
• Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's first proved value, $100\,001$, came from Schnirelmann's method with every constant written out. This entry records a sharper value, $485$, from the same elementary circle of ideas.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset of primes summing to $n$ with at most $k$ elements counted with multiplicity. The Schnirelmann density of $A \subseteq \mathbb{Z}_{\ge 0}$ is $\sigma(A) = \inf_{N \ge 1} |A \cap \{1, \dots, N\}|/N$ (Mathlib: schnirelmannDensity).

Formalization target

Goal

$$\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 485,\ \textstyle\sum s = n.$$

This is the campaign template with the value $485$ filled in. The source proves the stronger statement that every odd $n \ge 971$ is a sum of exactly $485$ primes; the at-most form for all odd $n > 1$ follows.

How the bound arises

It keeps the explicit Selberg sieve and Schnirelmann's original sumset inequality from the $100\,001$ entry, and improves only the density estimate:

1. Lower sieve threshold. With $z = \sqrt{s}/(\log s)^2$ the sieve gives $r(s) \le 13\,C(s)\,s/(\log s)^2$ for even $s \ge e^{100}$, where $C(s) = \prod_{p \mid s}\bigl(1 + p/(p-1)^2\bigr)$.
2. Weighted first moment. Counting over the whole triangle $p + q \le x$ and weighting by $(\log s)^2/s$ gives $\sum_{e^{100} < s \le x} r(s)(\log s)^2/s \ge \tfrac{43}{100}x$ for $x \ge e^{200}$.
3. Eighth moment of $C$. An Euler-product estimate (primes $3, 5, 7$ handled individually, the tail bounded at once) gives $\sum_{s \le x,\, 2 \mid s} C(s)^8 \le 800\,000\,x$.
4. Hölder instead of Cauchy–Schwarz. This yields $\#\{s \le x : r(s) > 0\} \ge x/345$ for $x \ge e^{200}$, and with Chebyshev's bound for smaller scales, $\sigma(A) \ge 1/175$ for $A = B + B$, $B = \{(p-3)/2\}$.
5. Schnirelmann's inequality with $m = 121$ (since $(174/175)^{121} < 1/2$) gives $242A = \mathbb{Z}_{\ge 0}$, hence $K = 4m + 1 = 485$.

Only Chebyshev-type prime bounds, the Selberg upper-bound sieve, Hölder's inequality and Schnirelmann's inequality are used.

Significance

The bound is far weaker than Tao's $5$ or Helfgott's $3$, but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from $100\,001$. Reusable components:

1. Explicit Chebyshev-type lower bound for $\pi(y)$.
2. Explicit Selberg upper-bound sieve for $r(s)$ with threshold $e^{100}$.
3. The eighth-moment bound $\sum_{s \le x} C(s)^8 \le 800\,000\,x$.
4. Schnirelmann's inequality $\sigma(D+E) \ge \sigma(D)+\sigma(E)-\sigma(D)\sigma(E)$.

Formalization scope

The Lean statement is the campaign template verbatim with $485$ in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.

Selected references

• P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
• K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
• O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
• T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
• H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
• Explicit improvement of the $100\,001$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $485$; not peer reviewed.

Motivation

Schnirelmann showed around 1930, by elementary means, that some absolute constant $k$ makes every integer $n > 1$ a sum of at most $k$ primes. For odd $n$:

• Schnirelmann (1930s): some finite $k$, by elementary methods.
• Vinogradov (1937): every sufficiently large odd integer is a sum of three primes.
• Ramaré (1995): every even integer is a sum of at most six primes, so every odd $n > 1$ is a sum of at most seven. (Ann. Sc. Norm. Super. Pisa, 1995)
• Tao (2014): at most five primes. (arXiv:1201.6656)
• Helfgott (2013): every odd $n > 5$ is a sum of three primes. (arXiv:1312.7748)

The campaign's first proved value, $100\,001$, came from Schnirelmann's method with every constant written out. This entry records a sharper value, $973$, from the same elementary circle of ideas.

Setting

A representation of $n$ as a sum of at most $k$ primes is a finite multiset of primes summing to $n$ with at most $k$ elements counted with multiplicity. The Schnirelmann density of $A \subseteq \mathbb{Z}_{\ge 0}$ is $\sigma(A) = \inf_{N \ge 1} |A \cap \{1, \dots, N\}|/N$ (Mathlib: schnirelmannDensity).

Formalization target

Goal

$$\forall n \in \mathbb{N},\quad n \text{ odd},\ n > 1 \implies \exists\, s \text{ multiset of primes},\ |s| \le 973,\ \textstyle\sum s = n.$$

This is the campaign template with the value $973$ filled in. The source proves the stronger statement that every odd $n \ge 1947$ is a sum of exactly $973$ primes; the at-most form for all odd $n > 1$ follows.

How the bound arises

It keeps the explicit Selberg sieve and Schnirelmann's original sumset inequality from the $100\,001$ entry, and improves the density estimate:

1. Lower sieve threshold. With $z = \sqrt{s}/(\log s)^2$ the sieve gives $r(s) \le 13\,C(s)\,s/(\log s)^2$ for even $s \ge e^{100}$.
2. Weighted first moment of at least $\tfrac{43}{100}x$ for $x \ge e^{200}$.
3. Fourth moment of $C$. An Euler-product estimate gives $\sum_{s \le x,\, 2\mid s} C(s)^4 \le 400\,x$.
4. Hölder then yields $\sigma(A) \ge 1/350$ for $A = B + B$, $B = \{(p-3)/2\}$.
5. Schnirelmann's inequality with $m = 243$ (the least $m$ with $(349/350)^m < 1/2$) gives $K = 4m + 1 = 973$.

Significance

The bound is far weaker than Tao's $5$ or Helfgott's $3$, but it rests on an elementary argument with no "sufficiently large" threshold and no prime number theorem, so it is a realistic target for a complete formalization and a large step down from $100\,001$. Reusable components:

1. Explicit Chebyshev-type lower bound for $\pi(y)$.
2. Explicit Selberg upper-bound sieve for $r(s)$.
3. Moment bounds for the singular-series factor $C(s)$.
4. Schnirelmann's inequality $\sigma(D+E) \ge \sigma(D)+\sigma(E)-\sigma(D)\sigma(E)$.

Formalization scope

The Lean statement is the campaign template verbatim with $973$ in place of the value. Mathlib already has schnirelmannDensity, the Λ² Selberg sieve setup (Mathlib/NumberTheory/SelbergSieve.lean) and central-binomial bounds.

Selected references

• P. Pollack, Not Always Buried Deep, AMS, 2009, Chapter 6, §6. https://www.pollack-math.net/NABDofficial.pdf
• K. S. Kedlaya, Notes on Analytic Number Theory, Chapter 13, "The Selberg sieve". https://kskedlaya.org/ant/chap-selberg.html
• O. Ramaré, On Šnirel'man's constant, Ann. Sc. Norm. Super. Pisa (4) 22 (1995), 645–706.
• T. Tao, Every odd number greater than 1 is the sum of at most five primes, Math. Comp. 83 (2014). https://arxiv.org/abs/1201.6656
• H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. https://arxiv.org/abs/1312.7748
• Explicit improvement of the $100\,001$ constant (unpublished AI-assisted calculation, October 2026). Source of the constant $973$; not peer reviewed.

Motivation

Optimization problems with orthonormality constraints arise throughout numerical linear algebra and its applications: computing a few eigenvectors or singular vectors, Procrustes problems in statistics and shape analysis, orthogonal factor rotation, independent component analysis, and the orthogonality constraints of electronic-structure calculations. The feasible set of such a problem is the Stiefel manifold of orthonormal $m$-frames in $\mathbb R^n$. Riemannian optimization algorithms on this manifold (Riemannian gradient, Newton and trust-region methods; see Absil, Mahony and Sepulchre, Optimization Algorithms on Matrix Manifolds, 2008) take a step in a tangent direction and then need a retraction: a map that brings the updated point back onto the manifold while agreeing with the geometry to first order.

The most natural way to come back to a constraint set is to take the nearest point. P.-A. Absil and J. Malick, Projection-like retractions on matrix manifolds (SIAM J. Optim. 22(1), 2012; the mission follows the authors' version, HAL hal-00651608v2), show in their Proposition 3.2 that the metric projection onto a smooth submanifold yields a retraction, and then work out the projection explicitly for several matrix manifolds. For the Stiefel manifold, their Proposition 3.4 identifies the projection with a factor of the singular value decomposition, equivalently with the orthonormal factor of the polar decomposition. The paper notes that this result was mentioned without proof in Higham's survey of matrix nearness problems, and gives a proof along the lines of Horn and Johnson, Matrix Analysis, §7.4.

Section 4.5 of the same paper treats a second, "orthographic" retraction on the Stiefel manifold, which corrects a tangent step by a normal vector instead of projecting; for the orthogonal group $\mathbf O_n$ (the case $m=n$) it admits a closed form through a matrix square root (Proposition 4.12).

Setting

Fix natural numbers $1\le m\le n$. Matrices are real, and $\mathbb R^{n\times m}$ carries the Frobenius norm

$$\|X\|^2=\sum_{i,j}X_{ij}^2=\operatorname{trace}(X^\top X).$$

The Stiefel manifold is

$$V_{n,m}=\{X\in\mathbb R^{n\times m}:\ X^\top X=I_m\},$$

the set of matrices with orthonormal columns; $V_{n,n}$ is the orthogonal group $\mathbf O_n$.

The singular values of $X$ are $\sigma_1(X)\ge\sigma_2(X)\ge\dots\ge\sigma_{\min\{n,m\}}(X)\ge0$, the square roots of the eigenvalues of $X^\top X$. A singular value decomposition of $X$ is a factorization $X=U\Sigma V^\top$ with $U=[u_1,\dots,u_n]\in\mathbf O_n$, $V=[v_1,\dots,v_m]\in\mathbf O_m$, and $\Sigma\in\mathbb R^{n\times m}$ zero off its diagonal, with nonnegative nonincreasing diagonal entries. For $\bar X\in V_{n,m}$ every singular value equals $1$; in particular $\sigma_m(\bar X)=1$.

A projection of $X$ onto $V_{n,m}$ is a point $Y\in V_{n,m}$ with $\|X-Y\|\le\|X-Z\|$ for all $Z\in V_{n,m}$. A polar decomposition of $X$ is a factorization $X=WS$ with $W\in V_{n,m}$ and $S\in\mathbb R^{m\times m}$ symmetric positive definite.

Formalization targets

Goal: Proposition 3.4 (p. 10)

Let $\bar X\in V_{n,m}$ and let $X$ satisfy $\|X-\bar X\|<\sigma_m(\bar X)$. For every singular value decomposition $X=U\Sigma V^\top$,

$$\{\,Y:\ Y\text{ is a projection of }X\text{ onto }V_{n,m}\,\}=\Big\{\sum_{i=1}^m u_iv_i^\top\Big\},$$

and $\sum_{i=1}^m u_iv_i^\top$ is the $W$ of the polar decomposition $X=WS$: it is the orthonormal factor of every polar decomposition of $X$, and a polar decomposition with this factor exists.

The statement asserts existence, uniqueness and the closed form of the projection on the whole open ball of radius $\sigma_m(\bar X)$, for whichever singular value decomposition is supplied.

Steps of the proof (milestones)

1. For $Y\in V_{n,m}$: $\|X-Y\|^2=\|X\|^2+m-2\operatorname{trace}(Y^\top X)$.
2. For every $Y\in V_{n,m}$, $\operatorname{trace}(Y^\top X)\le\sum_{i=1}^m\sigma_i$, with equality at $Y=\sum_{i=1}^m u_iv_i^\top$.
3. If $\|X-\bar X\|<\sigma_m(\bar X)$ with $\bar X\in V_{n,m}$, then $X$ has full rank $m$.
4. The polar factor of a full-rank matrix is unique (Horn and Johnson, Theorem 7.3.2).

Further items (§4.5)

$$(S+I)^2=I-\Omega^\top\Omega \tag{4.14}$$

for $X\in\mathbf O_n$, $\Omega$ skew-symmetric and $S$ symmetric with $X+X\Omega+XS\in\mathbf O_n$; and Proposition 4.12,

$$R(X,X\Omega)=X\big(\Omega+\sqrt{I-\Omega^\top\Omega}\big),$$

stated as: $S_+=-I+\sqrt{I-\Omega^\top\Omega}$ is the unique symmetric correction of smallest Frobenius norm.

Significance

Proposition 3.4 makes the projective retraction on the Stiefel manifold computable from one singular value decomposition of an $n\times m$ matrix, and identifies it with the polar factor, which is also what many numerical codes already compute for re-orthonormalization. Combined with Proposition 3.2 of the paper, it yields a second-order-accurate retraction usable in any Riemannian algorithm on $V_{n,m}$. The same statement is the orthogonal Procrustes problem in the special case of a full-rank target: the nearest orthonormal frame to $X$.

The result is classical and proved; the paper's argument is short but cites two external facts (Weyl's perturbation bound for singular values and the uniqueness of the polar decomposition). To our knowledge no machine-checked proof of the nearest-orthonormal-frame property, of the uniqueness of the polar factor, or of the closed form of Proposition 4.12 exists in Mathlib or on this platform. A formalization produces reusable pieces: the trace inequality over the Stiefel manifold, the uniqueness of the polar decomposition, and the full-rank property near $V_{n,m}$, all of which recur in matrix analysis and in the analysis of Riemannian algorithms.

Difficulty

Existence of a nearest point is easy (the Stiefel manifold is compact), and attainment of the trace bound is a direct computation. The content is in two places. First, the bound $\operatorname{trace}(Y^\top X)\le\sum_i\sigma_i$ for every $Y\in V_{n,m}$ requires transporting $Y$ by the orthogonal factors of the singular value decomposition and bounding diagonal entries of a matrix with orthonormal columns. Second, uniqueness does not follow from the trace argument: when $X$ is rank deficient there are many maximizers. Uniqueness needs both a perturbation bound (singular values are 1-Lipschitz in the Frobenius norm, so $\sigma_m(X)>0$ near $\bar X$) and the uniqueness of the polar factor, which in turn rests on the uniqueness of the positive-semidefinite square root of $X^\top X$. Mathlib has singular values of linear maps and the spectral theorem but, at the pinned revision, neither Weyl's inequality for singular values nor the polar decomposition.

For Proposition 4.12, the printed proof compares only two solutions $S_\pm$ of (4.14), while (4.14) has other symmetric solutions (mixed signs of the square roots, or non-diagonal ones on repeated eigenvalues); minimality must be proved against all of them.

Formalization scope

Matrices are Matrix (Fin n) (Fin m) ℝ with the Frobenius norm brought in by open scoped Matrix.Norms.Frobenius. The Stiefel manifold is the set stiefel n m of matrices with Xᵀ * X = 1. Singular values are Mathlib's LinearMap.singularValues of Matrix.toEuclideanLin X, re-indexed to be 1-based as on the page (sv X m is $\sigma_m(X)$). A singular value decomposition is the predicate IsSVD X U S V of display (3.5), and $\sum_{i=1}^m u_iv_i^\top$ is U * E * Vᵀ with E the $n\times m$ rectangular identity (frameOfSVD U V). The projection is the set of nearest points, using the published predicate RandomGradFree.Nonsmooth.IsMetricProjection; "exists and is unique" is equality of that set with a singleton. Positive definiteness is Mathlib's Matrix.PosDef, which over $\mathbb R$ includes symmetry.

Standing assumptions and added hypotheses: $m\le n$ is the page's assumption of §3.3; $0<m$ is added so that $\sigma_m$ is meaningful. The radius is $\sigma_m(\bar X)$ with strict inequality, kept in that form although its value is $1$. Two misprints of the page are corrected in the Lean and kept in the verbatim milestone texts: the display of Proposition 3.4 reads $P_{\mathcal R_r}(X)$ for $P_{V_{n,m}}(X)$, and the distance identity reads $m^2$ for $m$. The uniqueness of the polar factor is stated for positive semidefinite factors under the rank hypothesis, which contains the positive definite case of Proposition 3.4. The matrix square root of §4.5 is defined through Mathlib's spectral theorem; Proposition 4.12 is stated for every admissible symmetric correction, and is vacuous only when no symmetric correction exists.

A trivializing formalization is ruled out: the projection is not taken as a hypothesis or chosen by definition; the goal asserts that the nearest-point set equals the singleton of the explicit matrix, for every singular value decomposition supplied, so neither existence nor uniqueness can be assumed away.

Contributions welcome beyond the stated items: Weyl's inequality $|\sigma_i(X)-\sigma_i(Y)|\le\|X-Y\|$ in Mathlib's singular-value API, existence of a singular value decomposition in the matrix form (3.5), and the polar decomposition with its uniqueness, all reusable well beyond this mission.

Selected references

• P.-A. Absil and J. Malick, Projection-like retractions on matrix manifolds, SIAM J. Optim. 22(1):135–158, 2012. https://doi.org/10.1137/100802529 ; authors' version https://hal.science/hal-00651608v2
• P.-A. Absil, R. Mahony and R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244
• R. A. Horn and C. R. Johnson, Matrix Analysis, Cambridge University Press, 1985 (cited by the paper in its 1989 printing) (Theorem 7.3.2, §7.4). https://doi.org/10.1017/CBO9780511810817
• N. J. Higham, Matrix nearness problems and applications, in Applications of Matrix Theory (M. J. C. Gover and S. Barnett, eds.), Oxford University Press, 1989, pp. 1–27 (cited by the paper as [15, §4]; no DOI).
• A. Edelman, T. A. Arias and S. T. Smith, The geometry of algorithms with orthogonality constraints, SIAM J. Matrix Anal. Appl. 20(2):303–353, 1998. https://doi.org/10.1137/S0895479895290954

Motivation

Blackwell approachability is the vector-payoff analogue of von Neumann's minimax theorem. In a repeated game where each round's outcome is a vector $u(x_t, y_t) \in \mathbb R^d$, a player wants the running average of these vectors to converge to a target set $S$, whatever the opponent does. Blackwell (1956) showed when this is possible, and approachability has since become a standard tool for calibrated forecasting, regret minimization with respect to general benchmarks, and learning in games.

Online linear optimization (OLO) is the problem of choosing points $\theta_t$ in a fixed decision set $\mathcal K$ against a sequence of linear losses $\langle f_t, \cdot\rangle$, with performance measured by regret against the best fixed point in hindsight. Algorithms with regret $o(T)$ — "no-regret" algorithms such as online gradient descent (Zinkevich, 2003) — are among the most studied objects of machine learning.

Abernethy, Bartlett and Hazan (COLT 2011) showed that the two problems are algorithmically equivalent: each can be converted into the other with explicit control of the rates. This mission covers the direction from OLO to approachability.

Timeline:

• 1956: Blackwell proves the approachability theorem for convex sets, via a geometric projection strategy.
• 2003: Zinkevich introduces online gradient descent, a no-regret algorithm for any bounded convex decision set.
• 2009: Even-Dar, Kleinberg, Mannor and Mansour state approachability in the response-satisfiability form (as cited on p. 32 of the 2011 paper).
• 2011: Abernethy, Bartlett and Hazan give the two reductions, with explicit rates, and apply them to efficient calibration.

Setting

A Blackwell instance $(\mathcal X, \mathcal Y, u, S)$ consists of compact convex sets $\mathcal X \subseteq \mathbb R^n$, $\mathcal Y \subseteq \mathbb R^m$, a payoff $u : \mathcal X \times \mathcal Y \to \mathbb R^d$ that is affine in each argument (biaffine), and a closed convex target set $S \subseteq \mathbb R^d$. Write $\mathtt{dist}(z, U) = \inf_{w \in U}\|z - w\|$ for the Euclidean distance to a set, and $B_2(r)$ for the closed Euclidean ball of radius $r$.

A halfspace oracle takes a halfspace $H = \{z : \langle a, z\rangle \le c\}$ and returns a point $\mathcal O(H) \in \mathcal X$; it is valid if for every halfspace $H \supseteq S$, $u(\mathcal O(H), y) \in H$ for all $y \in \mathcal Y$.

A set $X \subseteq \mathbb R^d$ is a cone if $\alpha z \in X$ for all $z \in X$, $\alpha \ge 0$. For $K \subseteq \mathbb R^d$, $\mathtt{cone}(K) = \{\alpha x : \alpha \ge 0, x \in K\}$, and the polar cone of $C$ is $C^0 = \{\theta : \langle \theta, x\rangle \le 0 \ \forall x \in C\}$.

An OLO algorithm $\mathcal L$ maps past loss vectors $(f_1, \dots, f_{t-1})$ to a point $\theta_t \in \mathcal K$, and its regret is

$$\mathrm{Regret}_T = \sum_{t=1}^T \langle f_t, \theta_t\rangle - \min_{\theta \in \mathcal K} \sum_{t=1}^T \langle f_t, \theta\rangle .$$

Algorithm 2 runs $\mathcal L$ on $\mathcal K = S^0 \cap B_2(1)$ when $S$ is a cone: at round $t$ it sets $\theta_t = \mathcal L(f_1, \dots, f_{t-1})$, plays $x_t = \mathcal O(\{z : \langle \theta_t, z\rangle \le 0\})$, observes $y_t \in \mathcal Y$, and feeds $f_t = -u(x_t, y_t)$ back to $\mathcal L$.

When $S$ is compact but not a cone, it is lifted: with $\kappa = \max_{s\in S}\|s\|$ and $\kappa \oplus z \in \mathbb R^{d+1}$ the concatenation, put $u'(x, y) = \kappa \oplus u(x, y)$ and $S' = \mathtt{cone}(\{\kappa\} \times S)$, and run Algorithm 2 on $(\mathcal X, \mathcal Y, u', S')$.

Formalization targets

Goal: Corollary 18 (p. 39)

For a Blackwell instance with $S$ nonempty and compact, any valid halfspace oracle for the lifted instance, any OLO algorithm with values in $\mathcal K' = (S')^0 \cap B_2(1)$, any $T \ge 1$ and any $y_1, \dots, y_T \in \mathcal Y$, the run of Algorithm 2 on the lifted instance satisfies

$$\mathtt{dist}\Big(\frac1T\sum_{t=1}^T u(x_t,y_t), S\Big) \le 2\,\mathtt{dist}\Big(\frac1T\sum_{t=1}^T u'(x_t,y_t), S'\Big) \le \frac2T\,\mathrm{Regret}_T .$$

The bound holds for every $T$ and every adversary, with no rate assumed for $\mathcal L$; a no-regret $\mathcal L$ then gives approachability.

Milestones

1. Lemma 13 (p. 35): for a nonempty convex cone $C$, $\mathtt{dist}(x, C) = \max_{\theta \in C^0 \cap B_2(1)} \langle \theta, x\rangle$.
2. Theorem 17 (p. 38): if $S$ is a cone, Algorithm 2 achieves $\mathtt{dist}\big(\frac1T\sum_t u(x_t,y_t), S\big) \le \mathrm{Regret}(\mathcal L_{\mathcal K}; f_{1:T})/T$.
3. Lemma 14 (p. 35): for nonempty compact convex $\mathcal K$, $\kappa = \max_{\mathcal K}\|\cdot\|$ and $x \notin \mathcal K$, $\mathtt{dist}(\kappa\oplus x, \mathtt{cone}(\{\kappa\}\times\mathcal K)) \le \mathtt{dist}(x, \mathcal K) \le 2\,\mathtt{dist}(\kappa\oplus x, \mathtt{cone}(\{\kappa\}\times\mathcal K))$.

Significance

The result. Corollary 18 turns any no-regret algorithm into an approachability strategy for a compact convex target, provided a valid halfspace oracle is available, with rate $2\,\mathrm{Regret}_T/T$. Combined with online gradient descent it gives an $O(1/\sqrt T)$ approachability rate, and through the choice of OLO algorithm it lets approachability inherit the computational efficiency of online learning. The paper uses this route to build an efficient calibrated forecaster (Section 5). Together with the converse reduction (Theorem 16), it shows that the two problems are equivalent.

Formalizing it. The results are proved in the paper; none of them has been machine-checked. Formalizing them requires the conic duality formula for distances (Lemma 13), a quantitative lifting lemma (Lemma 14) and the bookkeeping of an interactive protocol. The proof of Lemma 14 on the page is a sketch: it refers to an undefined point and uses a triangle-similarity argument, so a complete proof is new work.

Difficulty

The reduction's core is Lemma 13: the distance to a cone is a maximum of a linear function over the polar cone's unit ball. Lemma 13 needs projection onto a cone in Euclidean space; for a non-closed cone the projection may not exist, and the argument must go through the closure. The lifting Lemma 14 is a geometric statement whose page proof relies on a picture and an undefined point, so the factor 2 has no complete written argument. Finally, connecting the average lifted payoff to the lift of the average payoff, and the halfspace guarantee $\langle\theta_t, f_t\rangle \ge 0$ to the regret, requires keeping the round indexing and the oracle's validity domain exactly aligned.

Formalization scope

All spaces are EuclideanSpace ℝ (Fin d). The concatenation $\kappa\oplus z$ lives in EuclideanSpace ℝ (Fin (d+1)) with coordinate 0 equal to $\kappa$, so $\|\kappa\oplus z\|^2 = \kappa^2 + \|z\|^2$; a product type with the sup norm would change every distance and is ruled out. Distances are Metric.infDist. The polar cone uses the paper's sign ($\le 0$), the negative of Mathlib's innerDual. A halfspace is the pair $(a, c)$; a valid oracle must answer every halfspace containing $S$, including $a = 0$, not only the halfspaces the algorithm happens to query. The OLO algorithm is a map from histories Fin t → ℝᴰ with values in $S^0 \cap B_2(1)$ at every history. Rounds are $t = 1, \dots, T$, and the run of Algorithm 2 is given as hypotheses on sequences $\theta, x, f$, which exist and are unique by recursion. The minimum in the regret and $\kappa$ are written as sInf/sSup of images over nonempty compact sets, where they are attained.

Hypotheses added relative to the page: $S \neq \emptyset$ and $T \ge 1$ in the goal; $C \ne \emptyset$ in Lemma 13 (the empty set is a cone under Definition 11 and the identity fails for it); $\mathcal K \ne \emptyset$ in Lemma 14. Corrected misprints, each disclosed in the item's note: "$\mathrm{Regret}_T(\mathcal A)$" in Corollary 18 and (9) denotes the regret of the OLO algorithm $\mathcal L$ on the lifted losses; Lemma 14's "$\mathcal K \subseteq \mathcal H$" has a stray $\mathcal H$; $\kappa$ is the maximal norm of the set, not its diameter. The oracle in the goal is a valid oracle for the lifted instance, which is what applying Algorithm 2 to $(\mathcal X, \mathcal Y, u', S')$ requires.

A formalization in which the oracle is valid only at the run's own queries, the OLO algorithm is unconstrained, the regret's minimum ranges over all of $\mathbb R^{d+1}$, or the middle term of the goal is dropped, is a different statement and is ruled out.

The development needs: the dual formula for the distance to a convex cone, nearest-point projection onto closed convex sets (in Mathlib), compactness of polar-cone slices, and finite sums of biaffine payoffs. The cone layer (Lemma 13) is reusable for the converse direction of the paper and for conic duality generally. Proofs of any milestone, and of the bridge from an oracle for the original instance to one for the lifted instance, are welcome.

Selected references

• J. Abernethy, P. L. Bartlett, E. Hazan, Blackwell Approachability and No-Regret Learning are Equivalent, JMLR W&CP 19 (COLT 2011), pp. 27–46. https://proceedings.mlr.press/v19/abernethy11b.html
• D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific Journal of Mathematics 6(1), 1956, pp. 1–8. https://doi.org/10.2140/pjm.1956.6.1
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, ICML 2003. https://www.aaai.org/Papers/ICML/2003/ICML03-120.pdf