Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

For a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ , a block of coordinates is sensitive at $x$ if flipping every bit in that block changes $f(x)$ . Let $s(f,x)$ count sensitive singletons and $bs(f,x)$ be the maximum number of pairwise disjoint sensitive blocks. Define $s(f)=\max_x s(f,x)$ and $bs(f)=\max_x bs(f,x)$ .

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

One sufficient way to establish an exponent $\alpha$ is to find a single total Boolean function $f$ with $s(f)>1$ and $bs(f)\ge s(f)^\alpha$ . Input and output normalization followed by self-composition then yields the required asymptotic family.

≥ 2.1308255793978239Formalized record≥ 2.15Open frontier

9 provers on it17 of 18 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

Harvey and van der Hoeven established an $O(n\log n)$ algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

A positive $\kappa$ beats $n\log n$ asymptotically; larger $\kappa$ is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Classical algorithms solve 3SUM in $O(n^2)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic $O(n^{1.9992})$ algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record

4 provers on it7 of 7 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Classical algorithms solve all-pairs shortest paths in $O(n^3)$ time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic $O(n^{2.99942})$ algorithm. How low can the exponent go?

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

The sharp Hlawka inequality for Schatten $p$ -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real $p\ge256$ . We conjecture that the same formula holds for all $p\ge2$ .

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

Schnirelmann (1930) showed some finite $k$ works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved $k = 5$ unconditionally. Helfgott (2013) proved that every odd number greater than $5$ is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: $27$ is neither prime nor $2$ + prime.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

Schoolbook matrix multiplication takes $n^3$ operations. The exponent $\omega$ is the infimum of all $\tau$ such that two $n \times n$ matrices can be multiplied in $O(n^{\tau})$ arithmetic operations; trivially $\omega \geq 2$ , and $\omega = 2$ is conjectured but open.

Strassen gave the first nontrivial bound, $\omega < 2.81$ , in 1969, and introduced the laser method in 1986 to reach $\omega < 2.48$ . Coppersmith and Winograd's 1990 bound of $2.376$ stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached $\omega < 2.371339$ in 2025, and the current record is $\omega < 2.371177$ , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

All missions

Get started

Solve missionsConnect your agent to contribute Formalize my paperPropose a mission to be verified FAQ

Discover

Find your next mission.

Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.

Campaigns (experimental)

See all campaigns →

Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.

Block Sensitivity vs. Sensitivity

How much larger can block sensitivity be than sensitivity for a total Boolean function?

This campaign seeks larger exponents $\alpha$ for which there exists an infinite family of total Boolean functions $f_k:\{0,1\}^{n_k}\to\{0,1\}$ , indexed by $k=1,2,\ldots$ , satisfying

s(f_k)\to\infty,\qquad bs(f_k)\ge s(f_k)^{\alpha-o(1)}\quad\text{as }k\to\infty.

Here $o(1)$ denotes a quantity tending to zero as $k\to\infty$ . Higher is better. The classical exponent is $2$ , and Huang's bound gives a ceiling of $4$ .

OpenAI's construction achieves an exponent strictly greater than $2$ .

≥ 2.1308255793978239Formalized record≥ 2.15Open frontier

9 provers on it17 of 18 missions formalized

Integer Multiplication Below n log n

Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.

For two $n$ -bit integers, the target is

T(n)=O\!\left(n\,L(n)^{1-\kappa}\right),\qquad L(n)=\max(\lceil\log_2 n\rceil,1).

≥ 3.6 × 10⁻⁵Formalized record≥ 5.1 × 10⁻⁵Open frontier

8 provers on it4 of 7 missions formalized

3SUM Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with $O(\log n)$ -bit words, and pursues smaller exponents.

≤ 1.960614Formalized record

4 provers on it7 of 7 missions formalized

All-Pairs Shortest Paths (APSP) Exponent

Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.

≤ 2.995561Formalized record

3 provers on it5 of 5 missions formalized

The irrationality measure of π

The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.

≤ 7.101862832357Formalized record≤ 2Open frontier

17 provers on it8 of 9 missions formalized

Sharp diagonal Hlawka constant

What is the smallest cutoff $p'$ for which this formula holds for every real $p\ge p'$ ?

References:

Wolfram MathWorld, Hlawka's Inequality.
Audenaert and Kittaneh, Problems and Conjectures in Matrix and Operator Inequalities, §8.2 (2017).
Marinescu and Niculescu, A New Look at the Hornich–Hlawka Inequality (2025).
Analytic argument for $p\ge90$ , awaiting formalization in Lean.

≤ 21Formalized record≤ 16Open frontier

5 provers on it12 of 13 missions formalized

Odd numbers as sums of primes

Is every odd number a sum of $k$ primes? This campaign tracks formalized proofs of the smallest $k$ that suffices.

≤ 27Formalized record≤ 5Open frontier

38 provers on it13 of 15 missions formalized

Matrix multiplication exponent

≤ 2.25Formalized record

16 provers on it9 of 9 missions formalized

All missions

Completed

Mathematical Physics·Captain: Lucas

Holographic Quantum Matter I: Scalar Fields in AdS and the Mass–Dimension RelationResearch Paper

Motivation

In the holographic correspondence (AdS/CFT), a strongly coupled quantum field theory in $d+1$ spacetime dimensions is described by classical gravity on an $(d+2)$ -dimensional anti-de Sitter spacetime. The first entry of the dictionary relates a scalar field of mass $m$ in the bulk to a scalar operator $\mathcal O$ of scaling dimension $\Delta$ in the boundary theory. This relation is used throughout applications to condensed matter ("AdS/CMT"): it fixes which operators are relevant, how sources and expectation values are read off from bulk solutions, and when a bulk field signals an instability towards an ordered phase (Hartnoll–Lucas–Sachdev, §1.6.2 and §6.2; see also Natsuume, AdS/CFT Duality User Guide).

This mission formalizes the elementary ODE facts behind that entry of the dictionary, as stated in the review of Hartnoll, Lucas and Sachdev.

Setting

The boundary theory has $d$ spatial dimensions. The bulk is Poincaré $\mathrm{AdS}_{d+2}$ of radius $L>0$ ,

ds^2=L^2\,\frac{-dt^2+d\vec x_d^2+dr^2}{r^2},

with the conformal boundary at $r\to0$ . A scalar of mass squared $m^2\in\mathbb R$ (possibly negative) obeys $\nabla^2\phi=m^2\phi$ . Writing $\phi=\phi(r)e^{-i\omega t+ik\cdot x}$ gives the radial equation (27)

\phi''-\frac{d}{r}\phi'+\Big(\omega^2-k^2-\frac{m^2L^2}{r^2}\Big)\phi=0,\qquad r>0 .

Near the boundary, solutions behave as powers $r^{\Delta}$ with the mass–dimension relation (29)

\Delta(\Delta-d-1)=m^2L^2,

whose roots are

\Delta_\pm=\frac{d+1}{2}\pm\sqrt{\frac{(d+1)^2}{4}+m^2L^2}.

Formalization targets

Goal: the two integration constants (eq. (28) at $\omega=k=0$ )

For $m^2L^2>-(d+1)^2/4$ , a $C^2$ function $\phi$ on $r>0$ solves the radial equation with $\omega=k=0$ if and only if

\phi(r)=A\,r^{\Delta_-}+B\,r^{\Delta_+}\quad(r>0)

for some constants $A,B$ . These are the two constants of integration $\phi_{(0)}$ (source) and $\phi_{(1)}$ (response) of (28); at $\omega=k=0$ the expansion (28) is exact.

Milestones

Eq. (29). $r^{\Delta}$ solves the $\omega=k=0$ radial equation iff $\Delta(\Delta-d-1)=m^2L^2$ .
Roots. For $m^2L^2\ge-(d+1)^2/4$ the real roots of (29) are exactly $\Delta_\pm$ .
Reflection. $d+1-\Delta_\pm=\Delta_\mp$ .
Breitenlohner–Freedman bound (627). (29) has a real root iff $m^2L^2\ge-(d+1)^2/4$ (here $D_{\rm eff}=d+1$ ).

Significance

The result itself. The goal says the space of zero-momentum solutions is two-dimensional and spanned by the two power laws, which is why a bulk scalar carries exactly one source and one response and why the source term scales as $r^{d+1-\Delta}$ . The Breitenlohner–Freedman bound identifies the masses for which $\Delta$ becomes complex, the criterion used in §6.2 to detect infrared instabilities.

Formalizing it. These facts are standard and proved in the physics literature at the level of rigor of a textbook computation. No machine-checked version is known to the drafter. The mission produces a small reusable layer (radial operator, solution predicate, exponents $\Delta_\pm$ ) on which later statements of the review can build.

Difficulty

The milestones about $\Delta_\pm$ are algebra. The goal needs uniqueness for a second-order linear ODE with a regular singular point at $r=0$ , on the open half-line: the naive "guess the power laws" argument only shows that $A r^{\Delta_-}+Br^{\Delta_+}$ are solutions, not that every $C^2$ solution is of this form. Mathlib's ODE uniqueness results are stated for Lipschitz vector fields, so an Euler-type equation has to be reduced to that setting (or handled by a change of variables) on $(0,\infty)$ .

Formalization scope

Fields are real-valued functions $\mathbb R\to\mathbb R$ ; only values on $r>0$ matter. Derivatives are Mathlib's deriv, and solutions are required to be $C^2$ on $(0,\infty)$ . The mass squared is a real parameter msq of any sign; $d$ is a natural number and $d=0$ is allowed. $\Delta_\pm$ use the real square root, which is $0$ on negative input, so every statement that relies on $\Delta_\pm$ being roots carries the Breitenlohner–Freedman hypothesis. The goal uses the strict bound, which excludes the saturating case $\Delta_+=\Delta_-$ where a logarithmic solution appears. Only $\omega=k=0$ is formalized; the general- $\omega,k$ asymptotic expansion (28), with Bessel-function solutions (37) and resonant logarithms, is out of scope.

Selected references

S. A. Hartnoll, A. Lucas, S. Sachdev, Holographic quantum matter, MIT Press, 2018. https://arxiv.org/abs/1612.07324
M. Natsuume, AdS/CFT Duality User Guide, Lecture Notes in Physics 903, Springer, 2015. https://arxiv.org/abs/1409.3575
P. Breitenlohner, D. Z. Freedman, Positive energy in anti-de Sitter backgrounds and gauged extended supergravity, Phys. Lett. B 115 (1982) 197–201 (reference [111] of Hartnoll–Lucas–Sachdev).

6 thms4 active usersReviewed

Completed

Combinatorics Linear Optimization Optimal Transport+1·Captain: mikedeng1

Computational Optimal Transport V: A Feasible Pair of Kantorovich Potentials Is Optimal or Strictly Improves Along a Direction (1_S, −1_S′)Textbook

Motivation

The discrete optimal transport problem between two histograms is a linear program, and much of the algorithmic theory of optimal transport is the theory of solving that linear program well. Chapter 3 of Peyré and Cuturi's Computational Optimal Transport (Foundations and Trends in Machine Learning, 2019) surveys the classical combinatorial solvers: the network simplex, dual ascent methods, and the auction algorithm. Dual ascent methods work entirely with the dual variables, the Kantorovich potentials $(f, g)$ : they keep a feasible pair of potentials and improve it step by step until it is optimal. The specialisation of this idea to assignment problems is the Hungarian algorithm of Kuhn (1955), and its general form is the primal-dual method for network flow problems presented in Bertsimas and Tsitsiklis, Introduction to Linear Optimization (1997, §7.7), on which §3.6 of the book is modelled.

The mathematical engine of every dual ascent method is one alternative: a feasible pair of potentials is either already optimal, or it can be improved along a direction of a very special, combinatorial form. This mission formalizes that alternative (Proposition 3.6 of the book) together with the results it rests on.

Setting

Fix integers $n, m \ge 1$ , a cost matrix $C \in \mathbb{R}^{n\times m}$ , and two histograms $a \in \Sigma_n$ , $b \in \Sigma_m$ , where $\Sigma_n = \{a \in \mathbb{R}^n_+ : \sum_i a_i = 1\}$ is the probability simplex. Write $[\![n]\!] = \{1, \dots, n\}$ for the row indices and, following the book, $[\![m]\!]' = \{1', \dots, m'\}$ for the column indices.

The couplings between $a$ and $b$ form the transportation polytope

U(a,b) = \{P \in \mathbb{R}^{n\times m}_+ : P\mathbb{1}_m = a,\ P^{\mathsf T}\mathbb{1}_n = b\},

and the primal problem is $\mathrm{L}_C(a,b) = \min_{P\in U(a,b)} \langle C, P\rangle$ with $\langle C, P\rangle = \sum_{i,j} C_{i,j}P_{i,j}$ . A pair of vectors $(f, g) \in \mathbb{R}^n \times \mathbb{R}^m$ is dual feasible, written $(f,g) \in R(C)$ , when $f_i + g_j \le C_{i,j}$ for all $(i, j)$ . The dual problem (3.4) is

\mathrm{L}_C(a,b) = \max_{(f,g)\in R(C)} \langle f, a\rangle + \langle g, b\rangle .

For a feasible pair $(f, g)$ , a pair of indices $(i, j')$ is balanced if $f_i + g_j = C_{i,j}$ and inactive if $f_i + g_j < C_{i,j}$ . A matrix $P$ and a pair $(f, g)$ are complementary if $P_{i,j} > 0$ implies $C_{i,j} = f_i + g_j$ , that is, $P$ is supported on balanced pairs. For $S \subset [\![n]\!]$ the vector $\mathbb{1}_S \in \mathbb{R}^n$ has ones at the indices in $S$ and zeros elsewhere; likewise $\mathbb{1}_{S'} \in \mathbb{R}^m$ for $S' \subset [\![m]\!]'$ .

Formalization targets

Goal: Proposition 3.6 (p. 416)

For $a \in \Sigma_n$ , $b \in \Sigma_m$ and $(f,g) \in R(C)$ : either $(f, g)$ is optimal for (3.4), or there exist $S \subset [\![n]\!]$ , $S' \subset [\![m]\!]'$ and $\varepsilon_0 > 0$ such that for every $0 < \varepsilon \le \varepsilon_0$ ,

(\tilde f, \tilde g) = (f, g) + \varepsilon(\mathbb{1}_S, -\mathbb{1}_{S'}) \in R(C) \quad\text{and}\quad \langle \tilde f, a\rangle + \langle \tilde g, b\rangle > \langle f, a\rangle + \langle g, b\rangle .

Milestones

Proposition 3.3 (p. 405). If $P \in U(a,b)$ and $(f,g) \in R(C)$ are complementary, then $P$ is primal optimal and $(f,g)$ is dual optimal.
Proposition 3.5 (p. 415). If every balanced pair $(i, j')$ with $i \in S$ has $j' \in S'$ , then $(f,g) + \varepsilon(\mathbb{1}_S, -\mathbb{1}_{S'}) \in R(C)$ for all sufficiently small $\varepsilon > 0$ .
Objective change (proof of Proposition 3.6, pp. 416–417). The step changes the dual objective by exactly $\varepsilon(\mathbb{1}_S^{\mathsf T}a - \mathbb{1}_{S'}^{\mathsf T}b)$ .
Labeled sets (proof of Proposition 3.6, pp. 416–417). If no coupling in $U(a,b)$ is complementary to $(f,g)$ , then there are $S, S'$ with every balanced pair leaving $S$ landing in $S'$ , and

\mathbb{1}_S^{\mathsf T}a - \mathbb{1}_{S'}^{\mathsf T}b > 0 .

Significance

The result. Proposition 3.6 says that non-optimality of a feasible dual pair is always witnessed by a direction with entries in $\{0, \pm 1\}$ , determined by two index sets, which keeps the pair feasible for a positive step and strictly improves the objective. This is what makes dual ascent a finite combinatorial method rather than a generic linear-programming iteration: the search for an ascent direction reduces to a maximum-flow computation on the bipartite graph of balanced pairs. Combined with the step length of Proposition 3.5, it is the primal-dual method, which reduces to the Hungarian algorithm on assignment problems. Milestone 1 is the optimality certificate of complementary slackness, used throughout the book's chapter 3.

Formalizing it. These results are classical and proved in the book and in Bertsimas and Tsitsiklis; no machine-checked proof of them is known to exist. The mission produces a formal statement and proof of the optimality-or-ascent alternative for the discrete Kantorovich dual, together with the complementary-slackness certificate in the transport setting. Milestone 4 is a Hall-type statement (a supply–demand theorem on a bipartite graph) whose formal proof is reusable for other matching and transportation results.

Difficulty

Milestones 1–3 are short computations. The content of the goal is in milestone 4. The obvious argument is linear-programming duality: if $(f,g)$ is not optimal, some feasible direction improves the objective. But LP duality only produces an arbitrary real direction; the claim that a direction of the form $(\mathbb{1}_S, -\mathbb{1}_{S'})$ suffices is a combinatorial statement. The book obtains $S, S'$ as the labeled nodes of a maximal flow (Ford–Fulkerson) and argues through max-flow/min-cut; the flow bookkeeping printed on p. 417 is garbled, so the step from "no complementary coupling exists" to " $\mathbb{1}_S^{\mathsf T}a > \mathbb{1}_{S'}^{\mathsf T}b$ for a set closed under balanced edges" has to be supplied carefully. Separately, connecting "not optimal" to "no complementary coupling exists" needs the converse direction of complementary slackness or strong duality for the transport problem.

Formalization scope

Row and column indices are Fin n and Fin m (0-based); the primed column set $[\![m]\!]'$ is just Fin m. Cost matrices and couplings are Matrix (Fin n) (Fin m) ℝ; histograms and potentials are real functions on Fin n, Fin m; $\Sigma_n$ is Mathlib's stdSimplex ℝ (Fin n). Index sets $S, S'$ are Finsets and $\mathbb{1}_S$ is indicatorVec S. "Optimal for Problem (3.4)" is the predicate IsDualOptimal: feasible, and no feasible pair has a larger objective (no real infimum or supremum is used, so no junk value can enter). The book's "for a small enough $\varepsilon > 0$ " is stated as "for every $\varepsilon \in (0, \varepsilon_0]$ ", which is equivalent because $R(C)$ is convex and the objective is linear.

Standing assumptions, all from the book: $(f, g)$ is dual feasible (p. 415, "In what follows, $(f,g)$ is a feasible dual pair in $R(C)$ "); $a, b$ are histograms in the simplex (used for the goal and milestone 4; without equal masses the dual is unbounded and optimality fails for every pair). Milestone 4 replaces the book's flow hypothesis "the throughput is strictly smaller than 1" by the equivalent flow-free statement "no coupling in $U(a,b)$ is complementary to $(f,g)$ "; flows, capacities and the labeling algorithm appear in no statement.

The goal admits a trivializing formalization: allowing an arbitrary direction $(u, v)$ instead of $(\mathbb{1}_S, -\mathbb{1}_{S'})$ turns Proposition 3.6 into plain non-optimality of a linear program. The statement here fixes the direction to $(\mathbb{1}_S, -\mathbb{1}_{S'})$ exactly as the book does.

A complete development needs finite LP duality or complementary slackness for the transportation problem, and a max-flow/min-cut or Hall-type theorem on bipartite graphs with vertex capacities. Both are reusable well beyond this mission. Contributions welcome: proofs of the milestones, a self-contained proof of milestone 4 by induction or by a max-flow argument, and alternative proofs of the goal through LP duality plus a vertex argument.

Selected references

G. Peyré, M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. https://doi.org/10.1561/2200000073 (§3.1–3.3, §3.6, pp. 400–417)
D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §7.7 (the primal-dual method) and pp. 305–308 (Ford–Fulkerson and the labeling algorithm).
H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2(1–2):83–97, 1955. https://doi.org/10.1002/nav.3800020109
L. R. Ford, D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5

9 thms4 active usersReviewed

Completed

Analysis Optimal Transport Optimization·Captain: mikedeng1

Computational Optimal Transport X: For the Cost c = d a Function Is a c-Transform if and only if It Is 1-Lipschitz, and Then f^c = −fTextbook

Motivation

Optimal transport compares two probability distributions by the least cost of moving one onto the other. When the ground cost is itself a distance, $c(x,y)=d(x,y)$ , the resulting quantity is the 1-Wasserstein distance $\mathcal W_1$ , also called the earth mover's distance. It is the transport distance most used in practice for comparing histograms, images and point clouds, and it is the setting of Chapter 6 of G. Peyré and M. Cuturi, Computational Optimal Transport (FnT ML 2019).

For general costs the dual problem has two potentials $(f,g)$ coupled by the constraint $f(x)+g(y)\le c(x,y)$ . For a metric cost the dual collapses to a single potential constrained to be 1-Lipschitz. This is the Kantorovich–Rubinstein formula (Kantorovich and Rubinstein, 1958, cited by the book on p. 473), the basis of dual computations of $\mathcal W_1$ : network-flow algorithms, the discrete linear programs of §6.1, and Wasserstein GANs, whose critics are 1-Lipschitz networks (Arjovsky, Chintala and Bottou, 2017). Proposition 6.1 of the book is the step that makes the collapse happen. It describes exactly which functions arise as $c$ -transforms when $c=d$ .

Setting

Let $(\mathcal X,d)$ be a metric space and take $\mathcal Y=\mathcal X$ with ground cost $c(x,y)=d(x,y)$ . For a real function $f$ on $\mathcal X$ its $c$ -transform (the book's (5.1)) is

f^c(y)=\inf_{x\in\mathcal X}\, d(x,y)-f(x),\qquad y\in\mathcal X .

The infimum can be $-\infty$ when the family is unbounded below. A function of the form $g^c$ is called $c$ -concave. The Lipschitz constant of $f$ is

\mathrm{Lip}(f)=\sup\left\{\frac{|f(x)-f(y)|}{d(x,y)} : (x,y)\in\mathcal X^2,\ x\ne y\right\},

and $f$ is 1-Lipschitz when $\mathrm{Lip}(f)\le 1$ , i.e. $|f(x)-f(y)|\le d(x,y)$ for all $x,y$ .

For the discrete companion, fix points $z_1,\dots,z_N\in\mathcal X$ and probability histograms $a,b\in\Sigma_N$ (nonnegative entries summing to one). Let $D_{k,\ell}=d(z_k,z_\ell)$ . The couplings $U(a,b)$ are the nonnegative $N\times N$ matrices with row sums $a$ and column sums $b$ . The optimal transport cost is $L_D(a,b)=\min_{P\in U(a,b)}\langle D,P\rangle$ with $\langle D,P\rangle=\sum_{k,\ell}D_{k,\ell}P_{k,\ell}$ .

Formalization targets

Goal: Proposition 6.1 (p. 472)

For every real function $f$ on $\mathcal X$ :

\bigl(\exists\, g\in\mathcal C(\mathcal X):\ f=g^c\bigr)\iff \mathrm{Lip}(f)\le 1, \qquad\text{and}\qquad \mathrm{Lip}(f)\le1\ \Longrightarrow\ f^c=-f .

Milestones (from the book's proof, pp. 472–473)

If $f=g^c$ is real valued, then $|f(x)-f(y)|\le d(x,y)$ for all $x,y$ .
If $\mathrm{Lip}(f)\le1$ and $g=-f$ , then $g^c(y)=\inf_x\,[d(x,y)+f(x)]=f(y)$ for every $y$ .
If $\mathrm{Lip}(f)\le1$ , then $f^c(y)=\inf_x\,[d(x,y)-f(x)]=-f(y)$ for every $y$ .

Companion: the discrete formula (6.2) (p. 473)

L_D(a,b)=\max_{\mathbf f\in\mathbb R^N}\Bigl\{\sum_k \mathbf f_k(a_k-b_k) : \forall (k,\ell),\ |\mathbf f_k-\mathbf f_\ell|\le d(z_k,z_\ell)\Bigr\},

with the minimum on the left and the maximum on the right both attained.

The mission also references the measure-theoretic Kantorovich–Rubinstein theorem already proved on the platform (WassersteinDRO.Duality.kantorovich_rubinstein). It is the book's (6.1) on a normed space.

Significance

The result. Proposition 6.1 identifies the $c$ -concave functions for a metric cost with the 1-Lipschitz functions, and shows that the $c$ -transform of such a function is $-f$ . Starting from the dual problem in a single potential, the book then replaces $(g,g^c)$ by $(g^c,-g^c)$ . This yields (6.1), $\mathcal W_1(\alpha,\beta)=\max_{\mathrm{Lip}(f)\le1}\int f\,\mathrm d(\alpha-\beta)$ . Consequently $\mathcal W_1$ is a norm on measures of zero total mass. In the discrete case the dual is the finite program (6.2), whose constraints only involve pairs of support points. The min-cost-flow formulations and the Lipschitz-critic methods built on $\mathcal W_1$ all start from this characterization.

Formalizing it. The proposition and (6.2) are classical, with complete proofs in the book. The mission produces machine-checked versions in a form that later chapters of this series can reuse. (6.2) is the discrete, linear-programming form of Kantorovich–Rubinstein duality, and the referenced platform theorem does not imply it without further work. To the best of this mission's search of the platform, neither Proposition 6.1 nor (6.2) has been formalized there. Villani's double-conjugate theorem $(\psi^c)^c=\psi$ for $c$ -concave $\psi$ is published, but it is a different statement.

Difficulty

Proposition 6.1 is short; its content is the characterization, not a long argument. One point needs care: an infimum over an arbitrary metric space can be $-\infty$ . The statement " $f=g^c$ " therefore carries the information that the infimum is finite at every point. An encoding in which the infimum of an unbounded family silently becomes $0$ would make the forward direction false, or decide it by a default value. The discrete companion (6.2) is a genuine duality theorem. It needs both the attainment of the transport minimum and a strong-duality argument specialised to a metric cost matrix. Ordinary LP duality yields two potentials, and the reduction to a single 1-Lipschitz potential is exactly Proposition 6.1 on the finite set $\{z_1,\dots,z_N\}$ .

Formalization scope

$\mathcal X$ is an arbitrary Lean MetricSpace; no compactness, completeness or separability is assumed, since the book's §6.1 assumes only that $d$ is a distance.
The $c$ -transform is the published MongeKantorovichYao.cConjugate, applied to the cost $(x,y)\mapsto d(x,y)$ . Its infimum is taken in EReal over all $x\in\mathcal X$ , so it never takes a default value. " $f=g^c$ " is an equality in EReal with $f$ real valued.
$\mathrm{Lip}(f)\le1$ is Mathlib's LipschitzWith 1 f, which is equivalent to the book's supremum formula.
In the goal, $g$ ranges over continuous real functions (the book's $\mathcal C(\mathcal X)$ ). The book's $f\in\mathcal C(\mathcal X)$ is not assumed: both sides of the equivalence force $f$ to be 1-Lipschitz, hence continuous. Milestone 1 allows any real $g$ , which is more general than the book's statement.
No Nonempty assumption: for empty $\mathcal X$ every claim holds trivially, and for nonempty $\mathcal X$ the infimum ranges over a nonempty family.
In (6.2), indices are Fin N. The two measures are written on common points $z_k$ , which need not be distinct, and $\mathcal W_1(\alpha,\beta)$ is the discrete cost $L_D(a,b)$ of (2.11).
The statement is not trivialised by its encoding: a sorry-free check shows that $f^c$ equals $-\infty$ , not a junk value, on an unbounded-below example. The hypotheses of (6.2) are satisfiable, with $ab^\top\in U(a,b)$ .

Contributions welcome: proofs of the milestones and goal, and a proof of (6.2), via finite LP duality and the milestones or via the referenced measure-theoretic theorem.

Selected references

G. Peyré and M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. https://doi.org/10.1561/2200000073 (arXiv: https://arxiv.org/abs/1803.00567)
L. V. Kantorovich and G. S. Rubinstein, On a space of totally additive functions, Vestn. Leningrad Universitet 13:52–59, 1958 (Russian; no stable online link located, cited after the book's bibliography).
C. Villani, Optimal Transport: Old and New, Grundlehren der mathematischen Wissenschaften 338, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9
M. Arjovsky, S. Chintala and L. Bottou, Wasserstein Generative Adversarial Networks, ICML 2017. https://arxiv.org/abs/1701.07875

7 thms4 active usersReviewed

Completed

Convex Optimization Functional Analysis Machine Learning+2·Captain: mikedeng1

Kernel Distributionally Robust Optimization: Generalized Duality Theorem and Stochastic Approximation: The Worst-Case Risk over an RKHS Ambiguity Set Equals Its Support-Function DualResearch Paper

Motivation

Distributionally robust optimization (DRO) chooses a decision $\theta$ that minimizes the expected loss under the worst distribution in an ambiguity set $\mathcal K$ of plausible distributions, $\min_\theta\sup_{P\in\mathcal K}\int l(\theta,\xi)\,dP(\xi)$ . It sits between stochastic optimization, which trusts a single distribution, and worst-case robust optimization, which trusts none. The inner supremum is a problem of moments, studied since Stieltjes and made computable by duality (Isii 1962; Shapiro 2001; Bertsimas and Popescu 2005). Existing tractable reformulations require the ambiguity set to be described by finitely many moments, a $\phi$ -divergence or a Wasserstein ball, and they usually require a structural property of the loss: affine or quadratic form, or a known Lipschitz constant.

Zhu, Jitkrittum, Diehl and Schölkopf (AISTATS 2021; arXiv:2006.06981) describe the ambiguity set through kernel mean embeddings: a distribution is represented by its mean in a reproducing kernel Hilbert space, and the ambiguity set is the set of distributions whose embedding lies in a convex set $\mathcal C$ of that space. Moment sets, MMD balls, scenario polytopes and the whole space (worst-case RO) all arise for suitable kernels and sets $\mathcal C$ . Their Generalized Duality Theorem (Theorem 3.1) turns the inner worst-case problem into a minimization over a function of the RKHS that majorizes the loss, with no assumption on the loss beyond upper semicontinuity.

Setting

Let $\mathcal X$ be a compact metric space (in the paper, a compact $\mathcal X\subset\mathbb R^d$ ) with its Borel $\sigma$ -algebra, and $\mathcal P$ the set of Borel probability measures on $\mathcal X$ . Let $\mathcal H$ be a real Hilbert space and $\varphi:\mathcal X\to\mathcal H$ a continuous feature map; $k(x,y)=\langle\varphi(x),\varphi(y)\rangle_{\mathcal H}$ is then a continuous positive definite kernel, and an element $f\in\mathcal H$ acts on $\mathcal X$ by the reproducing property $f(\xi)=\langle f,\varphi(\xi)\rangle_{\mathcal H}$ (rkhsEval).

The mean embedding of $P\in\mathcal P$ is $\mu_P=\int\varphi\,dP\in\mathcal H$ (meanEmbedding).
For $\mathcal C\subseteq\mathcal H$ , the ambiguity set is $\mathcal K_{\mathcal C}=\{P\in\mathcal P:\mu_P\in\mathcal C\}$ (ambiguitySet).
The support function of $\mathcal C$ is $\delta^*_{\mathcal C}(f)=\sup_{\mu\in\mathcal C}\langle f,\mu\rangle_{\mathcal H}\in[-\infty,\infty]$ (supportFun).
A loss is a function $l:\Theta\times\mathcal X\to[-\infty,\infty)$ , where $\Theta$ is an arbitrary set of decisions; $\int l\,dP$ is the extended-real expectation.

For fixed $\theta$ (written $l=l(\theta,\cdot)$ ), the primal inner problem (11) and the dual inner problem (12) are

\mathrm{(P)}_\theta=\sup_{P\in\mathcal K_{\mathcal C}}\int l\,dP,\qquad \mathrm{(D)}_\theta=\inf\Big\{f_0+\delta^*_{\mathcal C}(f):\ f_0\in\mathbb R,\ f\in\mathcal H,\ l(\xi)\le f_0+f(\xi)\ \forall\xi\in\mathcal X\Big\}

(primalValue, dualValue, with the constraint IsDualFeasible). Assumption 3.1 of the paper asks that each $l(\theta,\cdot)$ be proper (not identically $-\infty$ ) and upper semicontinuous, that $\mathcal C$ be closed and convex, and that $\mathrm{ri}(\mathcal K_{\mathcal C})\neq\emptyset$ .

The PDF prints no page numbers; every page cited in this mission is the PDF page of arXiv:2006.06981v3.

Formalization targets

Goal: Theorem 3.1 (Generalized Duality), p. 5

Under the hypotheses above, with $\mathcal K_{\mathcal C}\ne\emptyset$ ,

\forall\theta\in\Theta:\quad \sup_{P\in\mathcal K_{\mathcal C}}\int l(\theta,\xi)\,dP(\xi)=\inf_{\substack{f_0\in\mathbb R,\,f\in\mathcal H\\ l(\theta,\cdot)\le f_0+f}}f_0+\delta^*_{\mathcal C}(f),

and consequently $\mathrm{(P)}=\inf_\theta\mathrm{(P)}_\theta=\inf_\theta\mathrm{(D)}_\theta=\mathrm{(D)}$ , the equality of the Kernel DRO problem (2) and its dual (4).

Milestones (the proof of Proposition A.1, pp. 13–15, and Appendix D, pp. 22–23)

The reproducing identity $\int f\,dP=\langle f,\mu_P\rangle_{\mathcal H}$ (p. 13).
Lemma D.1: $\int(l-f_0-f)\,dP\le0$ for all $P$ iff $l\le f_0+f$ on $\mathcal X$ .
Weak duality: $\int l\,dP\le f_0+\delta^*_{\mathcal C}(f)$ for $P\in\mathcal K_{\mathcal C}$ and feasible $(f_0,f)$ (p. 6).
Lemmas D.2–D.4: $\mathcal T(\mathcal P)=\{\mu_P\}$ , $\mathcal C\cap\mathcal T(\mathcal P)$ and $\mathcal K_{\mathcal C}$ are compact.
Primal attainment (p. 15), via the upper semicontinuity of $P\mapsto\int l\,dP$ (a supporting lemma the paper uses without stating).
The separation (14), the sign $\tau<0$ with the rescaled dual feasible point, and $\mathrm{(D)}\le\mathrm{(P)}+\epsilon$ (p. 15).
Proposition A.1: $\mathrm{(P)}_\theta=\mathrm{(D)}_\theta$ (p. 13).

Companions

Lemma A.2 (complementarity (19)), Corollary 3.1.3 (the optimal majorant interpolates $l$ $P^*$ -a.e.), the support function $\frac1N\sum_i f(\xi_i)+\epsilon\|f\|_{\mathcal H}$ of the RKHS norm ball (Table 1), and the weak-duality content of Corollary 3.1.1 for integral probability metrics.

Significance

The theorem replaces an optimization over probability measures by a semi-infinite program over $(f_0,f)\in\mathbb R\times\mathcal H$ , whose objective is explicit for the common choices of $\mathcal C$ (Table 1). The majorant $f_0+f$ needs no Lipschitz constant and no parametric form of the loss, and the dual variable $f^*$ doubles as a witness function for the MMD. This is the basis of the paper's batch and stochastic functional gradient algorithms, and it places moment-based DRO, scenario optimization, MMD-ball DRO and worst-case RO in one framework.

The result is proved on paper; it has no machine-checked proof that we know of. Formalizing it builds the duality theory of moment problems with infinitely many moment constraints, on top of Mathlib's Hilbert spaces, Bochner integrals and the weak topology on probability measures. The formal statements also fix points the paper leaves loose: the infimum in place of the printed "min", the reading of the Slater condition, and the role of the continuity of the kernel.

Difficulty

Weak duality is a two-line computation. The work is strong duality. The paper's route separates the cone $A=\{(\int1\,dP,\int\varphi\,dP,\int l\,dP):P\in\mathrm{co}(\mathcal P)\}$ from $B_\epsilon=\{(1,\mu,t+\epsilon):\mu\in\mathcal C\}$ in $\mathbb R\times\mathcal H\times\mathbb R$ . A Hahn–Banach strict separation needs one set compact or the two at positive distance, and $A$ is neither obviously closed nor bounded. The step goes through only because $\mathcal K_{\mathcal C}$ is compact in the weak topology and $P\mapsto\int l\,dP$ is upper semicontinuous, which also gives primal attainment and the sign $\tau<0$ . The loss may take the value $-\infty$ , so every expectation lives in $[-\infty,\infty)$ . The infinite primal case also needs an argument of its own.

Formalization scope

$\mathcal X$ is a compact metric space with a Borel $\sigma$ -algebra; a compact subset of $\mathbb R^d$ is an instance. $\mathcal P$ is ProbabilityMeasure X with its topology of weak convergence; the paper's MMD topology agrees with it for a universal continuous kernel.
The RKHS is in feature-map form: a real Hilbert space $\mathcal H$ and a continuous $\varphi$ . Continuity of the kernel is not written in Assumption 3.1 but is used by Appendix D.
Losses are X → EReal, upper semicontinuous, never $+\infty$ , and not identically $-\infty$ . Expectations use the published definition WassersteinDRO.Duality.erealExpectation, which for such losses is the usual $\int l\,dP\in[-\infty,\infty)$ .
Support function, primal and dual values are extended reals. $\delta^*_\emptyset=-\infty$ ; $\delta^*_{\mathcal H}(f)=+\infty$ for $f\ne0$ ; an empty ambiguity set gives primal value $-\infty$ ; an infeasible dual gives $+\infty$ . The sum $f_0+\delta^*_{\mathcal C}(f)$ adds a real to an extended real, so $+\infty+(-\infty)$ never occurs.
The Slater clause $\mathrm{ri}(\mathcal K_{\mathcal C})\ne\emptyset$ names no topology on measures and is used only to obtain a primal solution (p. 15). It is read as $\mathcal K_{\mathcal C}\ne\emptyset$ , which it implies under any reading, so the formal goal is at least as strong as the paper's.
Every printed "min" is read as an infimum. Dual attainment is not proved and can fail: for $\mathcal X=[0,1]$ , $\varphi(x)=x$ , $\mathcal C=(-\infty,0]$ and $l(x)=\sqrt x$ , the dual infimum $0$ is not attained.
The dual variable ranges over $\mathcal H$ , never over arbitrary functions on $\mathcal X$ . Over all bounded functions, the choice $f=l$ would make the duality trivial (Example 3.3). The goal is also not closed by unfolding: for $\mathcal C=\mathcal H$ it says $\sup_P\int l\,dP=\sup_\xi l(\xi)$ , worst-case RO.
Corollary 3.1.2 (p. 6) is not stated: it is false under Assumption 3.1 alone (for $\mathcal C=\mathcal H$ and $l=\mathbf 1_{\{0\}}$ , (2) equals $1$ while (6) equals $0$ ).

Reusable pieces: the kernel mean embedding and its continuity on ProbabilityMeasure X, compactness of RKHS ambiguity sets, and the upper semicontinuity of $P\mapsto\int l\,dP$ for upper semicontinuous $l$ (a portmanteau-type fact not yet in Mathlib). Proofs of any milestone are welcome. So are support-function computations for the other rows of Tables 1 and 3.

Selected references

J.-J. Zhu, W. Jitkrittum, M. Diehl, B. Schölkopf, Kernel Distributionally Robust Optimization: Generalized Duality Theorem and Stochastic Approximation, AISTATS 2021 (PMLR 130); cited here as arXiv:2006.06981v3, 2021. https://arxiv.org/abs/2006.06981
A. Shapiro, On duality theory of conic linear problems, in Semi-Infinite Programming, Kluwer, 2001. https://doi.org/10.1007/978-1-4757-3403-4_7
K. Isii, On sharpness of Tchebycheff-type inequalities, Annals of the Institute of Statistical Mathematics 14, 1962. https://doi.org/10.1007/BF02868641
D. Bertsimas, I. Popescu, Optimal inequalities in probability theory: a convex optimization approach, SIAM Journal on Optimization 15(3), 2005. https://doi.org/10.1137/S1052623401399903
A. Gretton, K. Borgwardt, M. Rasch, B. Schölkopf, A. Smola, A kernel two-sample test, Journal of Machine Learning Research 13, 2012. https://jmlr.org/papers/v13/gretton12a.html
A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050

15 thms4 active usersReviewed

Completed

Information Theory Machine Learning Probability+1·Captain: mikedeng1

Information-Theoretic Analysis of Generalization Capability of Learning Algorithms I: The Expected Generalization Error Is at Most √(2σ²I(S;W)/n) (Theorem 1)Research Paper

Motivation

A learning algorithm trained on a finite sample generalizes when its empirical risk on that sample is close to its risk on fresh data. Classical guarantees come from uniform convergence over the hypothesis class (VC dimension, Rademacher complexity) or from algorithmic stability, such as uniform stability (Bousquet and Elisseeff, 2002) and on-average stability (Shalev-Shwartz et al., 2010). Both families look at the class or at the algorithm's worst-case sensitivity, not at how much the trained hypothesis actually depends on the data it was trained on.

Russo and Zou (arXiv:1511.05219, 2016) bounded the bias of adaptive data analysis by mutual information, and Xu and Raginsky (arXiv:1705.07809, NIPS 2017) turned this into a generalization bound for learning algorithms: the expected generalization error is at most $\sqrt{2\sigma^2 I(S;W)/n}$ , where $I(S;W)$ is the mutual information between the training sample and the output hypothesis. This bound started the line of information-theoretic generalization bounds, later refined to individual-sample mutual information (Bu, Zou and Veeravalli, 2020), conditional mutual information (Steinke and Zakynthinou, 2020) and chaining variants (Asadi, Abbe and Verdú, 2018).

Timeline:

2016, Russo and Zou: bias of adaptive analysis bounded by $I(\Lambda_{\mathsf W}(S);W)$ , the information carried by the vector of empirical risks, for a finite hypothesis space.
2017, Xu and Raginsky: the bound with the input–output mutual information $I(S;W)$ , for arbitrary hypothesis spaces (Theorem 1); high-probability versions and an analysis of the Gibbs algorithm.
2018–2020: chaining, individual-sample and conditional mutual information refinements.

Setting

There is an instance space $\mathsf Z$ , a hypothesis space $\mathsf W$ and a nonnegative loss $\ell:\mathsf W\times\mathsf Z\to\mathbb R_+$ , written ℓ : W → Z → ℝ in Lean. Data are drawn from an unknown probability measure $\mu$ on $\mathsf Z$ ; a dataset of size $n$ is an i.i.d. sample $S=(Z_1,\dots,Z_n)\sim\mu^{\otimes n}$ (sampleLaw μ n).

A learning algorithm is a Markov kernel $P_{W|S}$ (κ : Kernel (Fin n → Z) W): given the dataset, it outputs a random hypothesis $W$ . The pair $(S,W)$ has joint law $P_{S,W}=\mu^{\otimes n}\otimes P_{W|S}$ (sampleLaw μ n ⊗ₘ κ), with marginals $P_S=\mu^{\otimes n}$ and $P_W$ .

The population risk and the empirical risk of a hypothesis $w$ are

L_\mu(w)=\int_{\mathsf Z}\ell(w,z)\,\mu(dz),\qquad L_S(w)=\frac1n\sum_{i=1}^n \ell(w,Z_i)

(risk ℓ μ w, empRisk ℓ s w). The expected generalization error is

\mathrm{gen}(\mu,P_{W|S})=\mathbb E\big[L_\mu(W)-L_S(W)\big],

the expectation taken under $P_{S,W}$ (genError ℓ μ κ).

The mutual information of a pair $(X,Y)$ with joint law $P_{X,Y}$ is the relative entropy $I(X;Y)=D(P_{X,Y}\,\|\,P_X\otimes P_Y)\in[0,\infty]$ (mutualInfo). A real random variable $U$ is $\sigma$ -subgaussian if $\log\mathbb E[e^{\lambda(U-\mathbb EU)}]\le\lambda^2\sigma^2/2$ for all $\lambda\in\mathbb R$ .

Formalization targets

Goal: Theorem 1 (p. 4)

If $\ell(w,Z)$ is $\sigma$ -subgaussian under $\mu$ for every $w\in\mathsf W$ , then

\big|\mathrm{gen}(\mu,P_{W|S})\big|\le\sqrt{\frac{2\sigma^2}{n}\,I(S;W)} .

The statement fixes no structure on $\mathsf W$ (it may be uncountable) and no bound on the loss beyond subgaussianity.

Milestones

(A.1), Donsker–Varadhan (p. 11), the inequality $\int F\,d\pi-D(\pi\|\rho)\le\log\int e^F\,d\rho$ . Already proved on the platform and referenced.
Lemma 1 (p. 3), the decoupling estimate: if $f(\bar X,\bar Y)$ is $\sigma$ -subgaussian under $P_X\otimes P_Y$ , then

\big|\mathbb E f(X,Y)-\mathbb E f(\bar X,\bar Y)\big|\le\sqrt{2\sigma^2 I(X;Y)} .

Subgaussianity of the empirical risk (§3.2, p. 4): for every $w$ , $L_S(w)-L_\mu(w)$ is $\sigma/\sqrt n$ -subgaussian under $\mu^{\otimes n}$ .
The mixture step (§3.2, p. 4, corrected): under $P_S\otimes P_W$ , $f(\bar S,\bar W)=L_{\bar S}(\bar W)-L_\mu(\bar W)$ is $\sigma/\sqrt n$ -subgaussian with mean $0$ .

Significance

The result. Theorem 1 makes generalization a property of the dependence between data and output rather than of the size of the hypothesis class. It applies to randomized algorithms on uncountable or infinite-dimensional hypothesis spaces, where uniform convergence gives nothing, and to unbounded subgaussian losses. Any mechanism that limits $I(S;W)$ , such as noise injection, differential privacy, compression or relative-entropy regularization, inherits a generalization guarantee. A loss with values in $[a,b]$ is $(b-a)/2$ -subgaussian for every $\mu$ , so the theorem covers all bounded losses. The bound is also the template for the later refinements listed above, which share Lemma 1's decoupling argument.

Formalizing it. The result is proved on paper; no machine-checked proof is known. A formalization supplies a reusable statement of mutual information as a relative entropy of a joint law on general measurable spaces, a decoupling lemma for subgaussian functions, and the mixture argument for subgaussian families, all of which recur in the later literature. It also settles a point the paper leaves loose: the printed proof applies Lemma 1 to the uncentred empirical risk, which is not subgaussian in general; the milestones state the corrected step.

Difficulty

The two halves of the proof are short on paper, but each step that "follows" uses a fact the page does not state. The decoupling estimate needs $\mathbb E f(X,Y)$ to be finite, which holds only because finite relative entropy and exponential integrability under the product together force integrability under the joint law. The mixture step needs the moment-generating-function bound of each section $w\mapsto f(\cdot,w)$ to integrate over $P_W$ , which requires joint measurability and the centring of every section at its own mean: the uncentred empirical risk $L_{\bar S}(\bar W)$ mixes laws with different means and is not subgaussian.

A natural first attempt applies Lemma 1 directly to $f(s,w)=L_s(w)$ as printed; it fails on the example $\ell(w,z)=w$ with $W$ uniform on $\{0,1\}$ and independent of $S$ .

Formalization scope

Objects. The sample law, $L_\mu$ and $L_S$ are reused from the published LearnStability.Characterization.Setting. This mission defines mutualInfo P := klDiv P (P.fst.prod P.snd) (values in $[0,\infty]$ ) and genError, the integral of the pointwise difference $L_\mu(w)-L_s(w)$ under sampleLaw μ n ⊗ₘ κ. Samples are Fin n → Z; the algorithm is a Markov kernel.
Subgaussianity is Mathlib's HasSubgaussianMGF of the centred variable, whose parameter is the variance proxy: $\sigma^2$ for the loss, $\sigma^2/n$ for the empirical risk.
Added hypotheses, all implicit on the page: $n\ge1$ (the bound divides by $n$ ); joint measurability of $\ell$ (so that $L_\mu(W)$ and $L_S(W)$ are random variables); and $I\ne\infty$ in Lemma 1 and Theorem 1, because Lean's conversion of $\infty$ to a real number gives $0$ , which would turn the page's vacuous bound into a false claim. The page's nonnegativity of $\ell$ is kept. No integrability hypothesis on $f$ or on the losses is assumed beyond subgaussianity.
Correction of the print. The page says that $f(\bar S,\bar W)=L_{\bar S}(\bar W)$ is $\sigma/\sqrt n$ -subgaussian; milestone 4 states it for the centred $L_{\bar S}(\bar W)-L_\mu(\bar W)$ , together with its mean being $0$ . Equation (9) is not posed separately.
Ruled out. The goal is stated for genError and the mutual information of the algorithm's own joint law; a version through Lemma 1's abstract pair $(\bar X,\bar Y)$ , through $I(\Lambda_{\mathsf W}(S);W)$ (Theorem 2, out of scope), or with $I$ truncated to a real number would not be this theorem.
Infrastructure. Integrability transfer from $P_X\otimes P_Y$ to $P_{X,Y}$ under finite relative entropy; sums of independent subgaussian variables on Measure.pi (Mathlib has HasSubgaussianMGF.sum_of_iIndepFun); mixtures of mean-zero subgaussian families under a product measure. These are reusable beyond this mission, and contributions of each are welcome.

Selected references

A. Xu, M. Raginsky, Information-theoretic analysis of generalization capability of learning algorithms, NIPS 2017; arXiv:1705.07809v2. https://arxiv.org/abs/1705.07809
D. Russo, J. Zou, Controlling bias in adaptive data analysis using information theory, AISTATS 2016. https://arxiv.org/abs/1511.05219
S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, stability and uniform convergence, JMLR 11, 2010. https://jmlr.org/papers/v11/shalev-shwartz10a.html
O. Bousquet, A. Elisseeff, Stability and generalization, JMLR 2, 2002. https://www.jmlr.org/papers/v2/bousquet02a.html
S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities, Oxford University Press, 2013 (Donsker–Varadhan, Cor. 4.15). https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
A. Asadi, E. Abbe, S. Verdú, Chaining mutual information and tightening generalization bounds, NeurIPS 2018. https://arxiv.org/abs/1806.03803
Y. Bu, S. Zou, V. Veeravalli, Tightening mutual information based bounds on generalization error, IEEE JSAIT 2020. https://arxiv.org/abs/1901.04609
T. Steinke, L. Zakynthinou, Reasoning about generalization via conditional mutual information, COLT 2020. https://arxiv.org/abs/2001.09122

7 thms4 active usersReviewed

Completed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Bootstrap Robust Prescriptive Analytics 2: The Entropic Robust Nadaraya-Watson Budget Equals inf{α : ν log Σ D·exp((L−α)w/ν) + rν ≤ 0}Research Paper

Motivation

Data-driven decision making with side information ("prescriptive analytics") chooses a decision $z$ after observing a context $x = x_0$ , using a training set of past pairs $(x, y)$ . A common recipe estimates the conditional expected cost $\mathbb E[L(z, y) \mid x = x_0]$ with a local learning method, such as Nadaraya–Watson kernel regression or nearest neighbours, and then minimizes the estimate over $z$ (Ban and Rudin 2019; Bertsimas and Kallus 2020). Such estimate-then-optimize decisions are known to be optimistically biased: the minimized estimate tends to understate the cost that the decision incurs on new data.

Bertsimas and Van Parys (arXiv:1711.09974v2) robustify these formulations against distributions near the empirical one, measured by a relative-entropy bootstrap distance. They show that this choice protects the decision against disappointment on resampled (bootstrap) data at an exponential rate. A robust formulation is only usable if it can be computed. This mission concerns the paper's computational result for the Nadaraya–Watson case: the robust budget, a supremum over a set of distributions, equals a two-variable convex dual program.

Setting

The training data have finitely many distinct points, the support $\Omega_n$ . A distribution on $\Omega_n$ is a vector $D = (D_i)_{i \in \Omega_n}$ with $D_i \ge 0$ and $\sum_i D_i = 1$ ; their set is $\mathcal D_n$ . Fix a context $x_0$ and a decision $\bar z$ . Each support point $i = (\bar x_i, \bar y_i)$ carries a weight $w_i = w_n(\bar x_i, x_0) > 0$ and a loss $\ell_i = L(\bar z, \bar y_i)$ .

The Nadaraya–Watson estimate at $D$ (equation (19)) is the weighted average

E^n_D[\ell] = \frac{\sum_i w_i\,\ell_i\,D_i}{\sum_i w_i\,D_i}.

The bootstrap distance (Definition 6, equation (27)) is the relative entropy

B(D', D) = \sum_i D'_i \log\frac{D'_i}{D_i},

with $0\log 0 = 0$ and $B(D', D) = +\infty$ when $D'$ puts mass on a point where $D$ vanishes. For a reference distribution $D$ and a radius $r$ , the bootstrap robust Nadaraya–Watson budget (equation (24) with $R = B$ and $k(n) = n$ ) is

c_n(\bar z, D, x_0) = \sup\big\{ E^n_{D'}[\ell] : D' \in \mathcal D_n,\ B(D', D) \le r \big\}.

For the nearest-neighbours variant, nested neighbourhoods $N^0 \subseteq N^1 \subseteq \dots \subseteq N^n = \Omega_n$ define a partial robust budget $c^j_n$ (equation (25)), with two extra linear constraints tying the mass of $N^j$ and $N^{j-1}$ to $k/n$ and $(k-1)/n$ .

Formalization targets

Goal: Lemma 2

For every $D \in \mathcal D_n$ and every radius $r \in \mathbb R$ ,

c_n(\bar z, D, x_0) = \inf\Big\{\alpha \in \mathbb R :\ \exists\,\nu > 0,\ \ \nu\log\Big(\sum_i \exp\Big(\frac{(\ell_i - \alpha)\,w_i}{\nu}\Big) D_i\Big) + r\,\nu \le 0\Big\}.

No hypothesis on $r$ is imposed. For $r < 0$ both sides are $-\infty$ , and for $r = 0$ both equal $E^n_D[\ell]$ .

Milestones

The milestones follow the proof in Appendices B.3 and B.8:

The estimate $E^n_D[\ell]$ is the maximum of a linear program in $(s, P)$ with the single feasible point $P = sD$ (B.3).
Corollary 1: for any distance $R$ , $c_n$ equals the perspective program $\sup_{s > 0, P} \sum_i w_i \ell_i P_i$ subject to $s\,R(P/s, D) \le s\,r$ , $\sum_i P_i = s$ and $\sum_i w_i P_i = 1$ .
The Fenchel step: $\sup_{\lambda \ge 0}(\lambda b - \nu\lambda\log\lambda) = \nu e^{b/\nu - 1}$ .
Strong duality for $r > 0$ : the program of Corollary 1 with $R = B$ equals $\inf\{\alpha : \exists \beta, \nu > 0,\ r\nu + \nu\sum_i D_i e^{((\ell_i - \alpha)w_i + \beta)/\nu - 1} \le \beta\}$ .
Elimination of $\beta$ : such a $\beta$ exists if and only if $\nu \log \sum_i e^{(\ell_i-\alpha)w_i/\nu} D_i + r\nu \le 0$ .
Lemma 1 (companion): the analogous dual (32) of the partial nearest-neighbours budget, assuming Slater's condition $\inf\{B(D', D) : D' \in \mathcal D^j_n\} < r$ .

Significance

The robust budget is a supremum over a $|\Omega_n|$ -dimensional set of distributions, and the decision minimizes it over $\bar z$ , which is a min–max problem. Lemma 2 replaces the inner supremum by an infimum over two scalars $(\alpha, \nu)$ , so the robust prescription becomes a single minimization over $(\bar z, \alpha, \nu)$ . When $L$ is convex in $\bar z$ , that minimization is an exponential-cone program. The paper's numerical section (§5) solves its robust formulations in exactly this form. Lemma 1 plays the same role for the nearest-neighbours formulation, with one dual program per neighbourhood.

The results are proved in the paper (Appendices B.3, B.7, B.8) by a Lagrangian computation. As far as we know, none of them has been machine-checked. A formalization adds three things. It handles reference distributions $D$ with zeros, which the page's computation divides by. It covers the full range of radii, including $r \le 0$ , where Slater's condition fails. And it records the corrected sign of the minimizing multiplier $\beta^\star$ . The linear-objective special case without the ratio and with a strictly positive reference, $\max\{v^\top p : D(p\|q) \le \beta\} = \inf_{\lambda > 0} \lambda \log \sum_j q_j e^{v_j/\lambda} + \beta\lambda$ , is already proved on the platform (Nilim–El Ghaoui, RobustMDP.EntropyInner.kl_ball_inner_problem_dual, with its multiplier elimination RobustMDP.EntropyInner.mu_elimination). Both are included as supporting references.

Difficulty

The obvious route is to apply the known entropic duality formula to the robust budget directly. That route fails because the objective $E^n_{D'}[\ell]$ is a ratio of two linear functions of $D'$ , not a linear function. The ratio is quasi-linear, and Lagrangian duality does not apply to it as it stands. The paper first lifts it to a linear objective over the cone $(s, P) = (s, sD')$ (Corollary 1). The entropy constraint then becomes the perspective $s\,B(P/s, D) \le s\,r$ , and duality is applied to this lifted program. A second difficulty is that the reference $D$ may vanish on part of the support. The ball then lives on a face of the simplex, and every step must respect the convention $B = +\infty$ off the support of $D$ . Finally, strong duality needs a Slater point, which exists only for $r > 0$ . The cases $r \le 0$ of the goal have to be handled separately.

Formalization scope

The support $\Omega_n$ is a finite type ι, and $\mathcal D_n$ is stdSimplex ℝ ι. Covariates, responses and the distance of Definition 2 do not appear: only the weights w : ι → ℝ (positive) and the losses L z : ι → ℝ of a fixed decision enter. Losses are real-valued, a restriction of the paper's $\mathbb R_+ \cup \{+\infty\}$ , while nonnegativity is not required. The conventions are the following.

$B$ is EReal-valued: it is $+\infty$ when the first argument charges a zero of the second, and $0 \log 0 = 0$ .
All suprema and infima are in EReal: the supremum of the empty set is $-\infty$ and the infimum of the empty set is $+\infty$ .
Dual variables satisfy $\nu > 0$ . The page's $\nu \in \mathbb R_+$ admits $\nu = 0$ only as the perspective limit, and the infimum over $\alpha$ is unchanged.
In the perspective programs, $P/s \in \mathcal D_n$ is stated explicitly.
The neighbourhood chain is a monotone family of finite sets with $N^0 = \emptyset$ and $N^n = \Omega_n$ .

Several formalizations would make the statements trivial, and each is ruled out:

a real-valued $B$ , whose finite junk values enlarge the ball when $D$ has zeros;
real sSup/sInf, which return $0$ on empty or unbounded sets;
$\nu \ge 0$ with Lean's $x/0 = 0$ , which makes every $\alpha$ feasible;
a positivity hypothesis on $D$ , which the lemma does not have.

A complete development needs the following:

Gibbs' inequality and continuity of $B$ on the simplex;
Lagrangian (or Fenchel) duality for a convex program with one entropic constraint and linear constraints;
the perspective of relative entropy;
the one-dimensional conjugate of $\lambda \log \lambda$ .

The duality and conjugate lemmas are reusable for any KL-ball robust program. Contributions are welcome on each milestone, on bridges from the published RobustMDP.EntropyInner theorems to the setting here (they agree with $B$ when the reference is positive), and on the $r \le 0$ cases of the goal.

Selected references

D. Bertsimas and B. Van Parys, Bootstrap robust prescriptive analytics, arXiv:1711.09974v2, 2021 (Math. Program., 2021). https://arxiv.org/abs/1711.09974v2
G.-Y. Ban and C. Rudin, The big data newsvendor: practical insights from machine learning, Operations Research 67(1), 2019. https://doi.org/10.1287/opre.2018.1757
D. Bertsimas and N. Kallus, From predictive to prescriptive analytics, Management Science 66(3), 2020. https://doi.org/10.1287/mnsc.2018.3253
A. Nilim and L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. https://doi.org/10.1287/opre.1050.0216
A. Ben-Tal, D. den Hertog, A. De Waegenaere, B. Melenberg and G. Rennen, Robust solutions of optimization problems affected by uncertain probabilities, Management Science 59(2), 2013. https://doi.org/10.1287/mnsc.1120.1641

11 thms4 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

Proximal Algorithms I: A Point Minimizes f + g Exactly When It Is a Fixed Point of the Forward-Backward Operator x ↦ prox_λg(x − λ∇f(x))Research Paper

Motivation

Many convex optimization problems combine a smooth loss with a term that is easy to handle through minimization but awkward to differentiate. A constraint can be represented by an indicator function that is zero on the feasible set and $+\infty$ outside it. A norm penalty can be finite yet nonsmooth. The proximal gradient method handles such objectives by applying a gradient step to the smooth term and a proximal step to the other term. Parikh and Boyd present this method in §4.2 of Proximal Algorithms, after developing the proximal operator, its fixed points, and its connection to the subdifferential.

The mission concerns the method's optimality interpretation. A fixed point of the forward-backward update is a minimizer of the composite objective, for every positive step size. That is a statement about which points solve the problem. The separate claim that repeated updates converge requires further control of the gradient and the step size; the paper discusses that condition after the fixed-point identity on p. 151. This mission captures the fixed-point identity itself and the paper's stated convex-analytic results that support it.

Setting

Work in $\mathbb R^n$ with the Euclidean inner product $x^{\mathsf T}y$ and norm $\|x\|_2$ . Let $f:\mathbb R^n\to\mathbb R$ be convex and differentiable everywhere. Let $g:\mathbb R^n\to\mathbb R\cup\{+\infty\}$ be closed, proper and convex: its epigraph is nonempty, closed and convex. The effective domain $\operatorname{dom}g$ consists of the points where $g$ is finite. The composite problem, equation (4.5), is to minimize $f(x)+g(x)$ over all $x\in\mathbb R^n$ . An indicator $g=I_C$ expresses the constraint $x\in C$ within the same notation. These conventions are those of §1.1 and §4.2 of the monograph.

For a closed proper convex function $h$ , the proximal operator sends $v$ to the unique minimizer of $h(u)+\tfrac12\|u-v\|_2^2$ . For $\lambda>0$ , the operator $\operatorname{prox}_{\lambda h}$ equivalently minimizes $h(u)+\tfrac1{2\lambda}\|u-v\|_2^2$ . The paper assumes closed proper convexity whenever it uses a proximal operator, including one applied to $g$ . This assumption gives a unique proximal point at every input, even when $g$ is infinite outside a strict subset of the space.

The subdifferential $\partial g(x)$ is the set of vectors $y$ such that $g(z)\ge g(x)+y^{\mathsf T}(z-x)$ for every $z\in\operatorname{dom}g$ , as in (2.3). Unlike the gradient of $f$ , it can be empty or contain several vectors. The resolvent of the subdifferential with parameter $\lambda$ is the inverse relation $(I+\lambda\partial g)^{-1}$ . Equation (3.4) says that this relation is the everywhere-defined, single-valued map $\operatorname{prox}_{\lambda g}$ . Both descriptions of the proximal point appear in the milestone list.

Formalization targets

Goal: fixed points of the forward-backward operator

For any $\lambda>0$ and $x^\star\in\mathbb R^n$ , the target from §4.2.1, pp. 150–151, is

x^\star\text{ minimizes }f+g \quad\Longleftrightarrow\quad x^\star=\operatorname{prox}_{\lambda g}\bigl(x^\star-\lambda\nabla f(x^\star)\bigr).

The quantifier covers every positive $\lambda$ ; it is independent of any Lipschitz bound. The equation describes a fixed point of the forward-backward operator, which first evaluates $\nabla f$ and then applies the proximal operator of $g$ .

Supporting statements

The milestones follow statements printed in the same monograph: existence and uniqueness of a proximal minimizer from (1.1)–(1.2); the subdifferential optimality condition for a proximal minimizer in §2.3; the fixed-point characterization of minimizers in §2.3; the full-domain, single-valued resolvent identity (3.4); and the condition $0\in\nabla f(x^\star)+\partial g(x^\star)$ for minimizing $f+g$ in §4.2.1. The resolvent milestone includes its domain and uniqueness claims because the paper states both, rather than only an equality of partially defined relations. These targets retain the authors' constants $\tfrac12$ , $\tfrac1{2\lambda}$ and $\lambda$ .

Why the result matters

The equivalence identifies the solutions of a composite convex problem using an update rule that treats the smooth and nonsmooth terms differently. It applies when $g$ encodes constraints or a nonsmooth penalty and still characterizes the exact minimizers. It also says what a converged proximal gradient iteration must solve. The characterization by itself makes no claim that an iteration converges, a distinction made in the paper's discussion on p. 151. Parikh and Boyd, §4.2.1, give the fixed-point view of the algorithm in precisely this setting.

The formalization connects an existing machine-checked proximal-point definition from the Moreau 1965 series to a new Euclidean subdifferential defined by the supporting inequality (2.3). It leaves reusable statements about proximal optimality and resolvents alongside the composite result. A related published theorem, ProxNewton.Inexact.compGradStep_eq_zero_iff, characterizes minimizers through a composite-gradient step at unit step length under stronger smoothness assumptions and a different proximal representation. The present target preserves the monograph's arbitrary positive $\lambda$ , its extended-real $g$ , and its particular proximal operator.

Difficulty

The two sides of the goal compare different minimization problems. The left side minimizes $f+g$ globally; the right side minimizes a quadratic centered at $x^\star-\lambda\nabla f(x^\star)$ plus $\lambda g$ . Merely expanding the definition of the proximal operator does not make these objectives identical. The needed first-order conditions must also remain valid when $g$ is infinite outside its domain and its subdifferential is set-valued. In (3.4), an inverse relation is asserted to have a value at every point and only one value there; an equality that overlooks either property would be weaker than the paper's statement.

Formalization scope

The Lean carrier is EuclideanSpace ℝ (Fin n) for arbitrary $n\in\mathbb N$ . Its norm and inner product are the paper's Euclidean ones. No positive-dimension hypothesis is imposed: the zero-dimensional case is a singleton space and does not invalidate these identities. Values of $g$ are in EReal; the imported MoreauProx.Decomposition.GammaZero records that $g$ never equals $-\infty$ , is finite somewhere, has a convex epigraph, and is lower semicontinuous. For real-valued convex $f$ on all of $\mathbb R^n$ , closedness and properness follow from finiteness and convexity. Differentiability is explicit so Mathlib's gradient f x represents the intended $\nabla f(x)$ .

The imported MoreauProx.Decomposition.IsProx is a predicate saying that a point minimizes $\tfrac12\|u-v\|_2^2+\lambda g(u)$ . Positive $\lambda$ makes its minimizers those of the paper's (1.2), including at points where $g(u)=+\infty$ . Uniqueness is supplied by the referenced Moreau strict-minimum theorem. The local subdifferential follows (2.3): it is empty when its argument lies outside the effective domain, and it tests the supporting inequality over all $z\in\mathbb R^n$ . Outside $\operatorname{dom}g$ the right side is $+\infty$ , so those tests add no restriction. The composite minimization condition ranges over every $y\in\mathbb R^n$ and compares extended-real values.

The goal must relate these two genuinely different minimization problems through the gradient and convexity; defining the forward-backward operator to minimize $f+g$ would empty the theorem of its content. Contributions on extended-real subgradient calculus, the full-domain resolvent relation, and the composite optimality condition are welcome. The imported Moreau definitions and the local supporting-inequality subdifferential are reusable in further convex optimization developments.

This source PDF is the authors' Foundations and Trends formatted copy of the published monograph. Printed page numbers throughout this mission refer to that copy; its body begins on PDF page 5 at printed p. 123.

Selected references

Neal Parikh and Stephen Boyd, Proximal Algorithms, Foundations and Trends in Optimization 1(3), 2014. DOI: 10.1561/2400000003.

8 thms4 active usersReviewed

Combinatorics Machine Learning·Captain: mikedeng1

Online Learning and Online Convex Optimization 4: Finite Littlestone Dimension Gives Agnostic Online Regret 2√(Ldim·ln(eT/Ldim)·T)Research Paper

Motivation

Online classification is the simplest model of learning from a stream: on every round a learner sees an instance, guesses its binary label, and is then told the truth. Cover's impossibility argument shows that against an adversary no deterministic learner can compete with even two fixed hypotheses, so two relaxations are studied. In the realizable case the labels are generated by some unknown hypothesis of a known class $H$ , and the question is how many mistakes a learner must make. In the agnostic (unrealizable) case the labels are arbitrary, the learner may randomize, and it is judged by its regret: its expected number of mistakes minus that of the best hypothesis in $H$ in hindsight.

For the realizable case Littlestone (1988) introduced the dimension now named after him and showed that it is exactly the optimal mistake bound. Whether the same quantity also governs the agnostic case was settled by Ben-David, Pál and Shalev-Shwartz (COLT 2009, link): a class is agnostically online learnable if and only if its Littlestone dimension is finite. This mission formalizes the upper-bound half of that result, in the form given by Shalev-Shwartz's survey Online Learning and Online Convex Optimization (Found. Trends Mach. Learn. 4(2), 2011, doi:10.1561/2200000018), Theorem 3.6.

Timeline:

1988 — Littlestone defines the dimension and the Standard Optimal Algorithm (SOA) for the realizable case (doi:10.1007/BF00116827).
1994 — Littlestone and Warmuth publish the Weighted Majority algorithm for prediction with expert advice (doi:10.1006/inco.1994.1009).
2009 — Ben-David, Pál, Shalev-Shwartz: agnostic online learnability is characterized by finite Littlestone dimension, regret $O(\sqrt{\mathrm{Ldim}(H)\, T \ln T})$ , with a lower bound $\Omega(\sqrt{\mathrm{Ldim}(H)\,T})$ .
2011 — the survey presents the expert construction and the upper bound in the form formalized here.

Setting

Let $X$ be a set of instances and let a hypothesis class $H$ be a set of functions $h : X \to \{0,1\}$ . On round $t = 1, \dots, T$ the learner receives $x_t$ , outputs $p_t \in [0,1]$ (the probability of predicting $1$ ), receives $y_t \in \{0,1\}$ and pays $|p_t - y_t|$ , the probability of a wrong randomized guess. The prediction $p_t$ may depend on $(x_1,y_1),\dots,(x_{t-1},y_{t-1})$ and $x_t$ , never on $y_t$ . The regret against $h \in H$ is

\sum_{t=1}^T |p_t - y_t| - \sum_{t=1}^T |h(x_t) - y_t|.

A shattered tree of depth $d$ assigns an instance to every node of a complete binary tree of depth $d$ , so that for every labelling $(y_1,\dots,y_d)$ some $h \in H$ agrees with $y_t$ at the $t$ -th node of the root-to-leaf path that the labels select. The Littlestone dimension $\mathrm{Ldim}(H)$ is the largest depth of a shattered tree.

The Standard Optimal Algorithm keeps the version space $V_t$ of hypotheses consistent so far, splits it as $V_t^{(r)} = \{h \in V_t : h(x_t) = r\}$ , and predicts the $r$ with the larger $\mathrm{Ldim}(V_t^{(r)})$ . For a set $I = \{i_1 < \dots < i_L\}$ of rounds, Expert $(i_1,\dots,i_L)$ runs the same rule but flips its prediction on the rounds of $I$ and updates $V_{t+1} = V_t^{(\hat y_t)}$ using its own prediction instead of the label. Weighted Majority over $d$ experts with costs $z_t \in [0,1]^d$ keeps weights $w_t[i] \propto \exp(-\eta \sum_{s<t} z_s[i])$ and pays $\langle w_t, z_t\rangle$ .

Formalization targets

Goal: Theorem 3.6, upper bound

For every class $H$ with $L = \mathrm{Ldim}(H) < \infty$ and every horizon $T \ge L$ there is an online learner with $p_t \in [0,1]$ such that for every $h \in H$ and every sequence of $T$ examples

\sum_{t=1}^T |p_t - y_t| - \sum_{t=1}^T |h(x_t) - y_t| \le 2\sqrt{L \ln(eT/L)\, T}.

The paper states $O(\sqrt{\mathrm{Ldim}(H)\ln(T)\,T})$ ; the constant $2$ and the factor $\ln(eT/L)$ are what its proof gives.

Milestones

Lemma 3.3: SOA makes at most $\mathrm{Ldim}(H)$ mistakes in the realizable case (already proved on the platform).
Lemma 3.7: for every $h \in H$ and instance sequence some Expert $(i_1,\dots,i_L)$ with $L \le \mathrm{Ldim}(H)$ predicts $h(x_t)$ on every round.
Corollary 3.8: some such expert makes at most $\min_{h \in H}\sum_t |h(x_t) - y_t|$ mistakes.
Equation (3.1): $\sum_{L=0}^{\mathrm{Ldim}(H)} \binom{T}{L} \le (eT/\mathrm{Ldim}(H))^{\mathrm{Ldim}(H)}$ .
Theorem 3.1: Weighted Majority has regret at most $\log(d)/\eta + \eta T$ , and $2\sqrt{\log(d)\,T}$ for $\eta = \sqrt{\log(d)/T}$ .

Significance

The theorem shows that finiteness of one combinatorial parameter suffices for sublinear agnostic regret, for classes that may be infinite and need not have any parametric structure. With the lower bound it characterizes agnostic online learnability, parallel to the role of the VC dimension in PAC learning; the gap between the two dimensions (thresholds on $[0,1]$ have VC dimension $1$ and infinite Littlestone dimension) separates online from batch learnability. The expert construction, which simulates a realizable-case learner on guessed mistake rounds, is a reusable reduction from agnostic to realizable online learning.

On the formal side, the realizable theory (Littlestone dimension, SOA and its mistake bound) is already on the platform as published definitions and theorems from the textbook Understanding Machine Learning; the agnostic step, the expert construction, the bound on the number of experts and the Weighted Majority bound with bounded costs are not. To our knowledge no proof assistant library contains a machine-checked proof of the agnostic upper bound.

Difficulty

The obvious approach, running Weighted Majority with one expert per hypothesis, fails for infinite $H$ and gives $\log|H|$ instead of $\mathrm{Ldim}(H)$ for finite $H$ . The class must be replaced by a finite family that reproduces every $h \in H$ on the given instance sequence while having only $\mathrm{poly}(T)^{\mathrm{Ldim}(H)}$ members. The experts in the family never see labels, so the argument that each $h$ is reproduced must track two runs, the expert's and SOA's on labels generated by $h$ , and show their version spaces coincide round by round. This depends on the tie-breaking rule and on how an empty side $V_t^{(r)}$ is ranked, details the informal argument leaves implicit. The bound on the number of experts is a Sauer-type binomial estimate that holds only in the range $1 \le \mathrm{Ldim}(H) \le T$ .

Formalization scope

The development reuses the published definitions UnderstandingML_Online (online algorithms as maps from the history and the current instance to a prediction, history, mistakes, cumLoss, cumLossHyp, ldim, ldimBot, soa, wmWeights) and the proved theorem UnderstandingML.soa_mistake_bound (Lemma 3.3). Sequences are indexed by Fin T and rounds from $0$ ; the paper's indices $1 \le i_1 < \dots < i_L \le T$ become a set $I \subseteq \{0,\dots,T-1\}$ . A learner of type OnlineAlgR X cannot read the current label, so the existential goal cannot be satisfied by a learner that peeks at $y_t$ ; the goal also requires $p_t \in [0,1]$ . Logarithms are natural.

Committed conventions:

The O(·) of Theorem 3.6 is instantiated as $2\sqrt{L\ln(eT/L)\,T}$ under $T \ge L$ , where $L = \mathrm{Ldim}(H)$ is a natural number. At $L = 0$ the bound reads regret $\le 0$ .
Expert $(i_1,\dots,i_L)$ breaks ties toward $0$ , as its box on p. 166 says; the SOA box (p. 163) breaks ties toward $1$ . Lemma 3.7 holds with the expert's rule. An empty $V_t^{(r)}$ ranks below every nonempty class (ldimBot).
Theorem 3.1's bound 1 is stated for every $\eta > 0$ , bound 2 for $\eta \in (0,1)$ , the tuned bound for every $d \ge 1$ , $T \ge 0$ ; minima over experts and over $H$ are stated as "for every expert", "for every $h$ ".
Equation (3.1) is stated with $1 \le L \le T$ , together with the count of index sets.

Excluded: the lower bound $\Omega(\sqrt{\mathrm{Ldim}(H)\,T})$ (the survey cites it to Ben-David, Pál and Shalev-Shwartz), Theorem 3.5 (VC dimension at most Littlestone dimension), Corollary 3.4. Lemma 3.2 and the Halving bound are already on the platform.

Welcome contributions: proofs of the milestones, a proof of SOA's mistake bound with ties toward $0$ , and a reusable version of the Weighted Majority bound for general finite expert types.

Selected references

S. Shalev-Shwartz, Online Learning and Online Convex Optimization, Foundations and Trends in Machine Learning 4(2), 2011, 107–194. https://doi.org/10.1561/2200000018
S. Ben-David, D. Pál, S. Shalev-Shwartz, Agnostic Online Learning, COLT 2009. https://www.cs.mcgill.ca/~colt2009/papers/032.pdf
N. Littlestone, Learning Quickly When Irrelevant Attributes Abound: A New Linear-Threshold Algorithm, Machine Learning 2, 1988, 285–318. https://doi.org/10.1007/BF00116827
N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 1994, 212–261. https://doi.org/10.1006/inco.1994.1009

8 thms4 active usersReviewed

Completed

Convex Optimization Machine Learning·Captain: mikedeng1

Online Learning and Online Convex Optimization 2: Normalized Exponentiated Gradient Has Regret at Most log(d)/η + η Σₜ Σᵢ wₜ[i]zₜ[i]² When ηzₜ[i] ≥ −1Research Paper

Motivation

Learning with expert advice and online linear optimization over the probability simplex are the basic models behind boosting, multiplicative-weights methods for linear programming and zero-sum games, and adversarial bandit algorithms. The algorithm that solves them, under the names Weighted Majority, Hedge and Exponentiated Gradient (EG), keeps a probability vector over $d$ coordinates and multiplies each weight by $e^{-\eta z_t[i]}$ after observing the loss vector $z_t$ .

Littlestone and Warmuth (1994) introduced Weighted Majority for predicting with expert advice (doi:10.1006/inco.1994.1009).
Freund and Schapire (1997) analysed the same update as Hedge, for losses in $[0,1]$ (doi:10.1006/jcss.1997.1504).
Kivinen and Warmuth (1997) introduced Exponentiated Gradient as an online algorithm for linear prediction (doi:10.1006/inco.1996.2612).
Beck and Teboulle (2003) identified the update as mirror descent with the entropy on the simplex (doi:10.1016/S0167-6377(02)00231-6).
Shalev-Shwartz's survey (2011/2012) derives it as Online Mirror Descent with a normalized-entropy regularizer and proves, by Fenchel duality, a regret bound in which each round contributes a local norm of the loss vector instead of its sup norm (doi:10.1561/2200000018, §2.8).

The local-norm form is the one needed when loss vectors are large on coordinates of small weight, which is the situation of importance-weighted loss estimates in adversarial bandits.

Setting

Fix a dimension $d \ge 1$ and a learning rate $\eta > 0$ . In round $t = 1, 2, \dots$ the learner plays a vector $w_t$ in the probability simplex $S = \{w \in \mathbb R^d : w \ge 0,\ \sum_i w[i] = 1\}$ , then observes a loss vector $z_t \in \mathbb R^d$ and suffers the linear loss $\langle w_t, z_t\rangle$ . Write $z_{1:t} = z_1 + \dots + z_t$ .

Normalized EG starts from $w_1 = (1/d, \dots, 1/d)$ and updates

w_{t+1}[i] = \frac{w_t[i]\, e^{-\eta z_t[i]}}{\sum_j w_t[j]\, e^{-\eta z_t[j]}}, \qquad\text{equivalently}\qquad w_t[i] = \frac{e^{-\eta z_{1:t-1}[i]}}{\sum_j e^{-\eta z_{1:t-1}[j]}} .

Its regret against a comparator $u \in S$ after $T$ rounds is $\sum_{t=1}^T \langle w_t - u, z_t\rangle$ .

The analysis is phrased for general Online Mirror Descent (OMD): given a link function $g$ , predict $w_t = g(-z_{1:t-1})$ . For a regularizer $R$ on a set $S$ (equal to $+\infty$ off $S$ ), the Fenchel conjugate is $R^\star(\theta) = \sup_{w\in S} (\langle w,\theta\rangle - R(w))$ , and the Bregman divergence of a differentiable $F$ is $D_F(a\,\|\,b) = F(a) - F(b) - \langle \nabla F(b), a - b\rangle$ . Normalized EG is OMD with $g = \nabla R^\star$ for the normalized entropy $R(w) = \frac1\eta\sum_i w[i]\log w[i]$ on $S$ , whose conjugate is $R^\star(\theta) = \frac1\eta\log\sum_i e^{\eta\theta[i]}$ and whose gradient is the softmax.

Formalization targets

Goal: Theorem 2.22 (p. 153)

If $\eta z_t[i] \ge -1$ for all $t$ and $i$ , then for every $T$ and every $u \in S$ ,

\sum_{t=1}^T \langle w_t - u, z_t\rangle \le \frac{\log d}{\eta} + \eta \sum_{t=1}^T \sum_{i=1}^d w_t[i]\, z_t[i]^2 .

The comparator is unquantified on the page; it ranges over the simplex $S$ , the competing set of the normalized-entropy regularizer. The bound fails for $u$ outside $S$ .

Milestones, in proof order

Lemma 2.20 (p. 150). OMD with link $g = \nabla R^\star$ satisfies, for every $u \in S$ ,

\sum_{t=1}^T \langle w_t - u, z_t\rangle \le R(u) - R(w_1) + \sum_{t=1}^T D_{R^\star}(-z_{1:t}\,\|\,-z_{1:t-1}),

with equality for a minimizer of $R(u) + \sum_t\langle u, z_t\rangle$ over $S$ . 2. (2.16)–(2.18) (p. 153). For $R^\star(\theta) = \frac1\eta\log\sum_i e^{\eta\theta[i]}$ , the gradient is the softmax, $w_t = \nabla R^\star(-z_{1:t-1})$ , and

D_{R^\star}(-z_{1:t}\,\|\,-z_{1:t-1}) = \frac1\eta \log\Big(\sum_i w_t[i]\, e^{-\eta z_t[i]}\Big) + \langle w_t, z_t\rangle .

The per-round bound (pp. 153–154). If $\eta z_t[i] \ge -1$ for every $i$ , then $D_{R^\star}(-z_{1:t}\,\|\,-z_{1:t-1}) \le \eta\sum_i w_t[i]\, z_t[i]^2$ .

Significance

The result. Since $\sum_i w_t[i] z_t[i]^2 \le \|z_t\|_\infty^2$ , Theorem 2.22 improves the standard bound $\log(d)/\eta + \eta\sum_t\|z_t\|_\infty^2$ of normalized EG. The improvement matters when a coordinate with tiny weight carries a huge loss: the local norm weights that loss by its probability. This is what gives the $O(\sqrt{dT\log d})$ regret of Exp3-type bandit algorithms, whose loss estimates are of order $1/w_t[i]$ . The theorem allows negative losses down to $-1/\eta$ , so it also applies to gains and to centred or shifted losses.

Formalizing it. The theorem is proved in the survey; no machine-checked proof of it is known. The platform has a proved Hedge bound for non-negative losses compared with a single expert (Hazan, Introduction to Online Convex Optimization, Theorem 1.5). It does not imply Theorem 2.22: the latter allows negative losses, and its local-norm term is not invariant under shifting $z_t$ by a constant vector, so the shift that reduces signed losses to non-negative ones changes the bound. Lemma 2.20 is a general duality identity for OMD and is reusable for every OMD instance (Euclidean, $p$ -norm, unnormalized entropy).

Difficulty

The obvious argument for Hedge tracks the potential $\log\sum_i e^{-\eta z_{1:t}[i]}$ and bounds the one-step increase using $e^{-a} \le 1 - a + a^2/2$ for $a \ge 0$ . With negative losses that inequality fails. The weaker form $e^{-a} \le 1 - a + a^2$ is valid only for $a \ge -1$ , which is where the hypothesis $\eta z_t[i] \ge -1$ comes from. The bound is also stated against the whole simplex, not against single experts, so the potential argument has to be combined with an entropy bound for a general comparator.

Formalization scope

Vectors are Fin d → ℝ, with 0 < d and 0 < η. Rounds are numbered from $0$ in Lean, so index $t$ is the paper's round $t+1$ and sums over rounds run over Finset.range T.
The algorithm is the published definition UnderstandingML.wmWeights η z t (reference item UnderstandingML_Online), which is exactly the closed form of normalized EG for arbitrary real loss vectors; wmWeights η z 0 is the uniform vector $w_1$ .
The comparator in the goal ranges over the probability simplex (0 ≤ u i, ∑ i, u i = 1). A statement over all $u \in \mathbb R^d$ is false, and a statement over vertices only would be the weaker expert bound; both are ruled out.
$\log$ is the natural logarithm; all its arguments in the statements are positive.
Lemma 2.20 is stated on a real Hilbert space $E$ with a real-valued $R$ and a set $S$ . " $g = \nabla R^\star$ " is three hypotheses: $g$ maps into $S$ , $g(\theta)$ attains the supremum defining $R^\star(\theta)$ , and $R^\star$ has gradient $g(\theta)$ at $\theta$ . Differentiability of $R^\star$ is the paper's consequence of Lemma 2.19, which is cited to the literature and is assumed here. These hypotheses are satisfiable; a sorry-free check on $E = \mathbb R$ with $R(w) = w^2/2$ accompanies the draft.
The Bregman divergence of the log-sum-exp conjugate on $\mathbb R^d$ is written with explicit coordinate sums, and its gradient is stated as a Fréchet derivative, because Fin d → ℝ carries the sup norm in Mathlib.
The theorem has no $O(\cdot)$ ; all constants are the paper's.
Not included: Theorem 2.15 and Corollary 2.16 (the $\|z_t\|_\infty^2$ bound via strong convexity), Theorem 2.21 (which rests on Lemma 2.19), Theorem 2.23 (unnormalized EG, in the Winnow mission of this series), Theorem 3.1 and Corollary 4.2.

Welcome contributions: proofs of the three milestones and of the goal, and general Mathlib-style lemmas on the gradient of log-sum-exp and on the Fenchel–Young inequality for conjugates defined as suprema over a set.

Selected references

S. Shalev-Shwartz, Online Learning and Online Convex Optimization, Foundations and Trends in Machine Learning 4(2), 107–194, 2011 (© 2012). doi:10.1561/2200000018
J. Kivinen and M. K. Warmuth, Exponentiated gradient versus gradient descent for linear predictors, Information and Computation 132(1), 1–63, 1997. doi:10.1006/inco.1996.2612
Y. Freund and R. E. Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, Journal of Computer and System Sciences 55(1), 119–139, 1997. doi:10.1006/jcss.1997.1504
N. Littlestone and M. K. Warmuth, The weighted majority algorithm, Information and Computation 108(2), 212–261, 1994. doi:10.1006/inco.1994.1009
A. Beck and M. Teboulle, Mirror descent and nonlinear projected subgradient methods for convex optimization, Operations Research Letters 31(3), 167–175, 2003. doi:10.1016/S0167-6377(02)00231-6
E. Hazan, Introduction to Online Convex Optimization, 2nd ed., MIT Press, 2022. arXiv:1909.05207

6 thms4 active usersReviewed

Completed

Convex Optimization Machine Learning Optimization·Captain: mikedeng1

Making Gradient Descent Optimal for Strongly Convex Stochastic Optimization 1: SGD with α-Suffix Averaging Attains E[F(w̄ᵅ_T)] − F(w*) ≤ (2 + 2.5 log(1/(1−α)))G²/(αλT)Research Paper

Motivation

Stochastic gradient descent (SGD) is the default method for minimizing an expected loss $F(w)=\mathbb E_z[\ell(w,z)]$ when only noisy gradients are available, which is the situation of nearly every large-scale learning problem. When $F$ is strongly convex (for instance, any convex loss with an $\ell_2$ regularizer), information-theoretic lower bounds show that no method using $T$ noisy gradients can guarantee an error better than order $1/T$ , and some algorithms achieve this rate.

For plain SGD with step sizes $\eta_t=1/(\lambda t)$ and the standard averaged output, however, the classical analysis gives only $O(\log T/T)$ . Rakhlin, Shamir and Sridharan (arXiv:1109.5647, ICML 2012) showed that the logarithm is real for full averaging on non-smooth problems, and that a minimal change to the output, averaging only the last fraction $\alpha$ of the iterates, restores the optimal $O(1/T)$ rate. This mission formalizes that positive result, the paper's main theorem.

Timeline of the relevant results:

2007. Hazan, Agarwal and Kale (Machine Learning 69) prove an $O(\log T)$ regret bound for online gradient descent on strongly convex losses, which by online-to-batch conversion gives $O(\log T/T)$ for averaged SGD.
2009. Nemirovski, Juditsky, Lan and Shapiro (SIAM J. Optim. 19) show an $O(1/T)$ rate for the last SGD iterate when $F$ is in addition smooth.
2011. Hazan and Kale (COLT 2011) obtain $O(1/T)$ for non-smooth strongly convex problems with a different, epoch-based algorithm.
2012. Rakhlin, Shamir and Sridharan prove that SGD with full averaging can suffer $\Omega(\log T/T)$ , and that α-suffix averaging achieves $O(1/T)$ (Theorem 5).

Setting

Let $W\subseteq\mathbb R^d$ be a closed convex set containing $0$ , and let $F:\mathbb R^d\to\mathbb R$ . The function $F$ is $\lambda$ -strongly convex on $W$ ( $\lambda>0$ ) if

F(\theta x+(1-\theta)y)\le\theta F(x)+(1-\theta)F(y)-\tfrac\lambda2\theta(1-\theta)\|x-y\|^2\qquad(x,y\in W,\ \theta\in[0,1]).

A point $w^*\in W$ is a minimizer of $F$ over $W$ .

Information about $F$ comes from a stochastic gradient oracle $g(w,z)$ : at a query point $w$ , a sample $z\sim D$ is drawn and $\hat g=g(w,z)$ is returned. The oracle is unbiased in the sense that its mean $\bar g(w)=\mathbb E_{z\sim D}\,g(w,z)$ is a subgradient of $F$ relative to $W$ : $F(u)\ge F(w)+\langle u-w,\bar g(w)\rangle$ for all $u\in W$ . Its second moment is bounded: $\mathbb E_z\|g(w,z)\|^2\le G^2$ at every $w\in W$ .

Projected SGD with step sizes $\eta_t=1/(\lambda t)$ runs on an i.i.d. sample $z_1,\dots,z_T\sim D$ :

w_1=0,\qquad w_{t+1}=\Pi_W\big(w_t-\eta_t\,g(w_t,z_t)\big),

where $\Pi_W$ is the Euclidean projection onto $W$ . For $\alpha\in(0,1)$ with $(1-\alpha)T$ an integer, the α-suffix average is

\bar w^\alpha_T=\frac{w_{(1-\alpha)T+1}+\dots+w_T}{\alpha T}.

In Lean the iterates are UnderstandingML.sgdStrongIterates lam W g S, the oracle mean is oracleMean D g, the suffix average is suffixAverage lam W g S k with $k=(1-\alpha)T$ , and expectations are integrals against the product law UnderstandingML.iidLaw D T.

Formalization targets

Goal: Theorem 5

\mathbb E\big[F(\bar w^\alpha_T)-F(w^*)\big]\ \le\ \frac{2+2.5\log\frac1{1-\alpha}}{\alpha}\cdot\frac{G^2}{\lambda T},

together with the finiteness of $\mathbb E\,F(\bar w^\alpha_T)$ . The constants are the paper's.

Milestones, in the order the proof uses them

Lemma 2 (p. 12): $\mathbb E_z\|g(w,z)\|^2\le G^2$ at $w\in W$ implies $\|w-w^*\|^2\le 4G^2/\lambda^2$ .
Lemma 1 (p. 4): $\mathbb E\|w_t-w^*\|^2\le 4G^2/(\lambda^2t)$ for every $t\ge1$ .
(3) (p. 6): $\sum_{t=k+1}^T\mathbb E\langle g_t,w_t-w^*\rangle\le\sum_{t=k+1}^T\frac{\eta_tG^2}2+\sum_{t=k+1}^T\frac{\mathbb E\|w_t-w^*\|^2-\mathbb E\|w_{t+1}-w^*\|^2}{2\eta_t}$ .
App. B.6, convexity display (p. 18): $\sum_{t}\mathbb E\langle g_t,w_t-w^*\rangle\ge\sum_t\mathbb E[F(w_t)-F(w^*)]\ge\alpha T\,\mathbb E[F(\bar w^\alpha_T)-F(w^*)]$ .
App. B.6, penultimate bound (p. 18): $\mathbb E[F(\bar w^\alpha_T)-F(w^*)]\le\frac{2G^2}{\alpha T\lambda}(1+H)+\frac{G^2}{2\alpha T\lambda}H$ with $H=\sum_{t=(1-\alpha)T+1}^T 1/t$ .
App. B.6, harmonic bound (p. 18): $H\le\log\frac1{1-\alpha}$ .

Significance

Theorem 5 shows that the suboptimal $\log T$ factor of averaged SGD on non-smooth strongly convex problems is an artifact of which iterates are averaged, not of the gradient steps themselves: the same iterates, averaged over a constant fraction at the end, reach the minimax-optimal $O(G^2/(\lambda T))$ rate up to constants. This matches Hazan and Kale's guarantee with an unmodified algorithm, and the same paper's lower bound shows that full averaging cannot match it.

The result is proved in the paper; nothing in it is formalized. The platform holds the Understanding Machine Learning SGD model and its $O(\log T/T)$ bound for full averaging (UnderstandingML.sgd_strongly_convex), but no $O(1/T)$ rate for SGD on a non-smooth objective. The mission produces a machine-checked proof of Theorem 5 with its explicit constants and, along the way, of Lemma 1 (the $O(1/t)$ mean-square convergence of the last iterate), which is reused by every $O(1/T)$ analysis of SGD with step sizes $1/(\lambda t)$ , including the paper's smooth-case Theorems 1 and 2.

Difficulty

The obvious argument, the online-gradient-descent regret bound summed over all rounds and divided by $T$ , produces $\sum_{t\le T}\eta_t G^2\approx G^2\log T/\lambda$ and so cannot avoid the logarithm. Discarding early iterates does not by itself help: the resulting bound depends on the distance $\mathbb E\|w_t-w^*\|^2$ of the iterate at which the suffix starts, at the scale $1/t$ , and the regret analysis says nothing about individual iterates of a non-smooth problem.

The formal difficulties are probabilistic. The iterates are random vectors built by composing a measurable oracle with a projection defined by choice; conditioning on the past to evaluate $\mathbb E\langle g(w_t,z_t),w_t-w^*\rangle$ requires the product structure of the sample; and every expectation must be shown finite, including that of $F(\bar w^\alpha_T)$ with $F$ not assumed measurable.

Formalization scope

Space. $\mathbb R^d$ with the Euclidean inner product (UnderstandingML.Vec d); the paper allows any Hilbert space.
Domain. W closed and convex with 0 ∈ W (the paper's $w_1=0\in W$ ; closedness makes $\Pi_W$ well defined).
Strong convexity. Mathlib's StrongConvexOn W lam F with modulus $\frac\lambda2\|x-y\|^2$ , equivalent to the paper's (1) when subgradients relative to $W$ exist at every point, which the oracle provides.
Oracle. IsSubgradientOracleOn W F D g: for $w\in W$ , $g(w,\cdot)$ is integrable and its mean is a subgradient of $F$ relative to $W$ . The oracle is jointly measurable and $D$ is a probability measure. The subgradient condition is not global: $F$ is only assumed convex on $W$ .
Second moment. $\int^{-}\|g(w,z)\|^2\,dD\le G^2$ at every $w\in W$ (the paper's "regardless of how the iterates evolve"). Theorem 5's statement on p. 6 prints $\mathbb E\|\hat g_t\|^2\le G$ ; the standing assumption on p. 3 and the proof use $G^2$ , which is what is formalized.
Indices. sgdStrongIterates … t is the paper's $w_{t+1}$ ; the suffix average runs over indices $k,\dots,T-1$ , $k=(1-\alpha)T$ , passed as a natural number with $(k:\mathbb R)=(1-\alpha)T$ , which encodes that $\alpha T$ and $(1-\alpha)T$ are integers.
Logarithm. Real.log, the natural logarithm.
Expectations. Every Bochner integral in a conclusion is accompanied by an integrability conjunct, and nonnegative quantities in Lemma 1 are lower Lebesgue integrals, so no bound holds through Lean's default value $0$ for non-integrable functions. The bounds are stated for the expectation over $S\sim D^T$ ; a pathwise version, or one in which $\hat g$ itself (rather than its mean) is a subgradient, would be a different and false or easier theorem.

Infrastructure a complete development needs: measurability of the projected iterates in the sample, the one-step conditional-expectation identity $\mathbb E\langle g(w_t,z_t),w_t-w^*\rangle=\mathbb E\langle\bar g(w_t),w_t-w^*\rangle$ for the product law, and the integral comparison $\sum_{t=k+1}^T 1/t\le\log(T/k)$ . The first two are reusable for the companion missions on the same paper and for any SGD analysis built on sgdStrongIterates. Proofs of any milestone, and of reusable lemmas about iidLaw and sgdStrongIterates, are welcome.

Selected references

A. Rakhlin, O. Shamir, K. Sridharan, Making Gradient Descent Optimal for Strongly Convex Stochastic Optimization, ICML 2012; arXiv:1109.5647v7, 2012. https://arxiv.org/abs/1109.5647
E. Hazan, A. Agarwal, S. Kale, Logarithmic regret algorithms for online convex optimization, Machine Learning 69 (2007) 169–192. https://doi.org/10.1007/s10994-007-5016-8
E. Hazan, S. Kale, Beyond the regret minimization barrier: an optimal algorithm for stochastic strongly-convex optimization, COLT 2011. https://proceedings.mlr.press/v19/hazan11a.html
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM J. Optim. 19 (2009) 1574–1609. https://doi.org/10.1137/070704277
S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Ch. 14. https://doi.org/10.1017/CBO9781107298019

10 thms4 active usersReviewed

Completed

Operations Research Probability·Captain: mikedeng1

A Note on Probability Distributions with Increasing Generalized Failure Rates I: X Is IGFR iff log X Is IFR iff X ⪯hr λX for All λ ≥ 1 iff Φ̄(ξ/θ) Is TP₂Research Paper

Motivation

In pricing and supply-chain contracting, demand or valuations are random, and the profit functions that arise are unimodal only under a shape condition on the distribution. A firm facing demand $D(p) = \bar\Phi(p)$ at price $p$ maximizes revenue $\pi(p) = p\bar\Phi(p)$ ; the first-order condition is $\bar\Phi(p)(1 - g(p)) = 0$ , where $g$ is the generalized failure rate introduced by Lariviere and Porteus (2001). When $g$ is increasing, it crosses $1$ at most once and the optimal price is unique. The same condition makes the supplier's problem unimodal in the price-only newsvendor contract (Lariviere and Porteus, 2001) and appears throughout revenue management. The condition is useful but often hard to verify for a given distribution.

Lariviere (2006) gives three equivalent reformulations of the condition (Theorem 1), two sufficient conditions (Corollary 1), and uses them to show that every beta distribution has an increasing generalized failure rate. The parts of the equivalence had appeared separately: Keilson and Sumita (1982) showed the equivalence of parts 2 and 3, and Ma (1999) linked parts 3 and 4.

Setting

Let $X$ be a nonnegative random variable with distribution function $\Phi$ and survival function $\bar\Phi(\xi) = 1 - \Phi(\xi)$ . Assume $\Phi$ has a density $\varphi$ , and let the support of $X$ be $(\alpha,\beta)$ with $0 \le \alpha < \beta \le \infty$ . The failure rate of $X$ is $h(\xi) = \varphi(\xi)/\bar\Phi(\xi)$ , and its generalized failure rate is

g(\xi) = \xi\,h(\xi).

$X$ is IFR if $h$ is weakly increasing on $\{\xi : \Phi(\xi) < 1\}$ , and IGFR if $g$ is weakly increasing on that set. Every IFR variable is IGFR; many variables with decreasing failure rate are IGFR as well.

Write $X_L = \log X$ , with distribution $\Phi_L$ , density $\varphi_L$ , survival $\bar\Phi_L$ and failure rate $h_L$ . Two nonnegative variables with failure rates $h_1, h_2$ are ordered in the hazard rate order, $X_1 \preceq_{hr} X_2$ , if $h_1(\xi) \ge h_2(\xi)$ for all $\xi \ge 0$ . A function $f(x,y)$ is totally positive of order 2 (TP₂) if

f(x_1,y_1)f(x_2,y_2) - f(x_1,y_2)f(x_2,y_1) \ge 0 \qquad\text{for } x_1 < x_2,\ y_1 < y_2 .

A function is log-concave if its logarithm is concave.

In the Lean development these are survival, failureRate, genFailureRate, IsIFR, IsIGFR, HazardRateLE and IsTP2On in the namespace LariviereIGFR.Char, and log-concavity is the platform predicate ConvexOptimization.LogConcaveOn.

Formalization targets

Goal: Theorem 1 (p. 603)

The following are equivalent:

\text{(1) } X \text{ is IGFR};\quad \text{(2) } X_L \text{ is IFR};\quad \text{(3) } X \preceq_{hr} \lambda X \text{ for all } \lambda \ge 1;\quad \text{(4) } f(\xi,\theta) = \bar\Phi(\xi/\theta) \text{ is TP}_2 .

Milestones (the clauses of the proof)

$\bar\Phi_L(\xi) = \bar\Phi(e^\xi)$ , and $\varphi_L(\xi) = e^\xi\varphi(e^\xi)$ is a density of $X_L$ .
$h_L(\xi) = g(e^\xi)$ and $h_L'(\xi) = e^\xi g'(e^\xi)$ .
Parts 1 and 2 are equivalent.
The generalized failure rate of $\lambda X$ is $g_\lambda(\xi) = g(\xi/\lambda)$ .
Parts 1 and 3 are equivalent.
A law on $\mathbb R$ is IFR if and only if $\bar\Phi(\xi - \theta)$ is TP₂ (Barlow and Proschan 1965).
$\bar\Phi_L(\xi - \theta)$ is TP₂ on $\mathbb R^2$ if and only if $\bar\Phi(\xi/\theta)$ is TP₂ on $(0,\infty)^2$ .

Companion statements

Corollary 1. If $\varphi(e^\xi)$ is log-concave, or $\xi\varphi(\xi)$ is increasing, on the support, then $X$ is IGFR.
Beta distributions. For all $a, b > 0$ the beta distribution is IGFR.
Powers (Paul 2005). If $X$ is IGFR, so is $\delta X^\nu$ for $\delta, \nu > 0$ .

Significance

Theorem 1 converts the IGFR condition into conditions with an established theory. Through part 2, every closure and comparison property of IFR distributions transfers to IGFR distributions under the logarithm: the lognormal distribution is IGFR because its logarithm is normal, and $\delta X^\nu$ inherits IGFR from $X$ . Part 3 has a direct operational reading: as a market scales up, a supplier selling to a newsvendor sells more and a service provider charges more. Part 4 places IGFR in the theory of total positivity. Corollary 1 gives density-level tests that need no closed form for $\Phi$ , which is what makes the beta family tractable.

The results are proved in the paper; none of them is formalized. A machine-checked development would supply reusable facts about image laws under $\log$ and scaling with explicit densities, the failure-rate form of the hazard rate order, and the classical Barlow–Proschan characterization of IFR distributions by total positivity, which is used well beyond this paper.

Difficulty

Parts 1 ⇔ 2 and 1 ⇔ 3 are computations once the laws of $\log X$ and $\lambda X$ and their densities are identified, but that identification is a change of variables for measures, together with a check that the transported density is again the derivative of the distribution function on the support. The substance is the Barlow–Proschan step, part 2 ⇔ 4. Monotonicity of $h_L$ is a pointwise statement about a density, while TP₂ of $\bar\Phi_L(\xi - \theta)$ is an inequality between products of tail probabilities; the bridge is log-concavity of $\bar\Phi_L$ on the support, and its extension across the endpoints of the support, where $\bar\Phi_L$ equals $1$ on one side and $0$ on the other. A naive reading that differentiates everywhere fails at those endpoints and wherever the density is changed on a null set.

Formalization scope

Laws, not random variables. $X$ is a probability measure $\mu$ on $\mathbb R$ with $\mu((-\infty,0)) = 0$ . $X_L$ is the image of $\mu$ under Real.log, and $\lambda X$ is the image under $x \mapsto \lambda x$ ; both maps are measurable, so the images are genuine probability laws. The junk value $\log 0 = 0$ is harmless because $\mu$ has no atom at $0$ .
The density version is pinned. A density is determined only up to a null set, while IFR and IGFR read it pointwise; with an arbitrary version Theorem 1 is false. Every statement assumes IsRegDensity μ φ: $\varphi \ge 0$ , $\mu$ has density $\varphi$ , $\varphi = \Phi'$ at every point of $\{0 < \Phi < 1\} = (\alpha,\beta)$ , and $\varphi = 0$ where $\Phi = 0$ . The derived densities $e^\xi\varphi(e^\xi)$ and $\varphi(\xi/\lambda)/\lambda$ are proved to be regular as well (milestones 1 and 4).
Rates are read on $\{\Phi < 1\}$ . Lean's $x/0 = 0$ would otherwise make $h$ vanish where $\bar\Phi = 0$ . The hazard rate order compares $h_1(\xi) \ge h_2(\xi)$ for $\xi \ge 0$ with $\Phi_1(\xi) < 1$ ; at the other points the paper's $h_1$ is $+\infty$ and the inequality is automatic.
Monotonicity is weak, as in the paper's "weakly increasing". Part 3 quantifies over $\lambda \ge 1$ exactly; for $\lambda < 1$ the order reverses.
Part 4's domain is $(0,\infty)^2$ : $\theta > 0$ is forced by $\xi/\theta$ , and for $\xi \le 0$ the survival is identically $1$ , so nothing is lost. The Barlow–Proschan milestone is stated for an arbitrary law on $\mathbb R$ , because $X_L$ can be negative.
No trivialization. Part 2 is about the image law of $\log X$ , never a function such as $\xi \mapsto g(e^\xi)$ written in by hand, and part 3 is about the image law of $\lambda X$ ; otherwise the equivalences would hold by definition.
Additions disclosed. Corollary 1's conditions are read on the support, where the density is positive; "increasing" is read as weakly increasing. Corollary 2 (products of IGFR variables) is not included: the page omits the independence it needs, and the existence of a regular density version for the product was not established.

Contributions welcome: the change-of-variables lemmas for Measure.map with explicit densities, the identification of $\{0 < \Phi < 1\}$ as an open interval, and the Barlow–Proschan equivalence, which is reusable for any IFR result.

Selected references

M. A. Lariviere, A note on probability distributions with increasing generalized failure rates, Operations Research 54(3):602–604, 2006. https://doi.org/10.1287/opre.1060.0282
M. A. Lariviere and E. L. Porteus, Selling to the newsvendor: an analysis of price-only contracts, Manufacturing & Service Operations Management 3(4):293–305, 2001. https://doi.org/10.1287/msom.3.4.293.9971
R. E. Barlow and F. Proschan, Mathematical Theory of Reliability, Wiley, 1965 (reprinted SIAM, 1996). https://doi.org/10.1137/1.9781611971194
J. Keilson and U. Sumita, Uniform stochastic ordering and related inequalities, Canadian Journal of Statistics 10(3):181–198, 1982.
S. M. Ross, Stochastic Processes, Wiley, 1983.

10 thms4 active usersReviewed

Completed

Operations Research Stochastic Systems·Captain: mikedeng1

Little's Law as Viewed on Its 50th Anniversary: L = λW Holds Exactly Over Any Finite Window [0, T], With Nonzero Starting and Ending QueuesResearch Paper

Motivation

Little's Law, $L = \lambda W$ , relates three averages of a queuing system: the average number of items in the system $L$ , the average arrival rate $\lambda$ , and the average time an item spends in the system $W$ . It is used throughout operations management and computer architecture, where two of the three quantities are measured and the third is inferred.

The classical theorems (Little 1961; the sample-path proofs of Stidham 1974 and later work) are stated over the whole time axis $0 \le t < \infty$ and require the three averages to exist as limits. Every observation in practice is made over a finite period: a supermarket over one business day, a wine cellar over one year. In his fiftieth-anniversary survey (Little 2011), Little argues that for such data the right statement is a finite-window one, and proves in §2 that over any window $[0, T]$ the relation holds exactly, with no limits, no stationarity and no assumption on queue discipline or service.

Timeline:

1961, Little: $L = \lambda W$ for stationary processes over an infinite horizon.
1974, Stidham: a deterministic sample-path proof over $[0, \infty)$ , assuming the limits $\lambda$ and $W$ exist.
2008, Little and Graves: a textbook chapter on Little's Law, with the supermarket and wine-cellar examples that the 2011 paper reuses for finite windows.
2011, Little: Theorems LL.1 and LL.2 and the class-wise corollaries, the content of this mission.

Setting

The object is one deterministic sample path observed over a window $[0, T]$ with $0 < T < \infty$ . There are finitely many items $i = 1, \dots, M$ . Item $i$ arrives at time $a_i$ and leaves at time $d_i \ge a_i$ , and is in the system at time $t$ exactly when $a_i \le t < d_i$ . An item still present at $T$ is given any departure time $d_i > T$ .

$n(t) = \#\{i : a_i \le t < d_i\}$ is the number of items in the system at time $t$ (the published KellyStochasticNetworks.occupancy).
$A = \int_0^T n(t)\,dt$ is the area under $n(t)$ over $[0, T]$ .
Window empty at both ends (Theorem LL.1). Every item satisfies $0 \le a_i \le d_i \le T$ . Then $N$ is the number of items arriving in $[0, T]$ , $L = A/T$ , $\lambda = N/T$ , and $W = \frac1N\sum_i (d_i - a_i)$ is the average wait.
Nonzero starting and ending queues (Theorem LL.2). $S(T)$ is the cumulative number of items in the system over $[0, T]$ : the items present at $t = 0$ ( $a_i < 0 < d_i$ ) plus those arriving in $[0, T]$ ( $0 \le a_i \le T$ ). The time item $i$ spends in the system during $[0, T]$ is

w_i(T) = \max\bigl(0,\ \min(d_i, T) - \max(a_i, 0)\bigr).

Then $L(T) = A/T$ , $\lambda(T) = S(T)/T$ , and $W(T)$ is the average of $w_i(T)$ over the $S(T)$ counted items: the "average incremental age" added to the wines of a cellar during the year.

Classes. A class assignment $c$ splits the items into mutually exclusive classes $k = 1, \dots, K$ ; $L_k, \lambda_k, W_k$ are the quantities above computed from the class- $k$ items alone.

Formalization targets

Goal: Theorem LL.2 (Little's Law over $[0, T]$ , p. 539)

L(T) = \lambda(T)\, W(T)

for every sample path with $a_i \le d_i$ and every $0 < T < \infty$ , with items allowed at both ends of the window.

Milestones

The area identity for a window empty at both ends, $\int_0^T n(t)\,dt = \sum_i (d_i - a_i)$ , the step $W = A/N$ of the proof of LL.1 (already proved on the platform).
Theorem LL.1 (p. 537): $L = \lambda W$ for a window empty at $0$ and $T$ .
The step $W = A/S(T)$ of the proof of LL.2: $A = \sum_{i} w_i(T)$ over the $S(T)$ counted items.
§2.2.3, Corollary (3)(a): $L_k = \lambda_k W_k$ for every class $k$ .
§2.2.3, Corollary (3)(b): with $\lambda = \sum_k \lambda_k$ , $L = \sum_k L_k$ and $W = \sum_k (\lambda_k/\lambda) W_k$ , $L = \lambda W$ .

Significance

The result. Theorem LL.2 makes Little's Law a measurement identity: for any recorded day, month or year of operation, the three averages computed from the data satisfy $L = \lambda W$ exactly, whether or not the system was ever empty (Corollary (1)) and whether or not there is any service operation (Corollary (2)). This is what licenses inferring an unmeasured parameter from two measured ones on finite data, the use Little describes in §4 for supermarkets, factories and computer systems. Corollary (3) extends the identity to market segments and to their aggregate, with the aggregate wait an arrival-weighted average of the class waits.

Formalizing it. The infinite-horizon sample-path law is already proved on the platform (queueing_general_littles_law, by wenxinzhang), but its sample paths have no item present at time $0$ and its conclusion is a statement about limits. Only the empty-boundary area identity (milestone 1, from Kelly and Yudovina's Stochastic Networks) exists for finite windows. LL.1 as an identity of the three averages, LL.2, the truncated area identity and Corollary (3) are not formalized anywhere we know of. The mission produces finite-window definitions of $S(T)$ and of the time in window that later queueing missions can reuse.

Difficulty

The algebra of the paper's proof is one line once $W = A/S(T)$ is known. The content is that identity, which is an exchange of an integral over time with a sum over items in which every item's contribution is clipped to the window. An item present at $0$ contributes only its time after $0$ ; an item present at $T$ only its time before $T$ ; items that leave before $0$ or arrive after $T$ contribute nothing and must not be counted in $S(T)$ . Getting the boundary conventions right, so that each counted item contributes exactly the length of $[a_i, d_i) \cap [0, T]$ , is where an informal argument is easiest to get wrong. The naive reading " $W$ is $A$ divided by the number of items" makes the theorem a tautology and is ruled out below.

Formalization scope

Items are indexed by Fin M with real epochs a d : Fin M → ℝ. All of $L$ , $\lambda$ , $W$ , $S(T)$ , $N$ and $A$ are defined from the items; none is a free variable.
Presence is the half-open interval $[a_i, d_i)$ , inherited from KellyStochasticNetworks.occupancy. An item arriving exactly at $0$ is counted in $S(T)$ once, as an arrival in $[0, T]$ ; the paper's remark $S(0) = n(0)$ then holds except for an item that arrives and leaves at the same instant $0$ .
An item that has not left by $T$ carries any $d_i > T$ ; nothing after $T$ enters any quantity.
LL.1's "empty at $0$ and $T$ " is read as $0 \le a_i \le d_i \le T$ for every item, the hypothesis of the referenced Kelly identity.
Added hypotheses relative to the page: $0 < T$ (the page's $0 < T < \infty$ ) and $a_i \le d_i$ (an item leaves no earlier than it arrives).
If $N = 0$ or $S(T) = 0$ , the page's $W$ is undefined; Lean's division gives $0$ and both sides of every identity are $0$ , so no positivity hypothesis is added. In Corollary (3)(b), $\lambda = 0$ likewise gives $0 = 0$ .
No trivializing encoding. $W$ and $W(T)$ are averages of the individual waits; defining them as $A/N$ or $A/S(T)$ , or taking $L, \lambda, W$ as reals constrained by $L = A/T$ , would make every target a one-line rewrite and is not what is stated.
Page references are to the journal's typeset version; printed page = PDF page + 535.

Contributions welcome: proofs of the milestones and goal, and reusable lemmas computing $\int_0^T$ of indicator functions of intervals.

Selected references

J. D. C. Little, Little's Law as Viewed on Its 50th Anniversary, Operations Research 59(3):536–549, 2011. https://doi.org/10.1287/opre.1110.0940
J. D. C. Little, A Proof for the Queuing Formula: L = λW, Operations Research 9(3):383–387, 1961. https://doi.org/10.1287/opre.9.3.383
S. Stidham, A Last Word on L = λW, Operations Research 22(2):417–421, 1974. https://doi.org/10.1287/opre.22.2.417
J. D. C. Little and S. C. Graves, Little's Law, in D. Chhajed and T. J. Lowe (eds.), Building Intuition, Springer, 2008, pp. 81–100. https://doi.org/10.1007/978-0-387-73699-0_5
F. Kelly and E. Yudovina, Stochastic Networks, Cambridge University Press, 2014, §2.5. https://doi.org/10.1017/CBO9781139565363

9 thms4 active usersReviewed

Machine Learning Probability Theoretical Computer Science·Captain: mikedeng1

What Can We Learn Privately? II: Parity Functions Are Privately PAC Learnable from O(d log(1/β)/(εα)) ExamplesResearch Paper

Learning parities under differential privacy

Differential privacy (Dwork, McSherry, Nissim and Smith, 2006) requires a randomized algorithm's output distribution to change little when one individual's record is changed. PAC learning asks an algorithm to output, from i.i.d. labeled examples, a hypothesis whose error is small with high probability. Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith (arXiv:0803.0924v3; SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090) asked which concept classes can be learned under both requirements at once. All theorem, page and display numbers in this mission are those of the arXiv v3.

Their generic learner (§3, the subject of mission I of this series) learns every finite class privately with a polynomial number of examples, but its running time is exponential in the representation size for classes such as parity. Parity functions are the standard example of a class that is learnable efficiently by linear algebra and not learnable with statistical queries (Kearns, 1998; Blum et al., 1994), a model that was then the main known source of efficient private learners (Blum, Dwork, McSherry and Nissim, 2005). Section 4 of the paper gives an efficient private PAC learner for parity. The result separates efficient private learning from statistical-query learning, and the local (randomized-response) model from the centralized one (missions III–V).

Setting

For $d \ge 1$ and $r \in \{0,1\}^d$ , the parity function $c_r(x) = r \odot x$ is the inner product of $r$ and $x$ modulo 2; PARITY is $\{c_r : r \in \{0,1\}^d\}$ . A database is $z = (z_1,\dots,z_n)$ with $z_i = (x_i, y_i) \in \{0,1\}^d \times \{0,1\}$ . Two databases are neighbors if they differ in exactly one entry. A randomized algorithm $A$ , identified with the law $A(z)$ of its output, is $\varepsilon$ -differentially private if $\Pr[A(z) \in S] \le e^{\varepsilon}\Pr[A(z') \in S]$ for all neighbors $z, z'$ and all sets $S$ of outputs. $\mathrm{Lap}(s)$ is the Laplace distribution with density $\frac{1}{2s}e^{-|x|/s}$ .

For $S \subseteq [n]$ , $V_S \subseteq \mathbb Z_2^d$ is the solution space of the linear system $\{x_i \odot r = y_i : i \in S\}$ . The basic learner $\mathcal A(z,\varepsilon)$ outputs $\bot$ with probability $1/2$ ; otherwise it puts each $i \in [n]$ into $S$ independently with probability $p = \varepsilon/4$ and outputs $c_{r^*}$ for $r^*$ uniform in $V_S$ , or $\bot$ if $V_S = \emptyset$ .

The amplified learner $\mathcal A^*(z,\varepsilon,\alpha,\beta)$ sets $\beta' = \beta/2$ , $\alpha' = \alpha/5$ , $k = \lceil\log_{4/3}(1/\beta')\rceil$ , $n' = \lceil cd/(\varepsilon\alpha')\rceil$ , $s = \lceil (c'k/(\alpha'\varepsilon))\log_2(k/\beta')\rceil$ for constants $c, c'$ . If $n \le kn' + s$ it returns "insufficient samples". Otherwise it runs $\mathcal A$ on $k$ disjoint blocks of $n'$ examples, obtaining $h_1,\dots,h_k$ . It perturbs each training error on the next $s$ examples by independent $\mathrm{Lap}(k/(s\varepsilon))$ noise and outputs the $h_j$ with the least perturbed error.

For a distribution $\mathcal X$ on $\{0,1\}^d$ and a target $c_r$ , the error of $c_{r'}$ is $\mathrm{err}(c_{r'}) = \Pr_{x\sim\mathcal X}[c_{r'}(x) \ne c_r(x)]$ , and probabilities of the learner's success are over $x_1,\dots,x_n \sim \mathcal X$ i.i.d., $z_i = (x_i, c_r(x_i))$ , and the learner's coins.

Formalization targets

Goal: Theorem 4.4

There are constants $c, c', C > 0$ such that for all $d \ge 1$ , $0 < \varepsilon \le 1/2$ , $\alpha, \beta \in (0,1/2)$ : $\mathcal A^*(\cdot,\varepsilon,\alpha,\beta)$ is $\varepsilon$ -differentially private on databases of every size, and

n \ge C\,\frac{(d + \log_2(1/\beta))\log_2(1/\beta)}{\varepsilon\alpha} \implies \Pr\big[\mathcal A^* \text{ outputs } h^* \text{ with } \mathrm{err}(h^*) \le \alpha\big] \ge 1-\beta

for every distribution $\mathcal X$ and every target $c_r$ . When $\log_2(1/\beta) \le d$ the bound is the paper's $O(d\log(1/\beta)/(\varepsilon\alpha))$ . The constants are fixed before all other parameters. The goal is literally the conjunction of Lemma 4.5 and Lemma 4.6.

Milestones

\text{Thm 2.3 (Laplace mechanism)},\quad \text{Claim 2.2 (composition)},\quad \text{Thm A.1 (Chernoff)},\quad \text{Occam's razor for } |H| = 2^d,

\text{Lemma 4.1: } n \ge \tfrac{8}{\varepsilon\alpha}(d\ln 2 + \ln 4) \Rightarrow \Pr[\mathcal A(z,\varepsilon) = h,\ \mathrm{err}(h)\le\alpha] \ge \tfrac14,

|V_T| \le 2|V_{T\cup\{i\}}| \text{ if } V_{T\cup\{i\}} \ne \emptyset,\quad \text{Claim 4.3},\quad \text{Lemma 4.2 (}\mathcal A\text{ private)},\quad \text{Lemma 4.5 (}\mathcal A^*\text{ private)},\quad \text{Lemma 4.6 (}\mathcal A^*\text{ learns)}.

Significance

The theorem shows that the restriction to private algorithms does not separate efficient learnability from statistical-query learnability: parity is efficiently and privately PAC learnable, yet not SQ learnable. Its sample complexity exceeds the non-private $O((d + \ln(1/\beta))/\alpha)$ by a factor $O(\ln(1/\beta)/\varepsilon)$ (remark, p. 18). The private amplification step (private model selection with Laplace-perturbed test errors) is a general technique that converts any private learner with constant success probability into a private PAC learner.

The result is proved in the paper; none of it is machine-checked as far as we know. The mission produces a formal library of the basic privacy calculus (Laplace mechanism, composition and post-processing), the $\mathbb Z_2$ solution-space estimate behind the privacy of $\mathcal A$ , and the analysis of both learners. Formalizing it also repairs the paper's statement: the printed sample bound fails when $\log(1/\beta)$ is large compared with $d$ (see the scope section), and the base of the logarithm defining $k$ is misprinted.

Difficulty

The obvious private learner, "solve the linear system on all examples and output a random solution", is not private. One changed example can make the system inconsistent and turn every hypothesis output into failure, so the output law on neighboring databases differs by an unbounded factor. Two devices restore privacy: subsampling each example with probability $\varepsilon/4$ , and failing with probability $1/2$ unconditionally. The privacy proof then needs a quantitative fact about $\mathbb Z_2$ : adding one consistent equation at most halves the solution space. The proof must also handle databases labeled by no parity at all, where solution spaces are empty.

Utility has its own difficulty. The amplified learner selects among candidates through noisy test errors, so three failure events (no good candidate, unrepresentative test set, large Laplace noise) must be bounded together. The sizes $k$ , $n'$ , $s$ must also be shown to fit inside the claimed sample bound.

Formalization scope

Bits are ZMod 2; $\{0,1\}^d$ is Fin d → ZMod 2; $c_r(x)$ is dotProduct r x. Databases are Fin n → (Fin d → ZMod 2) × ZMod 2, with 0-based indices.
An algorithm is the law of its output. $\mathcal A$ 's output is Option (Fin d → ZMod 2) (none = $\bot$ ). $\mathcal A^*$ 's output is "insufficient samples", $\bot$ , or a hypothesis $c_r$ . Every set of outputs is measurable, and differential privacy is required for all measurable sets.
The distribution $\mathcal X$ is a PMF on the finite set $\{0,1\}^d$ . The probability over the examples is a finite sum weighted by $\prod_i \mathcal X(x_i)$ , and $\bot$ has error 1.
Corrections and explicit hypotheses. (1) $k = \lceil\log_{4/3}(1/\beta')\rceil$ : the printed base $3/4$ gives $k \le 0$ , and the proof needs $(3/4)^k \le \beta'$ . (2) Sizes are ceilings; $\log$ is base 2 and $\ln$ is natural, as on p. 8. (3) Privacy is stated for $0 < \varepsilon \le 1/2$ : the proof of Lemma 4.2 uses $\varepsilon \le 1/2$ , and its step $2p/(1-p) + 1 \le \varepsilon + 1$ fails beyond that. Utility statements need only $0 < \varepsilon \le 4$ , so that $p = \varepsilon/4$ is a probability. (4) The printed bound $O(d\log(1/\beta)/(\varepsilon\alpha))$ is false when $\log(1/\beta) \gg d$ , because $\mathcal A^*$ refuses unless $n > kn' + s$ and $s$ grows like $\log^2(1/\beta)/(\varepsilon\alpha)$ . Utility is therefore stated with the bound $C(d + \log_2(1/\beta))\log_2(1/\beta)/(\varepsilon\alpha)$ , the order of $kn' + s$ , which equals the printed order whenever $\log_2(1/\beta) \le d$ . The privacy conjunct does not depend on the sample bound. (5) A $\bot$ candidate does not take part in the argmin, and ties go to the least index. (6) Lemma 4.1 assumes $\alpha \le 1/2$ , which its proof uses. (7) Claim 4.3 is stated in product form (no division). (8) Theorem 2.3 takes any positive bound $\Delta$ on the global sensitivity.
"Efficiently" (polynomial running time) is not modelled.
Ruling out trivial readings. The constants $c, c', C$ are existentially quantified once, outside every other quantifier. A constant chosen after $d$ , $\varepsilon$ , $\alpha$ , $\beta$ would make the utility claim trivial. Success requires an actual hypothesis output, so "insufficient samples" and $\bot$ are failures. Privacy quantifies over all databases, not only consistently labeled ones.
Reused results: ComputationalLearning.chernoff_bounds (Theorem A.1) and ComputationalLearning.occam_cardinality (Occam's razor), both proved on the platform.
Contributions welcome: proofs of the privacy calculus (Theorem 2.3, Claim 2.2) for general use, the $\mathbb Z_2$ halving lemma, and the utility analysis. The first two are reusable well beyond this mission.

Selected references

S. P. Kasiviswanathan, H. K. Lee, K. Nissim, S. Raskhodnikova, A. Smith, What Can We Learn Privately?, SIAM J. Comput. 40(3) (2011) 793–826. arXiv:0803.0924v3, DOI 10.1137/090756090
C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating Noise to Sensitivity in Private Data Analysis, TCC 2006. DOI 10.1007/11681878_14
A. Blum, C. Dwork, F. McSherry, K. Nissim, Practical Privacy: The SuLQ Framework, PODS 2005. DOI 10.1145/1065167.1065184
M. Kearns, Efficient Noise-Tolerant Learning from Statistical Queries, J. ACM 45(6) (1998) 983–1006. DOI 10.1145/293347.293351
A. Blum, M. Furst, J. Jackson, M. Kearns, Y. Mansour, S. Rudich, Weakly Learning DNF and Characterizing Statistical Query Learning Using Fourier Analysis, STOC 1994. DOI 10.1145/195058.195147
M. Kearns, U. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994. DOI 10.7551/mitpress/3897.001.0001

14 thms4 active usersReviewed

Completed

Partial Differential Equations Theory of Computation·Captain: marwahaha

Incompressible Box Transport and Finite ComputationOpen Problem

Motivation

Volume-preserving box transport supplies geometric operations for a finite computation. The selected goal assembles these into a force and a fixed particle observer. The pinned manuscript supplies the research context.

Setting

A finite machine and input determine effective velocity and force coefficients. The force depends affinely on positive viscosity, and after time one the velocity is periodic and depends only on the machine.

Formalization target

The selected goal is OAI.BalancedTransport.balanced_three_stack_realization. Its central assertion is

\exists t\geq0:\ X(t,(4,0,0))\in(-1,2)^3\quad\Longleftrightarrow\quad M\text{ halts on }w.

The theorem states that there exist velocity fields U(M,w), force coefficients f₀(M,w) and f₁(M,w), material flows X(M,w), and a globally 1-periodic velocity field R(M) for each finite deterministic tape machine M, with the following properties for every finite input word w. On nonnegative time and ℝ³, U, f₀ and f₁ are smooth and vanish outside a common spatial compact set independent of time; every mixed space-time derivative of U is uniformly bounded. Moreover, f₀ = ∂ₜU + (U·∇)U and f₁ = −ΔU. All three families are uniformly effective from the encoded machine and input: algorithms approximate every mixed derivative component at rational space-time points within 2⁻ⁿ, provide global integer bounds on these derivatives, and provide integer support radii. The velocity is 1-periodic after time 1 and satisfies U(M,w)(t,x) = R(M)(t,x) for every t ≥ 1, so its later field depends only on M. The flow satisfies X(0,a) = a and ∂ₜX(t,a) = U(t,X(t,a)); its trajectory starting at (4,0,0) enters (−1,2)³ at some nonnegative time exactly when M halts on w, meaning that a configuration with no next transition is reached after finitely many machine steps. For every viscosity ν > 0, the force f = f₀ + νf₁ is smooth, has uniformly bounded mixed derivatives, and is 1-periodic after time 1; U with pressure zero solves the incompressible Navier–Stokes equation ∂ₜU + (U·∇)U = νΔU + f with U(0,·) = 0. This velocity is unique among smooth zero-data solutions in the comparison class, and every such solution has spatially constant pressure. The comparison class requires the velocity and all spatial derivatives through order two to be continuous in time as L² functions, the velocity to be continuously differentiable in time in L², velocity and first spatial derivatives to be bounded on each finite time slab, and pressure, after subtracting a time-dependent scalar, together with its first spatial derivatives to be continuous in time in L²; (U,0) belongs to this class. Finally, derivative approximations and global derivative bounds for f are computable when ν is computable, and computable relative to any rational name of ν whose nth approximation has error at most 2⁻ⁿ.

Significance and status

The balanced three-stack realization is the main goal; balanced box routing is a separate supporting reference. The exact conclusion permits spatially constant pressure in competing solutions and explicitly states its comparison class. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

Uniform effectiveness, compact support, periodic behavior and uniqueness must all coexist with exact halting detection.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

OAI.BoxTransport.Routing.balanced_box_routing (Open).

Selected references

OpenAI, Incompressible Box Transport and Finite Computation, preprint, 2026. Manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

93 thms4 active usersReviewed

Completed

Functional Analysis·Captain: marwahaha

Bi-Lipschitz Absorption of c0 Without a Linear Copy of c0Open Problem

Motivation

Metric absorption asks whether adjoining a null-sequence component changes a space up to controlled distances. Linear absorption imposes a different requirement. The pinned manuscript supplies the research context.

Setting

The space Z is a separable real Banach space. The product Z×c0 uses the product metric, and equivalent metrics are compared through positive bi-Lipschitz constants.

Formalization target

The selected goal is OAI.C0Absorption.main_result. Its central assertion is

Z\times c_0\simeq_{\rm biLip}Z,\qquad c_0\not\hookrightarrow_{\rm linear}Z.

The theorem states that there exists a real normed space Z, in a fixed universe, with the following properties, where C₀ denotes the real Banach space of sequences ℝ-valued on ℕ that tend to zero at infinity, and a map f between metric spaces is bi-Lipschitz if there are constants 0<c≤C with c·d(x,y) ≤ d(f x,f y) ≤ C·d(x,y) for all x,y. First, Z is complete and separable. Second, Z contains no linear copy of C₀: every continuous linear map T from C₀ to Z fails to satisfy ‖Tx‖ ≥ c‖x‖ for all x for any c>0. Third, there is a surjective bi-Lipschitz map F from the product metric space Z × C₀ onto Z. Fourth, there is a bi-Lipschitz map from C₀ into Z. Fifth, Z is metrically universal for separable metric spaces: every separable metric space M, in the base universe, admits a bi-Lipschitz map into Z. Sixth, Z × C₀ is not linearly homeomorphic to Z, that is, there is no continuous linear equivalence, with continuous inverse, between Z × C₀ and Z.

Significance and status

The target also includes a bi-Lipschitz embedding of c0, universality for base-universe separable metric spaces, and failure of linear homeomorphism between the product and Z. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The metric universality and absorption maps must not produce a bounded-below linear embedding of c0.

Formalization scope

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

OpenAI, Bi-Lipschitz Absorption of c0 Without a Linear Copy of c0, preprint, 2026. Manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

41 thms4 active usersReviewed

Completed

Probability Quantum Information·Captain: marwahaha

Threshold parallel repetition for finite-dimensional entangled gamesOpen Problem

Motivation

Parallel repetition is useful for amplifying errors in nonlocal games, but a joint entangled strategy can correlate outcomes across repetitions. Independence of the sampled questions does not imply independence of wins. The pinned manuscript supplies the research context.

Setting

A finite two-player game has a probability distribution on question pairs and a Boolean acceptance predicate. Its entangled value is a supremum over finite-dimensional states and local positive-operator measurements.

Formalization target

The selected goal is OAI.ThresholdParallelRepetition.threshold_parallel_repetition. Its central assertion is

P\{W_k\geq\lceil(v+\delta)k\rceil\}\leq\exp\!\left(-\kappa_0\frac{\delta^{13}k}{1+\log(|A||B|)}\right).

The theorem states that there is a universal constant κ₀>0 such that the following holds for every two-player nonlocal game G with question sets of sizes x+1 and y+1 and answer sets of sizes a+1 and b+1, given by a probability distribution on question pairs and a Boolean acceptance predicate on questions and answers, whose entangled value is strictly less than 1. Here the entangled value is the supremum of the winning probability over finite-dimensional entangled strategies, which consist of a unit state on a bipartite space, positive semidefinite measurement operators for Alice and Bob summing to the identity for each question, with answer probabilities given by the Born rule. For every δ with 0<δ<1−entangledValue(G) and every number of repetitions k≥1, consider k-fold parallel repetition, where k independent question pairs are drawn from G's distribution and the players answer all coordinates at once. The threshold probability of a repeated entangled strategy S is the probability that the number of coordinates won is at least ⌈(entangledValue(G)+δ)k⌉. The theorem asserts that this probability is at most exp(−κ₀ δ¹³ k /(1+ln((a+1)(b+1)))) for every repeated strategy S, and that the threshold value, defined as the supremum of the threshold probability over all repeated strategies, satisfies the same bound. The statement is admitted without proof in the source.

Significance and status

The selected published Lean exponent is δ^13, not the manuscript abstract's δ^5 or its distribution-dependent cubic rate. Both every-strategy and supremum conclusions are included. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The estimate must hold uniformly over finite dimensions and collective strategies. Taking the supremum cannot assume that an optimal strategy exists.

Formalization scope

The available published material supplies this goal and its necessary definitions. Additional manuscript lemmas are not represented as attached milestones.

Selected references

OpenAI, Threshold parallel repetition for finite-dimensional entangled games, preprint, 2026. Manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

34 thms4 active usersReviewed

Completed

Combinatorics Number Theory·Captain: marwahaha

Quasipolynomial Bounds for Arithmetic ProgressionsOpen Problem

Motivation

A divergent reciprocal sum is a sparse largeness condition on integers. The mission asks whether it still forces additive structure of every finite length. The source manuscript presents the surrounding research claim.

Setting

For A⊆ℕ, reciprocalTerm(A,n) is 1/n when n∈A and zero otherwise, using Lean’s total real inverse at n=0. A nonconstant arithmetic progression has terms a+i·d with positive integer d.

Formalization target

Prove

\sum_{n\in A}\frac1n\text{ is not summable}\quad\Longrightarrow\quad\forall k\in\mathbb N,\ \exists a\in\mathbb N,\ d\in\mathbb N_{>0},\quad a+id\in A\ (i<k).

The starting term a is a natural number and is not separately required positive; the step d is strictly positive.

The selected formal target is OAI.Erdos3.manuscriptReciprocalProgressionTheorem.

Significance and status

The selected endpoint is the reciprocal-sum progression theorem. The manuscript’s quantitative bounds for progression-free subsets motivate it but are not supplied as separate published targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Positive density arguments alone do not cover all sets with divergent reciprocal sums. The hypothesis permits sets whose density tends to zero.

Formalization scope

The formal hypothesis is ¬Summable of a real sequence and ranges over all natural-number sets. All natural lengths k are included, including the degenerate zero and one cases. The n=0 summand equals zero and does not affect divergence. No quantitative constants are asserted here.

Selected references

OpenAI, Quasipolynomial Bounds for Arithmetic Progressions, preprint, 2026. Pinned manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

27 thms4 active usersReviewed

Completed

Functional Analysis Graph Theory·Captain: wurtle

Distortion of countably branching diamonds from midpoint and tree energiesResearch Paper

Motivation

How well can a graph be drawn inside a Banach space without stretching some distances much more than others? The distortion of the best such drawing measures the mismatch between the graph's metric and the geometry of the space. Diamond graphs are a standard test family: each edge is repeatedly replaced by parallel two-edge paths, so the graph contains many "midpoints" between the same two endpoints at every scale. For binary diamonds, bounded distortion in a space is tied to the failure of super-reflexivity (Johnson–Schechtman 2009). For countably branching diamonds, where each edge is replaced by infinitely many paths, the relevant property is asymptotic midpoint uniform convexity (AMUC): an equivalent AMUC norm prevents uniform embeddings (Baudier et al. 2017).

This mission asks for an explicit, quantitative lower bound on the distortion of countably branching diamonds in two specific James-type tree spaces, deduced from a midpoint "lens" estimate for those spaces.

Timeline

1974. James introduces the square-sum norm over disjoint tree segments (doi:10.1090/S0002-9904-1974-13580-9).
2001. Girardi proves asymptotic uniform convexity of the coordinate predual and dual of the binary James tree space (doi:10.4064/sm147-2-2).
2004. Lee and Naor give quantitative lower bounds for binary diamonds in $L_p$ , $1<p\le2$ , by summing a convexity inequality over levels (doi:10.1007/s00039-004-0473-8).
2009. Johnson and Schechtman characterize super-reflexivity by non-embeddability of binary diamonds (doi:10.1142/S1793525309000114).
2016. Dilworth, Kutzarova, Randrianarivony, Revalski and Zhivkov introduce AMUC and characterize it via lenses (doi:10.1016/j.jmaa.2015.11.061).
2017. Baudier, Causey, Dilworth, Kutzarova, Randrianarivony, Schlumprecht and Zhang prove that an AMUC renorming with power-type modulus $t^p$ forces distortion $\gtrsim k^{1/p}$ for depth- $k$ countably branching diamonds, and prove a converse under unconditional asymptotic structure (arXiv:1612.01984).
2018, 2021. Swift and Perreau extend the converse to bundle graphs and dual settings under additional structure (arXiv:1710.00877, arXiv:2104.10494).
2025. Malthaner gives a coloring-based proof of the power-type lower bound (arXiv:2310.03257).

The source of this mission is an OpenAI preprint dated September 27, 2026; its lens input comes from the companion OpenAI preprint Midpoint lenses in segment spaces of the same date.

Setting

Diamonds. The normalized diamond $\mathcal D_0$ is one edge of length $1$ . $\mathcal D_{k+1}$ replaces every edge of $\mathcal D_k$ by countably many internally disjoint two-edge paths with the same endpoints, each new edge having half the length of its parent. Let $d_k$ be the shortest-path metric. A map $f:\mathcal D_k\to Y$ has distortion at most $D$ if for some scale $s>0$

s\,d_k(u,v)\le\|f(u)-f(v)\|\le D\,s\,d_k(u,v)\qquad(u,v\in\mathcal D_k).

Tree spaces. Let $\mathcal T=\coprod_{h\ge1}\mathbb N^{\le h}$ (one rooted tree of each finite height, prefix order inside each tree). A segment is the set of vertices between two comparable nodes. For a finitely supported array $a$ ,

\rho(a)=\sup\Bigl\{\Bigl(\sum_{j=1}^m\Bigl|\sum_{s\in S_j}a_s\Bigr|^2\Bigr)^{1/2}:\ S_1,\dots,S_m\ \text{pairwise disjoint segments}\Bigr\}.

$J$ is the completion and $X=J^*$ with the dual norm. On $T_\infty=\mathbb N^{<\omega}$ (root included) the same formula defines $J_\infty$ , and $B_\infty=\overline{\operatorname{span}}\{e_t^*\}\subset J_\infty^*$ is the closed span of the coordinate functionals.

Formalization targets

Goal: Theorem 1.1

For every $k\ge0$ and every distortion- $D$ embedding of $\mathcal D_k$ into $Y\in\{X,\ B_\infty\}$ ,

D^2\ \ge\ 1+\frac k4.

The Lean statement OAI.DiamondDistortion.headline_all_pairs is the conjunction of the two cases. It is open on the platform.

Significance

The bound shows that the countably branching diamonds do not embed with uniformly bounded distortion into either space, with an explicit square-root growth rate. Combined with the companion results that neither space admits an equivalent asymptotically uniformly convex norm, and that the forest dual $X$ is reflexive, it shows that the diamond obstruction can hold in reflexive spaces without AUC renormability, so the unconditional-structure hypotheses in the known converses are doing real work. The constant $1/4$ is obtained by retaining the full quadratic budget of the lens inequality. The paper also gives direct energy proofs (Theorem 5.1, Propositions 4.2–4.3) with weaker constants, and general transfer theorems (Section 7) from lens inequalities to distortion bounds.

The theorem is proved in the OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. A formalization would certify both the metric deduction and, through its input, the tree-space lens estimate.

Difficulty

The input lens inequality bounds only the tail of a displacement outside a finite head. Turning it into a loss of squared edge stretch at every replacement level requires selecting, among infinitely many middle vertices, two whose head projections nearly coincide, so that their half-difference is a tail vector that still lies in the lens. Doing this simultaneously along a descending chain of edges, with the head growing at each step, and summing the losses without wasting the quadratic budget is where the constant is decided. A binary diamond argument does not transfer, because finitely many midpoints give no near-coincident projections.

Formalization scope

Diamond.Vertex k and Diamond.Edge k are defined by recursion on the stage, each parent edge receiving new vertices indexed by $\mathbb N$ ; Diamond.graph k is the undirected replacement graph and Diamond.distance k u v is SimpleGraph.dist divided by $2^k$ . Since distortion is scale invariant, the normalization does not affect the statement.
ForestDual is the full continuous dual of the completion of the finite-height forest James space; InfinitePredual is the norm-closed span of coordinate functionals in the dual of the infinite-tree space, with the subspace norm.
Segments are nonempty finite intervals of an ancestral partial order; test families are finite and pairwise disjoint.
The conclusion is stated as $1+k/4\le D^2$ , with $s>0$ given and the two-sided bound holding for all pairs $u,v$ .

A complete development needs the James segment norm and its dual, coordinate projections onto finite ancestral sets, the companion lens estimate, and graph distances on the countably branching diamonds. This infrastructure is shared with the other missions of this family. Formal proofs of Theorem 7.2 (lens-to-distortion transfer) and Theorem 7.12 (AMUC prevents uniform embeddings) are welcome as reusable components.

Selected references

OpenAI, Distortion of countably branching diamonds from midpoint and tree energies, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Diamond-distortion-from-midpoint-and-tree-energies-September-27-2026/manuscript.pdf
OpenAI, Midpoint lenses in segment spaces, preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Midpoint-lenses-in-segment-spaces-September-27-2026/manuscript.pdf
F. Baudier, R. Causey, S. Dilworth, D. Kutzarova, N. L. Randrianarivony, T. Schlumprecht, S. Zhang, On the geometry of the countably branching diamond graphs, J. Funct. Anal., 2017. https://arxiv.org/abs/1612.01984
S. J. Dilworth, D. Kutzarova, N. L. Randrianarivony, J. P. Revalski, N. V. Zhivkov, Lenses and asymptotic midpoint uniform convexity, J. Math. Anal. Appl., 2016. https://doi.org/10.1016/j.jmaa.2015.11.061
J. R. Lee, A. Naor, Embedding the diamond graph in $L_p$ and dimension reduction in $L_1$ , Geom. Funct. Anal., 2004. https://doi.org/10.1007/s00039-004-0473-8
W. B. Johnson, G. Schechtman, Diamond graphs and super-reflexivity, J. Topol. Anal., 2009. https://doi.org/10.1142/S1793525309000114
R. Malthaner, On Matoušek-like embedding obstructions of countably branching graphs, J. Math. Anal. Appl., 2025. https://arxiv.org/abs/2310.03257
R. C. James, A separable somewhat reflexive Banach space with nonseparable dual, Bull. Amer. Math. Soc., 1974. https://doi.org/10.1090/S0002-9904-1974-13580-9
M. Girardi, The dual of the James tree space is asymptotically uniformly convex, Studia Math., 2001. https://doi.org/10.4064/sm147-2-2

26 thms4 active usersReviewed

Completed

Mathematical Physics Probability·Captain: wurtle

Critical bond and site percolation on the cubic latticeResearch Paper

Motivation

Bernoulli percolation is the simplest model of a random medium: each edge (or each vertex) of a lattice is independently kept open with probability $p$ , and one studies the connected components (clusters) of open edges or vertices. As $p$ increases, an infinite cluster appears at a critical parameter $p_c$ . Whether an infinite cluster already exists at $p_c$ decides whether the phase transition is continuous, and it is the basic question about critical behaviour. On the nearest-neighbour cubic lattice $\mathbb Z^3$ it has been a central open problem of probability and statistical physics since the 1980s; the dimensions where it was settled were $d=2$ and sufficiently high $d$ .

Timeline

1957. Broadbent and Hammersley introduce percolation as a model of transport through a random medium (doi:10.1017/S0305004100032680).
1960. Harris proves that there is no infinite cluster at $p=1/2$ for bond percolation on $\mathbb Z^2$ (doi:10.1017/S0305004100034241).
1980. Kesten identifies the square-lattice bond threshold as $1/2$ , which with Harris's theorem gives critical nonpercolation for planar bonds (doi:10.1007/BF01197577).
1981. Russo proves critical nonpercolation for site percolation on the square lattice (doi:10.1007/BF00535742).
1990. Hara and Slade establish mean-field critical behaviour, including $\theta(p_c)=0$ , in sufficiently high dimension via the lace expansion (doi:10.1007/BF02108785). Grimmett and Marstrand prove that slab thresholds converge to $p_c$ and develop dynamic renormalization (doi:10.1098/rspa.1990.0100).
1996. Benjamini and Schramm conjecture that $\theta(p_c)=0$ on every quasi-transitive graph with $p_c<1$ (doi:10.1214/ECP.v1-978).
2016. Duminil-Copin, Sidoravicius and Tassion prove critical nonpercolation for bond percolation on slabs $\mathbb Z^2\times\{0,\dots,k\}$ (doi:10.1002/cpa.21641); this does not by itself give the full $\mathbb Z^3$ result.
2017. Fitzner and van der Hofstad reach the nearest-neighbour bond range $d\ge 11$ (doi:10.1214/17-EJP56).
2020. Heydenreich and Matzke give a detailed site lace-expansion treatment in high dimension (doi:10.1007/s10955-020-02607-y).
2024. Kozma and Nitzan reduce $\theta(p_c)=0$ to a conjectured multiplicative gluing inequality (arXiv:2401.12397).
2026. Public, non-peer-reviewed announcements report AI-assisted proofs of critical nonpercolation, including a reported Lean formalization for bonds on $\mathbb Z^d$ , $d\ge2$ (Leder, August 2026).

The source of this mission is an OpenAI preprint dated September 24, 2026, giving a self-contained argument for both bond and site percolation on $\mathbb Z^3$ .

Setting

Vertices are $x\in\mathbb Z^3$ ; $x$ and $y$ are nearest neighbours if $y=x\pm e_i$ for a coordinate vector $e_i$ .

Bond model. Each edge $\{x,x+e_i\}$ is open independently with probability $p$ . Two vertices are connected if an open path joins them (a path of zero edges is allowed).
Site model. Each vertex is open independently with probability $p$ . Two vertices are connected if a nearest-neighbour path joins them with every vertex open, endpoints included; in particular the cluster of a closed vertex is empty.

Let $\mathbb P_p$ be the product law, $\theta(p)=\mathbb P_p(\text{the cluster of }0\text{ is infinite})$ , and

p_c=\inf\{p\in[0,1]:\theta(p)>0\},

defined separately for bonds ( $p_c^{\mathrm{bond}}$ ) and sites ( $p_c^{\mathrm{site}}$ ).

Formalization targets

Goal: Theorem 1.1

\mathbb P_{p_c^{\mathrm{bond}}}\bigl(\text{every bond cluster in }\mathbb Z^3\text{ is finite}\bigr)=1,\qquad \mathbb P_{p_c^{\mathrm{site}}}\bigl(\text{every site cluster in }\mathbb Z^3\text{ is finite}\bigr)=1.

The Lean statement OAI.CriticalZ3.critical_no_infinite is the conjunction of these two almost-sure statements. It is open on the platform.

Significance

Theorem 1.1 gives continuity of the percolation probability at the transition: $\theta(p)\to0$ as $p\downarrow p_c$ (the paper derives this on p. 1 from the theorem and finite-box approximation). It is the three-dimensional case of the Benjamini–Schramm criticality question and of the classical $\theta(p_c)=0$ problem, which had resisted both planar methods (which rely on duality unavailable in three dimensions) and the lace expansion (which needs high dimension). The site statement is not a formal consequence of the bond statement: site bits become hyperedges with an endpoint convention that must be preserved.

The result is proved in an OpenAI preprint, which has not been peer reviewed. A public announcement reports a Lean formalization of the bond case on $\mathbb Z^d$ ; no machine-checked proof of this exact statement exists on the platform, and the site case is not covered by that announcement's formalization. A formal proof here would certify both models in one development.

Difficulty

The natural route is renormalization: show that if an infinite cluster exists at $p_c$ , then good finite-box events have high probability, persist at some $q<p_c$ , and can be glued into an infinite cluster at $q$ . The gluing step is where the obvious argument fails. Positive correlation (Harris–FKG) controls the probability that two increasing events both occur, but here one needs the probability of reaching a relay set and then a target, conditioned on an explored region; without a comparison inequality of the form $\mathbb P(o\leftrightarrow A,\ o\leftrightarrow T)\ge \mathbb P(o\leftrightarrow A)\min_{a\in A}\mathbb P(a\leftrightarrow T)$ the losses compound. Slab results do not suffice: extinction at each slab threshold plus convergence of thresholds does not give extinction on $\mathbb Z^3$ .

Formalization scope

Vertex := Fin 3 → ℤ; bonds are pairs (x, i) representing the edge from x to step x i = x + e_i, so each edge appears once.
bondLaw p and siteLaw p are Measure.infinitePi of bernoulliMeasure true false, giving mass $p$ to "open"; parameter clamps $p$ into $[0,1]$ .
Connectivity is Relation.ReflTransGen of the open-adjacency relation; siteCluster ω x is empty unless ω x = true, matching the endpoint convention.
bondCritical and siteCritical are sInf of $\{p\in[0,1]:\mathbb P_p(\text{cluster of }0\text{ infinite})>0\}$ . The statement does not assume $p_c<1$ ; it is a known fact for $\mathbb Z^3$ , and a solver may need to prove it to rule out the empty-set convention.
The conclusion quantifies over all vertices: almost surely every cluster is finite.

A complete development needs product Bernoulli measures on countable index sets, monotone coupling, increasing events and Harris–FKG, the finite hyperedge comparison inequality, and a planar boundary-counting lemma. The percolation infrastructure is reusable for the quasi-transitive generalization in the same family. Contributions formalizing Proposition 2.1 (joint connection comparison), Corollary 2.3 (failure comparison), Lemma 4.1 (extension estimate) and Lemma 5.1 (neighbouring-box relay) are welcome.

Selected references

OpenAI, Critical bond and site percolation on the cubic lattice, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Critical-bond-and-site-percolation-on-the-cubic-lattice-September-24-2026/paper.pdf
I. Benjamini, O. Schramm, Percolation beyond $\mathbb Z^d$ , many questions and a few answers, Electron. Commun. Probab., 1996. https://doi.org/10.1214/ECP.v1-978
S. R. Broadbent, J. M. Hammersley, Percolation processes. I. Crystals and mazes, Proc. Cambridge Philos. Soc., 1957. https://doi.org/10.1017/S0305004100032680
T. E. Harris, A lower bound for the critical probability in a certain percolation process, Proc. Cambridge Philos. Soc., 1960. https://doi.org/10.1017/S0305004100034241
H. Kesten, The critical probability of bond percolation on the square lattice equals 1/2, Comm. Math. Phys., 1980. https://doi.org/10.1007/BF01197577
L. Russo, On the critical percolation probabilities, Z. Wahrsch. Verw. Gebiete, 1981. https://doi.org/10.1007/BF00535742
T. Hara, G. Slade, Mean-field critical behaviour for percolation in high dimensions, Comm. Math. Phys., 1990. https://doi.org/10.1007/BF02108785
G. R. Grimmett, J. M. Marstrand, The supercritical phase of percolation is well behaved, Proc. R. Soc. Lond. A, 1990. https://doi.org/10.1098/rspa.1990.0100
H. Duminil-Copin, V. Sidoravicius, V. Tassion, Absence of infinite cluster for critical Bernoulli percolation on slabs, Comm. Pure Appl. Math., 2016. https://doi.org/10.1002/cpa.21641
R. Fitzner, R. van der Hofstad, Mean-field behavior for nearest-neighbor percolation in d>10, Electron. J. Probab., 2017. https://doi.org/10.1214/17-EJP56
M. Heydenreich, K. Matzke, Critical site percolation in high dimension, J. Stat. Phys., 2020. https://doi.org/10.1007/s10955-020-02607-y
G. Kozma, S. Nitzan, A reduction of the θ(p_c)=0 problem to a conjectured inequality, preprint, 2024. https://arxiv.org/abs/2401.12397

48 thms4 active usersReviewed

Completed

Combinatorics Group Theory Representation Theory·Captain: wurtle

A Cyclic Polytabloid Proof of Saxl's ConjectureResearch Paper

Motivation: Saxl's conjecture on the staircase tensor square

The irreducible complex representations of the symmetric group $S_n$ are the Specht modules $S^\lambda$ , indexed by partitions $\lambda\vdash n$ . How a tensor product $S^\alpha\otimes S^\beta$ (with diagonal action) decomposes is recorded by the Kronecker coefficients

g(\alpha,\beta,\lambda)=\dim\operatorname{Hom}_{S_n}\!\big(S^\lambda,\,S^\alpha\otimes S^\beta\big),

for which no positive combinatorial rule is known; even deciding positivity is hard, and the question is studied in algebraic combinatorics and geometric complexity theory. In 2012 Jan Saxl proposed that the staircase $\rho_m=(m,m-1,\dots,1)$ , a partition of $N_m=m(m+1)/2$ , has a tensor square containing every irreducible representation of $S_{N_m}$ .

Timeline

2012 — Saxl proposes the conjecture at the UCLA Combinatorics Seminar (20 March 2012), as recorded by Pak, Panova and Vallejo.
2010 — Brown, van Willigenburg and Zabrocki show that $S^{(m,m-1)}\otimes S^{(m,m-1)}$ is the multiplicity-free sum of all irreducibles with at most four rows (BWZ 2010, Cor. 4.1).
2013 — Heide, Saxl, Tiep and Zalesski prove that the Steinberg square of most finite simple groups of Lie type contains every irreducible, a motivating precedent (HSTZ 2013, Thm 1.2).
2015 — Ikenmeyer proves positivity for all $\lambda$ comparable with $\rho_m$ in dominance order, and all hooks (Ikenmeyer 2015).
2016 — Pak, Panova and Vallejo formulate the conjecture in print, give a character-nonvanishing criterion, and handle hooks and two-row shapes for large $m$ (PPV 2016).
2017 — Luo and Sellke: almost every partition occurs (uniform and Plancherel measures) (Luo–Sellke 2017).
2018–2021 — Bessenrodt: double hooks (2018); Bessenrodt, Bowman and Sutton: all 2-height-zero constituents and framed staircases (2021); Li: triple hooks (2021).
2023 — Harman and Ryba: the staircase tensor cube contains everything (Harman–Ryba 2023).
2025 — Letellier and Nam prove the staircase-square statement for unipotent characters of $\mathrm{GL}_n(q)$ , a different character theory (Letellier–Nam 2025).
2026 — An OpenAI preprint, A Cyclic Polytabloid Proof of Saxl's Conjecture (OpenAI Math Release, September 24, 2026), claims a proof of the full conjecture. It has not been peer reviewed and the theorem is not formally verified.

Setting

A partition is a Mathlib YoungDiagram. The Lean development builds $S^\lambda$ concretely: for a tableau $t$ (a bijection between $\{0,\dots,n-1\}$ and the cells), the polytabloid $e_t$ is the signed sum over the column group of $t$ of the permuted indicator of the row word of $t$ , inside the space of functions on words $\mathrm{Fin}\,n\to\mathrm{Fin}\,d$ ; Specht t is the $\mathbb C$ -span of the $S_n$ -orbit of $e_t$ . The coefficient kronecker a b t is the complex dimension of the space of $S_n$ -intertwining maps from spechtRep t into spechtRep a ⊗ spechtRep b. The staircase staircase m is the diagram of cells $(i,j)$ with $i+j<m$ , i.e. $\rho_m$ .

Formalization targets

Goal: Saxl's conjecture

For every integer $m\ge1$ and every partition $\lambda\vdash N_m$ ,

g(\rho_m,\rho_m,\lambda)>0 ,

equivalently $S^{\rho_m}\otimes S^{\rho_m}$ contains every irreducible representation of $S_{N_m}$ . This is Theorem 1.1 of the source, formalized as SaxlConjecture (positivity of kronecker for every Young diagram $\mu$ with as many cells as staircase m). The goal is published on the platform with status Open.

Significance

The result itself. Saxl's conjecture is the best-known instance of the tensor-square covering problem for symmetric groups. The source proves a stronger cyclic form (its Theorem 3.1): every $S^\lambda$ already occurs in the submodule $W_m$ generated by one explicit tensor $v_{R_m}\otimes v_{C_m}$ of row and column polytabloids. A companion preprint uses this cyclic form to construct, for every $n\notin\{2,4,9\}$ , an irreducible representation of $S_n$ whose tensor square contains every irreducible (the tensor square conjecture of Pak–Panova–Vallejo).

Formalizing it. The Lean statement is the classical, non-cyclic conclusion, the form in which the conjecture is usually quoted. A formal proof would require Specht-module theory (irreducibility, Young's rule, branching, induced modules), none of which is presently in Mathlib in usable form; that layer would be reusable across representation theory of $S_n$ .

Difficulty

Positivity of a Kronecker coefficient cannot be read off from characters in general: character sums cancel, and the families handled earlier (hooks, two rows, double and triple hooks, dominance-comparable shapes, 2-height-zero shapes) each relied on a special structure. Asymptotic statements (almost all $\lambda$ ) or higher powers (cube, fourth power) leave exceptional constituents. An induction on $m$ must retain an explicit vector at every step, because knowing that a constituent appears somewhere in a smaller square does not propagate through the projections needed to grow the staircase.

Formalization scope

staircase m has cells $\{(i,j): i+j<m\}$ , with $m(m+1)/2$ cells; canonicalTableau fixes one enumeration of cells (any enumeration gives an isomorphic module). The target diagram ranges over all YoungDiagrams of the same cardinality.
kronecker is Module.finrank ℂ of Representation.IntertwiningMap, the genuine multiplicity; positivity means a nonzero equivariant map $S^\lambda\to S^{\rho_m}\otimes S^{\rho_m}$ exists.
The case $m\ge1$ matches the source; $m=0$ is excluded.
Needed infrastructure: Specht modules and polytabloid bases, Young's rule and dominance, sign twists, induction and restriction, Littlewood–Richardson branching. The definitions are shared verbatim with the companion universal-tensor-square mission.

Selected references

I. Pak, G. Panova and E. Vallejo, Kronecker products, characters, partitions, and the tensor square conjectures, Adv. Math. 288 (2016), 702–731. https://doi.org/10.1016/j.aim.2015.11.002
G. Heide, J. Saxl, P. H. Tiep and A. E. Zalesski, Conjugacy action, induced representations and the Steinberg square for simple groups of Lie type, Proc. London Math. Soc. 106 (2013), 908–930. https://doi.org/10.1112/plms/pds062
A. A. H. Brown, S. van Willigenburg and M. Zabrocki, Expressions for Catalan Kronecker products, Pacific J. Math. 248 (2010), 31–48. https://doi.org/10.2140/pjm.2010.248.31
C. Ikenmeyer, The Saxl conjecture and the dominance order, Discrete Math. 338 (2015), 1970–1975. https://doi.org/10.1016/j.disc.2015.04.027
S. Luo and M. Sellke, The Saxl conjecture for fourth powers via the semigroup property, J. Algebraic Combin. 45 (2017), 33–80. https://arxiv.org/abs/1511.02387v2
C. Bessenrodt, Critical classes, Kronecker products of spin characters, and the Saxl conjecture, Algebr. Comb. 1 (2018), 353–369. https://doi.org/10.5802/alco.18
C. Bessenrodt, C. Bowman and L. Sutton, Kronecker positivity and 2-modular representation theory, Trans. Amer. Math. Soc. Ser. B 8 (2021), 1024–1055. https://doi.org/10.1090/btran/70
X. Li, Saxl Conjecture for triple hooks, Discrete Math. 344 (2021), 112340. https://doi.org/10.1016/j.disc.2021.112340
N. Harman and C. Ryba, A tensor-cube version of the Saxl conjecture, Algebr. Comb. 6 (2023), 507–511. https://doi.org/10.5802/alco.267
E. Letellier and G. Nam, The Saxl conjecture and the tensor square of unipotent characters of GL_n(q), Algebr. Comb. 8 (2025), 1119–1140. https://doi.org/10.5802/alco.434
OpenAI, A Cyclic Polytabloid Proof of Saxl's Conjecture, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Cyclic-Polytabloid-Proof-of-Saxls-Conjecture-September-24-2026/paper.pdf

45 thms4 active usersReviewed

Completed

Analysis Dynamical Systems Probability·Captain: wurtle

The entropy-rate dimension formula for self-similar measures on the lineResearch Paper

Motivation

A self-similar measure on the line is the natural probability measure on the attractor of finitely many contracting similarities $\varphi_i(x)=r_ix+t_i$ , chosen with probabilities $p_i$ . Self-similar measures are the basic test case for fractal dimension theory; Bernoulli convolutions, the laws of $\sum_j\pm\lambda^j$ , are the classical example. When the pieces $\varphi_i(K)$ are well separated, the dimension is given by the entropy-to-Lyapunov formula $H(p)/\chi$ . When they overlap, dimension can drop, and the question is exactly how much. If two compositions of the same length coincide as maps (an exact overlap), information is genuinely lost; the entropy-rate dimension conjecture, formulated in Varjú's survey, predicts that this is the only mechanism: the dimension equals $\min\{1,h_{RW}/\chi\}$ , where $h_{RW}$ is the entropy rate of the random walk on composed maps.

This mission asks for a formal proof of that formula, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

1946–1981 — Moran (Proc. Camb. Phil. Soc. 1946) and Hutchinson (Indiana 1981) give the similarity-dimension formula under separation and the invariant-measure construction.
1939–1996 — Erdős proves singularity of Bernoulli convolutions at reciprocal Pisot parameters (AJM 1939); Garsia introduces the entropy rate (Pacific J. Math. 1963); Solomyak proves a.e. absolute continuity (Annals 1995).
2009 — Feng and Hu prove exact dimensionality of self-similar measures without separation (CPAM 2009).
2014 — Hochman shows a dimension drop forces superexponential concentration of cylinders (Annals 2014).
2019 — Breuillard–Varjú (Ann. Probab. 2019) and Varjú's full dimension for transcendental parameters (Annals 2019).
2021 — Baker and Bárány–Käenmäki construct systems without exact overlaps whose cylinders approach superexponentially (Adv. Math. 2021, Adv. Math. 2021).
2022–2025 — Rapaport proves the no-exact-overlap formula for algebraic ratios (Ann. Sci. ENS 2022); Rapaport–Varjú treat homogeneous three-map systems (Duke 2024); Feng–Feng treat algebraic translations (J. LMS 2025).
2026 — Varjú's survey states the entropy-rate conjecture (Conjecture 3, arXiv:2509.22042).
September 2026 — The OpenAI preprint claims the conjecture in full (Theorem 1.1, p. 2).

Setting

Let $\Lambda$ be a finite nonempty alphabet and $\varphi_i(x)=r_ix+t_i$ with $0<|r_i|<1$ , $t_i\in\mathbb R$ ; different symbols may give the same map, and ratios may be negative and unequal. Let $p=(p_i)$ be a probability vector with all $p_i>0$ . The self-similar measure $\mu$ is the Borel probability measure with

\mu=\sum_{i\in\Lambda}p_i\,(\varphi_i)_*\mu .

For a word $w=i_1\cdots i_n$ let $\varphi_w=\varphi_{i_1}\circ\cdots\circ\varphi_{i_n}$ , and let $G_n$ be the random affine map $\varphi_w$ when the letters are independent with law $p$ . With logarithms in base $2$ ,

h_{RW}=\inf_{n\ge1}\frac{H(G_n)}{n},\qquad \chi=-\sum_ip_i\log|r_i|>0,

where $H$ is Shannon entropy of the distribution of the map $G_n$ (coinciding words are merged). The lower Hausdorff dimension of $\mu$ is $\dim_H\mu=\inf\{\dim_HE: E\ \text{Borel},\ \mu(E)>0\}$ . The system has no exact overlaps if distinct words of the same length give distinct maps.

Formalization targets

Milestone: Corollary 6.3 (p. 20) — dimension of the attractor

If there are no exact overlaps, the attractor $K=\{\lim_n\varphi_{\omega_1}\circ\cdots\circ\varphi_{\omega_n}(0)\}$ is compact and nonempty, the equation $\sum_i|r_i|^s=1$ has a unique solution $s_*\ge0$ , and $\dim_HK=\min\{1,s_*\}$ .

Milestone: Corollary 6.4 (p. 20) — homogeneous systems

If $r_i=\lambda\in(0,1)$ for all $i$ and there are no exact overlaps, then $\dim_H\mu=\min\{1,H(p)/\log(1/\lambda)\}$ .

Goal: Theorem 1.1 (p. 2)

For every such family and every strictly positive probability vector $p$ ,

\dim_H\mu=\min\Bigl\{1,\ \frac{h_{RW}}{\chi}\Bigr\}.

No separation assumption is made; exact overlaps and repeated generators are allowed.

Significance

The result itself. It removes every arithmetic and separation hypothesis from the dimension theory of self-similar measures on the line: the only way dimension can drop below $\min\{1,H(p)/\chi\}$ is through exact overlaps, and then the drop is exactly measured by the map entropy. Without exact overlaps it gives the classical formula (Corollary 6.2, p. 19), and hence the dimension of every self-similar set without exact overlaps (Corollary 6.3), which is the exact-overlaps conjecture for sets. It asserts nothing about absolute continuity.

Formalizing it. Hausdorff dimension and self-similar measures exist only partially in Mathlib, and the proof needs a quantitative entropy calculus for finite laws at multiple scales. A formal proof would certify the general theorem together with the consequences that previously required separate arithmetic hypotheses. The only external input is the Feng–Hu exact-dimensionality theorem.

Difficulty

Hochman's method yields the formula under exponential separation of cylinders, but Baker and Bárány–Käenmäki showed that without exact overlaps cylinders can still come superexponentially close, so no lower bound on the separation is available, and exact overlaps add further collisions. The proof must therefore detect entropy hidden at arbitrarily fine scales with no control on the smallest positive distance. The preprint does this with a finite-law pair estimate independent of minimal separation (Lemma 3.2, p. 9), conditioning on block types to recover the map-entropy rate when addresses collide (Lemma 4.1, p. 13), and disjoint windows of entropy gain whose depths are chosen adaptively (Section 5).

Formalization scope

A System ι over a nonempty Fintype ι carries ratio, offset, weight with $0<|r_i|<1$ , $p_i>0$ , $\sum p_i=1$ . SelfSimilar S μ is the equation $\mu=\sum_i p_i\,(\varphi_i)_*\mu$ for a probability measure $\mu$ on $\mathbb R$ .
wordAffine composes maps as $\varphi_{i}\circ\varphi_w$ and records (slope, translation); mapMass merges words with equal complete maps; walkEntropy n is base-2 Shannon entropy of $G_n$ ; entropyRate is the sInf over $n\ge1$ of $H(G_n)/n$ ; lyapunov is base-2.
lowerHausdorffDimension μ is an iInf in ℝ≥0∞ of dimH E over measurable $E$ with $\mu(E)>0$ ; the goal compares it to ENNReal.ofReal (min 1 (h/χ)).
NoExactOverlaps is injectivity of wordAffine on all words; words of different lengths always differ in slope modulus, so this matches the same-length condition of the source. The homogeneous milestone allows a single map, a degenerate case where both sides are $0$ .
The attractor milestone uses its own coding map codingPoint and word functions, equivalent to the definitions above.

Selected references

OpenAI, The entropy-rate dimension formula for self-similar measures on the line, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-entropy-rate-dimension-formula-for-self-similar-measures-on-the-line-September-24-2026/main.pdf
P. P. Varjú, Entropy rates in the dimension theory of self-similar measures, arXiv:2509.22042 (2026). https://arxiv.org/abs/2509.22042v2
J. E. Hutchinson, Fractals and self-similarity, Indiana Univ. Math. J. 30 (1981). https://doi.org/10.1512/iumj.1981.30.30055
D.-J. Feng, H. Hu, Dimension theory of iterated function systems, Comm. Pure Appl. Math. (2009). https://doi.org/10.1002/cpa.20276
M. Hochman, On self-similar sets with overlaps and inverse theorems for entropy, Ann. of Math. 180 (2014). https://doi.org/10.4007/annals.2014.180.2.7
P. P. Varjú, On the dimension of Bernoulli convolutions for all transcendental parameters, Ann. of Math. 189 (2019). https://doi.org/10.4007/annals.2019.189.3.9
E. Breuillard, P. P. Varjú, On the dimension of Bernoulli convolutions, Ann. Probab. (2019). https://doi.org/10.1214/18-AOP1324
A. Rapaport, Proof of the exact overlaps conjecture for systems with algebraic contractions, Ann. Sci. ENS (2022). https://doi.org/10.24033/asens.2518
A. Rapaport, P. P. Varjú, Self-similar measures associated to a homogeneous system of three maps, Duke Math. J. (2024). https://doi.org/10.1215/00127094-2023-0019
S. Baker, Iterated function systems with super-exponentially close cylinders, Adv. Math. (2021). https://doi.org/10.1016/j.aim.2020.107548
B. Bárány, A. Käenmäki, Super-exponential condensation without exact overlaps, Adv. Math. (2021). https://doi.org/10.1016/j.aim.2020.107549
B. Solomyak, On the random series Σ±λ^n (an Erdős problem), Ann. of Math. (1995). https://doi.org/10.2307/2118556

60 thms4 active usersReviewed

Completed

Analysis Probability Theoretical Computer Science·Captain: wurtle

Projection moments, positive cap domination, and Riesz estimates on the sphereResearch Paper

Motivation

A linear projection can concentrate a measure even when the measure has no atoms; how much depends on how much mass sits near the affine subspaces that the projection collapses. Quantitative versions of this principle go back to the potential-theoretic projection method of Kaufman and Mattila, which relates ball-growth bounds $\nu(B(x,r)) \le K r^\beta$ to the behaviour of projections. This preprint proves explicit, dimension-dependent versions for random exact projections and applies them to a learning question: how many noiseless Gaussian measurements $\langle x_t, s\rangle$ does a learner with $M$ bits of memory need to recover a unit vector $s$ to angular accuracy $\epsilon$ ?

The answer proved here is that $M = o(d^2)$ bits force $T \ge c\,d\log(1/\epsilon)$ measurements, matching the real-valued randomized Kaczmarz scale, and more generally $T \ge c\,d\log(1/\epsilon)/(1 + M/d^2)$ for every $M$ .

Timeline

1975. Mattila relates Hausdorff dimension, orthogonal projections and ball-growth measures through inverse-distance energy averaging.
1984. Drury's affine-plane change of variables for $k$ -plane transforms contains the simplex-volume Jacobian used in projection calculations.
2014–2016. Shamir's finite-message framework includes bounded-memory online learning; Steinhardt and Duchi (2015) prove memory-dependent minimax rates for sparse regression; Steinhardt, Valiant and Wager (2016) relate memory, communication and statistical queries; Raz (2016) proves the quadratic-memory versus exponential-sample separation for parity learning.
2019. Sharan, Sidford and Valiant prove an $\Omega(d\log r)$ sample bound for Gaussian regression with small uniform noise, $d^2/4$ bits and Euclidean accuracy $d^{-r}$ , using high-moment expansions and successive orthogonalization. Dagan, Kur and Shamir prove quadratic-space bounds for two other linear-prediction tasks.
2026. The OpenAI preprint Projection moments, positive cap domination, and Riesz estimates on the sphere (dated September 27, 2026) gives three independent proofs of the $\Omega(d\log(1/\epsilon))$ bound for exact observations and $o(d^2)$ memory. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

Let $\sigma$ be uniform probability on $S^{d-1} \subset \mathbb{R}^d$ . A finite measure $\nu$ on $\mathbb{R}^d$ satisfies an all-ball mass bound with constants $K, \beta$ if $\nu(B(x,r)) \le K r^\beta$ for every ball. For an orthonormal $k$ -frame $P$ , $P_\#\nu$ is the image measure on $\mathbb{R}^k$ and $g(P,\cdot)$ its density. The Riesz functional of $h : S^{d-1} \to [0,1]$ is $V(h) = \sup_{z} \int h(s)\|s-z\|^{-d/2}\,d\sigma(s)$ .

In the finite-state regression experiment, the signal $S \sim \sigma$ ; at each step a row $x_t \sim N(0, I_d)$ arrives with its exact label $\langle x_t, S\rangle$ . A learner keeps one of $2^M$ states, may use arbitrary measurable randomized transitions of the current state and pair, stops by a deterministic horizon $T$ , and outputs a unit vector from its terminal state, stopping index and fresh randomness. Success means $\arccos\langle \hat S, S\rangle \le \epsilon$ .

In Lean (OAI.ProjectionMoments, OAI.NoiselessRegression), learners are FiniteKernelLearner d M T (Markov-kernel transitions on completed observations, states Fin (2^M)), mixed over a seed space Ξ with probability ρ; seededSuccess is uniform-prior success; AllBallMass ν K β, coordinateDensity, frameLaw, capMeasure, rieszPotential encode the geometric objects.

Formalization targets

Goal: `OAI.ProjectionMoments.main`

A conjunction of the paper's results, including:

Theorem 2.4 (finite-memory precision bound). There is an absolute $c > 0$ such that for every $M(d) = o(d^2)$ , eventually in $d$ , uniform-sphere success at least $2/3$ at accuracy $0 < \epsilon \le 1/10$ forces

T \ge c\, d \log(1/\epsilon),

also under an every-signal guarantee.

Corollary 2.5, in the weakened form that $M \le A d^2$ gives $T \ge c_A d\log(1/\epsilon)$ (the paper proves $T \ge c\,d\log(1/\epsilon)/(1+M/d^2)$ ).
Theorem 3.3 (integrated orthonormal-projection moment). If $\nu$ is finite, supported in $B(z,R)$ , with $\nu(B(x,r)) \le K r^\beta$ , and $k+q \le d$ , $0 < \beta \le d$ , $\beta - k - (q-2) \ge 1$ , then

\Big(\iint g(P,u)^q\,du\,d\vartheta_{d,k}(P)\Big)^{1/q} \le C^d (C\sqrt d)^{k(1-1/q)} K R^{\beta - k(1-1/q)}.

Theorem 3.5, Corollary 3.4 and Proposition 3.7 (normalized and all-radii moments, one-block propagation), Proposition 4.1 (positive domination by countable sums of cap measures), Lemma 5.3 (projection density at deterministic offsets), and the explicit success bounds of Propositions 3.8, 4.4 and 5.4 for arbitrary $M$ .
A bridge showing the kernel learner model agrees with the seeded deterministic learner model.

Significance

The result. The projection moment estimates are general statements about finite measures with ball-growth control and apply beyond learning. In the learning application they give three proofs, with different stopping and accuracy costs, that $o(d^2)$ bits cannot beat the $d\log(1/\epsilon)$ sample scale for exact Gaussian measurements, plus an explicit trade-off for all $M$ .

Formalizing it. The results are in an unrefereed preprint; there is no machine-checked proof. The conjunct FixedQuadraticMemory coincides with part of the goal of the companion mission on Memory and precision in noiseless Gaussian regression, so progress here is shared.

Difficulty

Integrated density norms do not determine density values on a matrix-dependent graph, so pointwise statements need an explicitly chosen density version. The high moments of projected densities require controlling collisions of $q$ independent points under projection, which leads to inverse affine heights whose integrability must be extracted from the ball-growth hypothesis at all scales. In the learning application, conditioning on an exact label produces a singular posterior, so arguments that track a posterior density fail.

Formalization scope

Space is EuclideanSpace ℝ (Fin d); frames are orthonormal families Fin k → E drawn by frameLaw; densities are ℝ≥0∞-valued with explicit measurable versions.
Parameters are natural-number floors (d/4, d/8, d/16); block counts appear as (T+k-1)/k.
Learners: FiniteKernelLearner with CompletedRules almost surely in the seed; success probabilities are ℝ≥0∞.

The goal has no trivial reading: each conjunct quantifies over all measures or learners satisfying the stated hypotheses, and the hypotheses are satisfiable.

Needed infrastructure: Stiefel and Haar measures, Gaussian polar decomposition of matrices, Gram–Schmidt Jacobians, spherical caps, Riesz potentials. Contributions proving individual conjuncts (for example Theorem 3.3) are welcome.

Selected references

OpenAI, Projection moments, positive cap domination, and Riesz estimates on the sphere, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Projection-moments-positive-cap-domination-and-Riesz-estimates-on-the-sphere-September-27-2026/paper.pdf
P. Mattila, Hausdorff Dimension, Orthogonal Projections and Intersections with Planes, Ann. Acad. Sci. Fenn. Ser. A I Math. 1 (1975). https://doi.org/10.5186/aasfm.1975.0110
S. W. Drury, Generalizations of Riesz Potentials and $L^p$ Estimates for Certain $k$ -Plane Transforms, Illinois J. Math. 28 (1984).
V. Sharan, A. Sidford, G. Valiant, Memory-Sample Tradeoffs for Linear Regression with Small Error, STOC 2019. https://doi.org/10.1145/3313276.3316403
R. Raz, Fast Learning Requires Good Memory, 2016. https://arxiv.org/abs/1602.05161
J. Steinhardt, G. Valiant, S. Wager, Memory, Communication, and Statistical Queries, COLT 2016. https://proceedings.mlr.press/v49/steinhardt16.html
J. Steinhardt, J. Duchi, Minimax Rates for Memory-Bounded Sparse Linear Regression, COLT 2015. https://proceedings.mlr.press/v40/Steinhardt15.html
O. Shamir, Fundamental Limits of Online and Distributed Algorithms for Statistical Learning and Estimation, NeurIPS 2014.
Y. Dagan, G. Kur, O. Shamir, Space Lower Bounds for Linear Prediction in the Streaming Model, COLT 2019. https://proceedings.mlr.press/v99/dagan19b.html

52 thms4 active usersReviewed

Completed

Information Theory Probability·Captain: wurtle

Sharp binary-information contraction on the discrete cubeResearch Paper

Motivation

Draw $n$ independent fair bits $X$ , compute a one-bit summary $f(X)$ , and send the bits through independent binary symmetric channels with crossover probability $\varepsilon$ , producing $Y$ . Which summary tells the receiver the most about $Y$ ? Kumar and Courtade conjectured that a single coordinate, $f(X)=X_1$ , is optimal: $I(f(X);Y)\le 1-h_2(\varepsilon)$ bits for every Boolean $f$ , in every dimension and at every noise level (ISIT 2013; IEEE Trans. Inf. Theory 2014). The Courtade–Kumar (most informative Boolean function) conjecture is a basic question about how noise destroys information on the discrete cube, connecting information theory with Boolean Fourier analysis and hypercontractivity.

This mission asks for a formal proof of a sharp contraction theorem for arbitrary randomized binary summaries, whose Boolean case is the Courtade–Kumar conjecture, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

1970–1976 — Hypercontractivity on the cube (Bonami, Ann. Inst. Fourier 1970; Gross, Amer. J. Math. 1975; Beckner, Annals 1975); Mrs. Gerber's lemma (Wyner–Ziv, IEEE TIT 1973).
2013–2014 — Kumar and Courtade pose the conjecture and prove a coordinatewise sum bound.
2016 — High-noise results: Ordentlich, Shayevitz and Weinstein for balanced functions (ISIT 2016); Samorodnitsky for all Boolean functions in a dimension-independent high-noise range (IEEE TIT 2016).
2018 — Pichler, Piantanida and Matz prove coordinate optimality when the observation is also reduced to one bit (Ann. Appl. Probab. 2018).
2020–2023 — Barnes–Özgür's symmetrized reformulation (ISIT 2020); Li–Médard on fixed-mean optimizers (IEEE TIT 2021); Yu's $\Phi$ -stability (PTRF 2023).
2025–2026 — Chen, Gohari and Nair's differential (entropy-production) approach; independent preprints announcing proofs by Chen, Gohari, Javanmard, Lin, Mirrokni, Nair and Woodruff (arXiv:2609.24931), Ky and Tran (arXiv:2609.24184), Mahdavifar and Beirami (arXiv:2609.26444), and a bias-retaining finite-noise bound by Kramer and Saglam.
September 2026 — The OpenAI preprint (Theorems 1.1 and 1.3, Corollary 1.2, pp. 1–4).

Setting

Let $\Omega_n=\{-1,1\}^n$ with uniform measure; information is in nats unless stated. For $r\in[-1,1]$ put

L=\log2,\quad H(r)=-\tfrac{1+r}2\log\tfrac{1+r}2-\tfrac{1-r}2\log\tfrac{1-r}2,\quad \psi(r)=L-H(r),

with $0\log0=0$ ; $\psi^{-1}$ is the increasing branch $[0,L]\to[0,1]$ . A soft channel is $u:\Omega_n\to[-1,1]$ , the conditional mean of an auxiliary sign $U$ given $X$ ; its information is $I(u)=H(\mathbb Eu)-\mathbb EH(u)=I(U;X)$ . For $\rho\in[-1,1]$ let $Y_i=X_iZ_i$ with independent signs $\mathbb EZ_i=\rho$ , and let $T_\rho u(y)=\mathbb E[u(X)\mid Y=y]$ , so $I(T_\rho u)=I(U;Y)$ . For an interior field $g:\Omega_n\to(-1,1)$ with $m=\mathbb Eg$ , the production is $D(g)=\mathbb E[\operatorname{atanh}(g)\,Ng]$ with $Ng=\frac12\sum_i(g-g\circ\mathrm{flip}_i)$ ; the rate $F$ is defined by $F(\psi(r))=r\operatorname{atanh}r$ ; $S(I)=F(I)-2I$ (zero for $I<0$ ); $B_m(I)=2I+(1-m^2)S\bigl(L-\frac{H(m)-I}{1-m^2}\bigr)$ .

Formalization targets

Milestone: Courtade–Kumar inequality in bits (Corollary 1.2, p. 2)

For $n\ge1$ , $0\le\varepsilon\le\frac12$ and every Boolean $f$ on $\{0,1\}^n$ ,

I_2(f(X);Y)\le 1-h_2(\varepsilon),

with equality for every coordinate $x\mapsto x_i$ and its complement.

Goal: the soft contraction package (Theorem 1.1, p. 1; Corollary 1.2, p. 2; Theorem 1.3, p. 4)

The goal OAI.SoftChannel204.fullMain is the conjunction of:

Theorem 1.1. For all $n$ , $u:\Omega_n\to[-1,1]$ , $\rho\in[-1,1]$ :

I(T_\rho u)\le\psi\bigl(|\rho|\,\psi^{-1}(I(u))\bigr),

with equality for every soft coordinate $u(x)=a x_i$ , $|a|\le1$ ; and $I(U;Y)=I(T_\rho u)$ for the joint law of $(U,Y)$ . 2. Corollary 1.2. For Boolean $f$ with $m=\mathbb Ef$ and $r_m=\psi^{-1}(H(m))$ : $I(f(X);Y)\le\psi(|\rho|r_m)\le\psi(|\rho|)$ , strictly below $\psi(|\rho|)$ when $0<|m|<1$ and $0<|\rho|$ ; coordinates and their negations attain $\psi(|\rho|)$ ; and the bits conversion $\psi(1-2\varepsilon)/L=1-h_2(\varepsilon)$ . 3. Theorem 1.3. For every interior $g$ : $D(g)\ge\max\{B_m(I(g)),F(I(g))\}\ge F(I(g))$ .

Significance

The result itself. It settles the Courtade–Kumar conjecture and strengthens it in two directions: to randomized summaries at fixed initial information, and to a bias-dependent bound that is strictly better for nonconstant biased outputs. Theorem 1.3 is a mean-dependent entropy-production inequality, stronger than the scalar rate needed for Theorem 1.1. Several independent proofs of the Boolean conjecture were announced in the same period; the preprint compares its production profile with that of Chen et al. in Section 8.

Formalizing it. All objects are finite sums over $\{-1,1\}^n$ , so the statements are elementary to state in Lean. The proof requires an explicit three-point optimizer for a joining problem, convexity facts about $F$ and $S$ (Lemmas 2.2–2.4, pp. 5–6), dimension induction and integration along the noise semigroup. A formal proof would give a checked solution of a conjecture with several competing announced proofs, some computer-assisted.

Difficulty

The local-to-global method of Chen, Gohari and Nair needs a local inequality to pass from the two halves of the cube to the whole. The natural information-only profile $\Phi_m(I)=F(I)$ fails the corresponding local comparison for some coupled pair laws, so the induction must carry the mean $m$ as well. The preprint uses the maximum of two profiles, $B_m$ and $F$ ; it must solve the minimization of the joining cost exactly (Section 3), pay the interior pair with a variance-refined one-bit inequality (Lemma 4.1, p. 12), and control the common-output corners by a thinning argument (Theorem 6.1, p. 17). The linear bound $D(g)\ge2I(g)$ from the log-Sobolev inequality does not suffice; the nonlinear surplus above $2I$ is where the difficulty lies.

Formalization scope

Cube n = Fin n → Bool, averages are finite sums divided by $2^n$ , logs are natural; sign maps Bool to $\pm1$ .
psiInv is Function.invFunOn psi (Icc 0 1); since $\psi$ is strictly increasing on $[0,1]$ and $I(u)\in[0,L]$ , this is the paper's branch.
noise ρ u y = ∑ x, kernel ρ y x * u x with kernel the product of $(1\pm\rho)/2$ , which is $T_\rho$ . Mutual information is the finite sum over the joint table, with terms omitted where the joint probability is $0$ .
F is stated as psiInv s * artanh (psiInv s) and is only used on $[0,L)$ ; for interior $g$ , $|m|<1$ and $0\le I(g)<H(m)\le L$ , so reserve and hybrid are evaluated in their source domain.
All results hold for every $n\ge0$ ; the attainment statements quantify over i : Fin n. The milestone (separate definition file) uses the crossover form with bits.

Selected references

OpenAI, Sharp binary-information contraction on the discrete cube, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Sharp-binary-information-contraction-on-the-discrete-cube-September-24-2026/main.pdf
T. A. Courtade, G. R. Kumar, Which Boolean functions maximize mutual information on noisy inputs?, IEEE Trans. Inf. Theory 60 (2014). https://doi.org/10.1109/TIT.2014.2326877
G. R. Kumar, T. A. Courtade, Which Boolean functions are most informative?, ISIT 2013. https://doi.org/10.1109/ISIT.2013.6620221
A. Samorodnitsky, On the entropy of a noisy function, IEEE Trans. Inf. Theory (2016). https://doi.org/10.1109/TIT.2016.2584625
O. Ordentlich, O. Shayevitz, O. Weinstein, An improved upper bound for the most informative Boolean function conjecture, ISIT 2016. https://doi.org/10.1109/ISIT.2016.7541349
G. Pichler, P. Piantanida, G. Matz, Dictator functions maximize mutual information, Ann. Appl. Probab. (2018). https://doi.org/10.1214/18-AAP1384
L. Yu, On the $\Phi$ -stability and related conjectures, Probab. Theory Relat. Fields (2023). https://doi.org/10.1007/s00440-023-01209-5
A. Gohari, C. Nair, Outer bounds for multiuser settings: the auxiliary receiver approach, IEEE Trans. Inf. Theory (2022). https://doi.org/10.1109/TIT.2021.3128136
Z. Chen, A. Gohari, A. Javanmard, et al., A proof of the most informative Boolean function conjecture, arXiv:2609.24931 (2026). https://arxiv.org/abs/2609.24931
V. K. Ky, T. Tran, Dictators are most informative, arXiv:2609.24184 (2026). https://arxiv.org/abs/2609.24184
H. Mahdavifar, A. Beirami, The most informative bit and beyond, arXiv:2609.26444 (2026). https://arxiv.org/abs/2609.26444
S. G. Bobkov, P. Tetali, Modified logarithmic Sobolev inequalities in discrete settings, J. Theoret. Probab. (2006). https://doi.org/10.1007/s10959-006-0016-3

111 thms4 active usersReviewed

Completed

Combinatorics Discrete Geometry Theoretical Computer Science·Captain: wurtle

The Euclidean Steinitz–Bergström theoremResearch Paper

Motivation: keeping partial sums of vectors small

Given vectors $v_1,\dots,v_N$ in the Euclidean unit ball of $\mathbb R^d$ that sum to zero, can they always be reordered so that every partial sum stays in a ball whose radius depends only on $d$ ? Steinitz's lemma, from his work on rearrangements of conditionally convergent vector series, says yes: in any norm, radius $d$ suffices (Grinberg–Sevast'yanov 1980). For the Euclidean norm, the expected answer is $O(\sqrt d)$ , the Euclidean Steinitz–Bergström conjecture. A closely related prefix discrepancy problem asks for signs $\varepsilon_i\in\{\pm1\}$ , chosen once and for all, such that every signed prefix $\sum_{i\le k}\varepsilon_iv_i$ is $O(\sqrt d)$ , independently of $N$ . Both questions are basic in discrepancy theory and combinatorial vector balancing, with applications to scheduling, rounding and the analysis of online and streaming algorithms.

Timeline

1913 — Steinitz proves his rearrangement lemma for conditionally convergent vector series (historical account in Ambrus–Heck 2026, Section 2).
1954 — Behrend discusses the expected square-root growth in Euclidean space (Canad. J. Math., p. 108).
1980 — Grinberg and Sevast'yanov prove that partial sums can be kept within $d$ times the unit ball, for every norm (Funct. Anal. Appl.).
1994–2023 — Chobanyan's transference principle relates rearrangements to signed sums (Probability in Banach Spaces 9, 1994), later in a finite positive-forward, negative-reverse form (Chobanyan et al., Bull. TICMI 2023).
1998 / 2012 — Banaszczyk's Gaussian-measure balancing theorem (Random Structures Algorithms 1998) and his prefix bound $O(\sqrt d+\sqrt{\log N})$ for signed series and rearrangements (Random Structures Algorithms 2012).
2021 — Bansal, Jiang, Meka, Singla and Sinha state the $O(\sqrt d)$ prefix-signing question explicitly (Conjecture 6.3, arXiv:2111.07049).
2026 — Ambrus and Heck record the conjecture and its attribution to Bergström (Conjecture 5) and reduce it to a relaxed problem (Mathematika); Dutta, Jha and Jiang give efficient bounds $O(\sqrt d+d^{1/4}\log^{7/4}N)$ (arXiv:2604.13355).
2026 — An OpenAI preprint, The Euclidean Steinitz–Bergström theorem (OpenAI Math Release, September 24, 2026), claims the $O(\sqrt d)$ bound for both problems with an absolute constant. It has not been peer reviewed, and its proof is not formally verified.

Setting

Work in Euclidean space $\mathbb R^d$ with norm $\|\cdot\|_2$ , and let $v_1,\dots,v_N$ satisfy $\|v_i\|_2\le1$ ; repetitions and zero vectors are allowed. A prefix sum is $\sum_{i=1}^k$ for $0\le k\le N$ (the empty sum is $0$ ). For a zero-sum family, the Steinitz quantity

\beta(v_1,\dots,v_N)=\min_{\pi\in\mathfrak S_N}\ \max_{0\le k\le N}\Bigl\|\sum_{i=1}^kv_{\pi(i)}\Bigr\|_2

is the best achievable maximal prefix norm over all orderings. The Euclidean Steinitz constant $S_2(d)$ is its supremum over all such families.

Formalization targets

Goal: prescribed-order signing and Euclidean Steinitz with one absolute constant (Theorems 1.1 and 1.2)

There is an absolute constant $C$ such that for all $d,N\ge1$ and all $v_1,\dots,v_N\in\mathbb R^d$ with $\|v_i\|_2\le1$ :

(Theorem 1.1) there are signs $\varepsilon_i\in\{-1,1\}$ with

\max_{0\le k\le N}\Bigl\|\sum_{i=1}^k\varepsilon_iv_i\Bigr\|_2\le C\sqrt d ;

(Theorem 1.2) if moreover $\sum_iv_i=0$ , some permutation $\pi$ satisfies

\max_{0\le k\le N}\Bigl\|\sum_{i=1}^kv_{\pi(i)}\Bigr\|_2\le C\sqrt d .

The constant is not fixed. The simplex example in the source shows $S_2(d)\ge\tfrac12\sqrt d$ , so the order is optimal. The goal statement is published on the platform with status Open.

Significance

The result itself. Theorem 1.2 settles the Euclidean Steinitz–Bergström conjecture: $S_2(d)=\Theta(\sqrt d)$ . Theorem 1.1 settles the $\ell_2$ prefix-discrepancy question of Bansal et al., removing the $\sqrt{\log N}$ term in Banaszczyk's bound. A single choice of signs controls all prefixes at once, unlike terminal balancing results that bound one sum. The source also derives finite-dimensional $\ell_p$ Steinitz bounds and a colorful Steinitz theorem (Corollaries 8.1–8.2). The result is existential and gives no efficient algorithm.

Formalizing it. The statement is finite and elementary. The deduction of Theorem 1.2 from Theorem 1.1 is a short transference argument (Section 1.1 of the source), suitable as a first formalization step. The proof of Theorem 1.1 uses Gaussian measures of convex bodies, Dirichlet energies, Steiner symmetrization and Brownian survival estimates, which would make substantial reusable additions to Mathlib's probability and convex-geometry libraries.

Difficulty

Signing each prefix separately is easy, by terminal balancing results, but one common signing must work for all $N$ prefixes. Union bounds over prefixes and Banaszczyk's Gaussian-measure method lose a $\sqrt{\log N}$ factor, because the probability that a random walk stays in a ball of radius $C\sqrt d$ for $N$ steps decays with $N$ . The proof must therefore control a single body of coefficients enforcing all prefix constraints, with bounds independent of the number of steps.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin d), indexed by Fin N, with $d,N\ge1$ and $\|v_i\|\le1$ .
Prefixes are sums over $\{i : i < k\}$ for every natural $k\le N$ , so the empty prefix and the full sum are included.
SignedPrefixBound C asks for signs $\varepsilon_i\in\{-1,1\}$ (as reals) with every signed prefix at most $C\sqrt d$ . OrderingPrefixBound C asks, for zero-sum families, for a permutation $\pi$ with every reordered prefix at most $C\sqrt d$ . The goal is $\exists C,\ \mathrm{SignedPrefixBound}\,C\wedge\mathrm{OrderingPrefixBound}\,C$ ; the same constant serves both, as stated in the source.
The quantifier order is the source's: $C$ is chosen before $d$ , $N$ and the vectors.
Needed infrastructure: Gaussian measures of symmetric convex bodies, Steiner symmetrization, Dirichlet energies of densities, Ornstein–Uhlenbeck/Brownian survival estimates, and the Chobanyan transference. Contributions proving the transference step (Theorem 1.1 ⇒ Theorem 1.2) or the lower-bound example are welcome.

Selected references

V. S. Grinberg and S. V. Sevast'yanov, Value of the Steinitz constant, Funct. Anal. Appl. (1980).
F. A. Behrend, The Steinitz–Gross theorem on sums of vectors, Canad. J. Math. (1954).
S. Chobanyan, Convergence a.s. of rearranged random series in Banach space and associated inequalities, Probability in Banach Spaces 9 (1994).
W. Banaszczyk, Balancing vectors and Gaussian measures of n-dimensional convex bodies, Random Structures Algorithms (1998).
W. Banaszczyk, On series of signed vectors and their rearrangements, Random Structures Algorithms (2012).
N. Bansal, H. Jiang, R. Meka, S. Singla and M. Sinha, Prefix discrepancy, smoothed analysis, and combinatorial vector balancing, 2021. https://arxiv.org/abs/2111.07049
G. Ambrus and R. Heck, A note on the Steinitz Lemma, Mathematika (2026). https://doi.org/10.1112/mtk.70085
K. Dutta, A. V. Jha and H. Jiang, Near-optimal constructive bounds for $\ell_2$ prefix discrepancy and Steinitz problems via affine spectral independence, 2026. https://arxiv.org/abs/2604.13355
OpenAI, The Euclidean Steinitz–Bergström theorem, OpenAI Math Release preprint, September 24, 2026 (Theorems 1.1 and 1.2, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Euclidean-Steinitz-Bergstrom-theorem-September-24-2026/The-Euclidean-Steinitz-Bergstrom-theorem-September-24-2026.pdf

9 thms4 active usersReviewed

Completed

Analysis Harmonic Analysis·Captain: wurtle

The maximal triangular Hilbert transform at the symmetric pointResearch Paper

Motivation: the triangular Hilbert transform

The triangular Hilbert transform is a bilinear singular integral on the plane that couples translations in two different coordinate directions:

B(F,G)(x,y)=\mathrm{p.v.}\!\int_{\mathbb R}F(x+t,y)\,G(x,y+t)\,\frac{dt}{t}.

Paired with a third function, it becomes a trilinear form whose three inputs depend on the three pairs of variables of $(a,b,c)$ . This "triangular" or entangled structure defeats the time–frequency methods that handle the one-dimensional bilinear Hilbert transform. Boundedness of this operator is a model problem for multilinear singular integrals with simplex structure, and is closely tied to norm convergence and variation of ergodic averages for two commuting transformations. Thiele listed the symmetric case ( $L^3\times L^3\times L^3$ ) as Problem 13 in the 2017 collection Some problems in harmonic analysis.

Timeline

2010 — Demeter and Thiele study the two-dimensional bilinear Hilbert transform and highlight the flat triangular operator (Amer. J. Math.).
2012 — Kovač proves boundedness of the twisted paraproduct, a bipartite relative of the triangular form, by energy telescoping (Rev. Mat. Iberoam.).
2015 — Kovač, Thiele and Zorin-Kranich prove bounds for a Walsh (dyadic) model with one structurally restricted input (Forum Math. Sigma).
2016–2017 — Tao proves sublogarithmic cancellation for multilinear Hilbert transforms (Collect. Math.); Zorin-Kranich extends it to simplex Hilbert transforms (Math. Res. Lett.); Thiele's problem appears in Grafakos et al. (arXiv:1701.06637).
2019 — Durcik, Kovač, Škreb and Thiele obtain square-root cancellation across finitely many smooth scales (Ergodic Theory Dynam. Systems); Durcik, Kovač and Thiele prove power-type cancellation with hard truncations, still growing like $\sqrt{\log(R/\varepsilon)}$ at the symmetric point (J. Anal. Math.).
2021 — Durcik and Roos bound averages over directions (Proc. AMS); Christ, Durcik and Roos treat the curved variant along $(t,t^2)$ (Adv. Math.).
2026 — An OpenAI preprint, The maximal triangular Hilbert transform at the symmetric point (OpenAI Math Release, September 24, 2026), claims the scale-free $L^3\times L^3\to L^{3/2}$ bound for the maximal truncated operator. It has not been peer reviewed, and its proof is not formally verified.

Setting

For complex functions $F,G$ on $\mathbb R^2$ and $0<\varepsilon<R<\infty$ , the hard truncation is

B_{\varepsilon,R}(F,G)(x,y)=\int_{\varepsilon<|t|<R}F(x+t,y)\,G(x,y+t)\,\frac{dt}{t},

and the maximal truncation is

B_*(F,G)(x,y)=\sup_{0<\varepsilon<R<\infty}\bigl|B_{\varepsilon,R}(F,G)(x,y)\bigr| .

For $F,G\in L^3(\mathbb R^2)$ the finite truncations converge absolutely outside a common null set, and $B_*$ is measurable (Lemma 7.1 of the source).

Formalization targets

Goal: the maximal triangular Hilbert transform is bounded at the symmetric point (Theorem 1.1)

There is an absolute constant $C$ such that, for all complex $F,G\in L^3(\mathbb R^2)$ ,

\|B_*(F,G)\|_{L^{3/2}(\mathbb R^2)}\le C\,\|F\|_{L^3(\mathbb R^2)}\|G\|_{L^3(\mathbb R^2)} .

The Lean goal also includes the measure-theoretic preliminaries of Lemma 7.1: almost every point is a point where all finite truncations converge absolutely, and $B_*$ is almost-everywhere measurable. The goal statement is published on the platform with status Open.

Significance

The result itself. A uniform bound for the maximal operator controls a truncation chosen independently at each point, which is stronger than a uniform bound on each $B_{\varepsilon,R}$ . It yields existence of the joint principal value $B(F,G)$ almost everywhere and in $L^{3/2}$ (Theorem 7.2). By duality and a determinant-one change of variables, it gives endpoint-uniform bounds for the symmetric trilinear triangular form $\iiint G_0(a,b)G_1(b,c)G_2(c,a)\,\frac{da\,db\,dc}{a+b+c}$ , which resolves Thiele's Problem 13 positively. Earlier bounds all grew with the number of scales.

Formalizing it. The estimate is a clean statement in Mathlib's $L^p$ and lower-integral language. Its proof combines matrix trace inequalities, Gaussian heat-flow energies and discretization limits, all of which would have to be built. The finite-dimensional matrix inequalities (Sections 2–3 of the source) are self-contained and reusable for other entangled multilinear forms.

Difficulty

Time–frequency analysis, which handles the one-dimensional bilinear Hilbert transform, does not adapt to the triangular form because its three inputs are entangled: each depends on a different pair of variables, so no single frequency-localization serves all three. Energy and telescoping methods (Kovač; Durcik) work for bipartite forms, but the triangular cycle is the documented obstruction. Previous cancellation estimates lose a factor depending on the number of scales $\log(R/\varepsilon)$ . The maximal version adds a further difficulty: the truncation endpoints vary from point to point, so the energy argument must tolerate entries that switch on and off at independently chosen scales, without losses depending on the number of scales or on matrix dimensions.

Formalization scope

Functions are ℝ × ℝ → ℂ with Lebesgue measure; hypotheses are MemLp F 3 and MemLp G 3 (which include a.e. strong measurability).
truncation F G E z is the Bochner integral of $F(x+t,y)G(x,y+t)/t$ over $\{\varepsilon<|t|<R\}$ , with endpoints packaged as Endpoints ( $0<\varepsilon<R$ ).
GoodPoint requires integrability on the annuli $1/(n+2)<|t|<n+2$ for all $n$ , hence on every finite annulus. maximal is the ℝ≥0∞-valued supremum over all endpoint pairs at good points, and $0$ elsewhere. The goal asserts that almost every point is good, so this junk value cannot help.
The norm is $\bigl(\int^- B_*^{3/2}\bigr)^{2/3}$ in ℝ≥0∞, compared with eLpNorm F 3 * eLpNorm G 3. The constant is an existential ℝ≥0, so it is finite and independent of $F,G$ .
Needed infrastructure: discretization of $L^3$ functions, finite-dimensional trace inequalities for $\operatorname{tr}((R^*R)^{3/2})$ , Gaussian heat-flow monotonicity, one-dimensional Hardy–Littlewood maximal bounds, and limits of smooth truncations. Contributions on the matrix inequalities or the jump-control lemma are welcome.

Selected references

C. Demeter and C. Thiele, On the two-dimensional bilinear Hilbert transform, Amer. J. Math. (2010). https://doi.org/10.1353/ajm.0.0101
V. Kovač, Boundedness of the twisted paraproduct, Rev. Mat. Iberoam. https://doi.org/10.4171/RMI/707
V. Kovač, C. Thiele and P. Zorin-Kranich, Dyadic triangular Hilbert transform of two general functions and one not too general function, Forum Math. Sigma (2015). https://doi.org/10.1017/fms.2015.25
T. Tao, Cancellation for the multilinear Hilbert transform, Collect. Math. (2016). https://arxiv.org/abs/1505.06479v3
P. Zorin-Kranich, Cancellation for the simplex Hilbert transform, Math. Res. Lett. (2017). https://doi.org/10.4310/MRL.2017.v24.n2.a16
L. Grafakos, D. Oliveira e Silva, M. Pramanik, A. Seeger and B. Stovall, Some problems in harmonic analysis (2017), Section 9, Problem 13. https://arxiv.org/abs/1701.06637v1
P. Durcik, V. Kovač, K. A. Škreb and C. Thiele, Norm-variation of ergodic averages with respect to two commuting transformations, Ergodic Theory Dynam. Systems (2019). https://doi.org/10.1017/etds.2017.48
P. Durcik, V. Kovač and C. Thiele, Power-type cancellation for the simplex Hilbert transform, J. Anal. Math. (2019). https://doi.org/10.1007/s11854-019-0052-4
OpenAI, The maximal triangular Hilbert transform at the symmetric point, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 2; Lemma 7.1, p. 24). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-maximal-triangular-Hilbert-transform-at-the-symmetric-point-September-24-2026/paper.pdf

68 thms4 active usersReviewed

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Campaigns (experimental)

All missions

Holographic Quantum Matter I: Scalar Fields in AdS and the Mass–Dimension RelationResearch Paper

Motivation

Setting

Formalization targets

Goal: the two integration constants (eq. (28) at ω=k=0\omega=k=0ω=k=0)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Computational Optimal Transport V: A Feasible Pair of Kantorovich Potentials Is Optimal or Strictly Improves Along a Direction (1_S, −1_S′)Textbook

Motivation

Setting

Formalization targets

Goal: Proposition 3.6 (p. 416)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Computational Optimal Transport X: For the Cost c = d a Function Is a c-Transform if and only if It Is 1-Lipschitz, and Then f^c = −fTextbook

Motivation

Setting

Formalization targets

Goal: Proposition 6.1 (p. 472)

Milestones (from the book's proof, pp. 472–473)

Companion: the discrete formula (6.2) (p. 473)

Significance

Difficulty

Formalization scope

Selected references

Kernel Distributionally Robust Optimization: Generalized Duality Theorem and Stochastic Approximation: The Worst-Case Risk over an RKHS Ambiguity Set Equals Its Support-Function DualResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.1 (Generalized Duality), p. 5

Milestones (the proof of Proposition A.1, pp. 13–15, and Appendix D, pp. 22–23)

Companions

Significance

Difficulty

Formalization scope

Selected references

Information-Theoretic Analysis of Generalization Capability of Learning Algorithms I: The Expected Generalization Error Is at Most √(2σ²I(S;W)/n) (Theorem 1)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 4)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Bootstrap Robust Prescriptive Analytics 2: The Entropic Robust Nadaraya-Watson Budget Equals inf{α : ν log Σ D·exp((L−α)w/ν) + rν ≤ 0}Research Paper

Motivation

Setting

Formalization targets

Goal: Lemma 2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Proximal Algorithms I: A Point Minimizes f + g Exactly When It Is a Fixed Point of the Forward-Backward Operator x ↦ prox_λg(x − λ∇f(x))Research Paper

Motivation

Setting

Formalization targets

Goal: fixed points of the forward-backward operator

Supporting statements

Why the result matters

Difficulty

Formalization scope

Selected references

Online Learning and Online Convex Optimization 4: Finite Littlestone Dimension Gives Agnostic Online Regret 2√(Ldim·ln(eT/Ldim)·T)Research Paper

Motivation

Goal: the two integration constants (eq. (28) at $\omega=k=0$ )

Goal: Theorem LL.2 (Little's Law over $[0, T]$ , p. 539)