Theoretical Computer Science

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$:

1. (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 ;$$

2. (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

Motivation

Split Euclidean space into finitely many measurable cells and record, for each cell, its Gaussian first moment, the integral of $x$ against the standard Gaussian measure over that cell. How large can the sum of the squared lengths of these vectors be? The propeller conjecture predicts that, with at least three cells in dimension at least two, the answer is $9/(8\pi)$, attained by three planar sectors of angle $2\pi/3$ (a "propeller") times the orthogonal complement. The question arose in Khot and Naor's work on approximate kernel clustering (Mathematika 2009), where this Gaussian partition parameter determines both the approximation ratio of Gaussian rounding and the matching Unique-Games hardness threshold. The surprise is that more cells or more dimensions do not help: the optimum uses only three cells in a plane.

This mission asks for a formal proof of the propeller bound in every dimension, 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

• 1983–2003 — The Gaussian Minkowski (Ehrhard) inequality: Ehrhard for convex sets (Math. Scand. 1983), Latała when one set is convex (Studia Math. 1996), Borell for Borel sets (C. R. Acad. Sci. 2003); later van Handel's game proof (PTRF 2018).
• 2009 — Khot and Naor introduce the problem, reduce maximizers to conical partitions in the span of their centroids, and compute the three-cell value (Mathematika 2009); see also their sharp kernel-clustering paper (RSA 2013).
• 2013 — Heilman, Jagannath and Naor prove the conjecture in $\mathbb R^3$ with a computer-assisted argument (DCG 2013).
• 2022 — Heilman gives a conditional route for three or four cells in any dimension, under a stability hypothesis on noise-stability maximizers (arXiv:2209.11216).
• September 2026 — The OpenAI preprint claims the bound for every dimension and every number of cells (Theorem 1.1, p. 1).

Setting

Let $\gamma_d$ be the standard Gaussian probability measure on $\mathbb R^d$, with density $(2\pi)^{-d/2}e^{-\|x\|^2/2}$. For a measurable set $A\subseteq\mathbb R^d$, its centroid is the unnormalized vector

$$z(A)=\int_A x\,d\gamma_d(x)\in\mathbb R^d .$$

A measurable partition $(A_1,\dots,A_k)$ of $\mathbb R^d$ consists of measurable sets such that almost every point (for $\gamma_d$) lies in exactly one of them; empty cells and arbitrary cell probabilities are allowed. Its value is $F(A)=\sum_{i=1}^k\|z(A_i)\|^2$. The propeller is the partition of $\mathbb R^d$, $d\ge2$, into the three sets $S_j\times\mathbb R^{d-2}$, where $S_1,S_2,S_3$ are the planar sectors of opening $2\pi/3$ bounded by the rays at angles $\pm\pi/3$ and $\pi$, with any further cells empty.

Formalization targets

Goal: Theorem 1.1 (p. 1)

For all positive integers $d,k$ and every measurable partition $(A_1,\dots,A_k)$ of $\mathbb R^d$,

$$\sum_{i=1}^k\Bigl\|\int_{A_i}x\,d\gamma_d(x)\Bigr\|^2\ \le\ \frac{9}{8\pi},$$

and for $d\ge2$, $k\ge3$ the propeller is a measurable partition attaining equality.

Significance

The result itself. It settles the propeller conjecture in all dimensions and for all numbers of cells, without constraints on cell masses. Through Khot and Naor's analysis, the constant $9/(8\pi)$ fixes the loss factor $\alpha_k=\frac{8\pi}{9}(1-\frac1k)$ of Gaussian rounding for identity-target kernel clustering; combined with the companion Unique Games preprint, the preprint deduces NP-hardness of any better fixed loss factor (Theorem 6.1, p. 18). The bound also gives a sharp inequality for expected Gaussian maxima (Corollary 5.1, p. 17).

Formalizing it. A formal proof needs Gaussian measures on Euclidean space (available in Mathlib as stdGaussian), a compactness argument for extremal partitions, the convex case of the Ehrhard inequality, and the three-dimensional theorem of Heilman, Jagannath and Naor, which the preprint uses as an established input and which itself relies on a finite computer verification. Each of these is a reusable component; the three-dimensional case alone would be a substantial formalization.

Difficulty

The optimization runs over all measurable partitions, with both shapes and probabilities free. Khot and Naor's reduction gives conical extremizers whose $m$ nonzero centroids span an $(m-1)$-dimensional space, so the three-dimensional theorem disposes of $m\le4$ active cells. The remaining cases $m\ge5$ cannot be handled by any fixed finite computation. The preprint constrains them in two ways: deleting one score costs a definite amount of expected maximum, via concavity from the Ehrhard inequality (Section 3), and competition against two residual scores constrains a covariance determinant (Section 4, Lemma 4.1 and Corollary 4.2, pp. 11–12). Combining these must rule out every configuration with five or more cells.

Formalization scope

• Space d is EuclideanSpace ℝ (Fin d) and the measure is stdGaussian. IsPartition A asks each cell to be measurable and almost every point to lie in exactly one cell, matching the paper's convention that partitions are taken up to null sets.
• centroid A is the Bochner integral of the identity over A; value sums squared Euclidean norms. Integrability holds because Gaussian measures have finite first moments.
• The goal is a conjunction: the bound for all $d,k\ge1$, and, for $d\ge2$, $k\ge3$, that the explicit three-sector propeller d k (cells $\ge3$ empty) is a partition with value exactly $9/(8\pi)$. The sectors are written with closed inequalities, so they overlap only on null rays.
• No hypothesis is vacuous: the case $k=1$ is included (value $0$), and the equality clause pins the constant.

Selected references

• OpenAI, The Gaussian propeller bound in every dimension, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Gaussian-Propeller-Bound-in-Every-Dimension-September-24-2026/main.pdf
• S. Khot, A. Naor, Approximate kernel clustering, Mathematika 55 (2009), 129–165. https://doi.org/10.1112/S002557930000098X
• S. Khot, A. Naor, Sharp kernel clustering algorithms and their associated Grothendieck inequalities, Random Struct. Algorithms 42 (2013), 269–300. https://doi.org/10.1002/rsa.20398
• S. Heilman, A. Jagannath, A. Naor, Solution of the Propeller Conjecture in $\mathbb R^3$, Discrete Comput. Geom. 50 (2013), 263–305. https://doi.org/10.1007/s00454-013-9530-0
• S. Heilman, Hyperstable sets with voting and algorithmic hardness applications, arXiv:2209.11216 (2022). https://arxiv.org/abs/2209.11216v1
• A. Ehrhard, Symétrisation dans l'espace de Gauss, Math. Scand. 53 (1983), 281–301. https://doi.org/10.7146/math.scand.a-12035
• R. Latała, A note on the Ehrhard inequality, Studia Math. 118 (1996), 169–174. https://doi.org/10.4064/sm-118-2-169-174
• C. Borell, The Ehrhard inequality, C. R. Acad. Sci. Paris 337 (2003), 663–666. https://doi.org/10.1016/j.crma.2003.09.031
• R. van Handel, The Borell–Ehrhard game, Probab. Theory Relat. Fields 170 (2018), 555–585. https://doi.org/10.1007/s00440-017-0762-4
• E. Mossel, R. O'Donnell, K. Oleszkiewicz, Noise stability of functions with low influences: invariance and optimality, Ann. of Math. 171 (2010), 295–341. https://doi.org/10.4007/annals.2010.171.295

Motivation: $L_1$ embeddings, sparsest cut and the GNRS conjecture

A finite metric embeds into $L_1$ exactly when it is a nonnegative combination of cut metrics $\delta_S(u,v)=|\mathbf 1_S(u)-\mathbf 1_S(v)|$. This makes $L_1$ distortion the right measure for the flow–cut gap: given edge capacities and pairwise demands, the ratio between the sparsest cut value $\phi_*$ and the maximum concurrent flow $\lambda_*$. Linial, London and Rabinovich (1995) and Aumann and Rabani (1998) developed this connection, and Gupta, Newman, Rabinovich and Sinclair (2004) proved that the worst flow–cut gap on a fixed graph equals the worst $L_1$ distortion of its weighted shortest-path metrics. They conjectured that every proper minor-closed family embeds into $L_1$ with uniformly bounded distortion (the GNRS conjecture). Graphs of bounded treewidth form one of its basic cases.

Timeline

• 1986 — Robertson and Seymour: excluding a fixed planar graph as a minor bounds the treewidth (JCTB 1986).
• 2004 — Gupta, Newman, Rabinovich and Sinclair prove the treewidth-two (series-parallel) case, show that some series-parallel metrics need expected tree distortion $\Omega(\log n)$, and state the GNRS conjecture (Combinatorica 2004).
• 2006 — Chekuri, Gupta, Newman, Rabinovich and Sinclair: bounded distortion for $k$-outerplanar graphs (SIDMA 2006).
• 2008–2010 — Chakrabarti, Jaffe, Lee and Vincent obtain the optimal bound $2$ for treewidth two (FOCS 2008), matched by Lee and Raghavendra (DCG 2010).
• 2010 — Chlamtáč, Krauthgamer and Raghavendra: bounded distortion for bounded treewidth under a local-consistency assumption on small vertex sets (APPROX/RANDOM 2010).
• 2013 — Lee and Sidiropoulos settle bounded pathwidth via stochastic tree embeddings (Combinatorica 2013); Lee and Poore treat 2-sums of a fixed finite family (SoCG 2013).
• 2022 — Abraham, Filtser, Gupta and Neiman: $O(\sqrt p)$ distortion for pathwidth $p$ (SICOMP 2022).
• 2025 — Filtser et al.: optimal padded decompositions for bounded treewidth and an $O(\sqrt{\log(2+t)\log n})$ bound (TheoretiCS 2025).
• 2026 — An OpenAI preprint, $L_1$ Embeddings of Graphs of Bounded Treewidth (OpenAI Math Release, September 23, 2026), claims a uniform bound for every fixed treewidth. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

Let $G=(V,E)$ be a finite connected graph with edge lengths $\ell:E\to(0,\infty)$. The shortest-path metric $d_{G,\ell}(u,v)$ is the least total length of a path from $u$ to $v$.

A tree decomposition of $G$ is a finite tree $T$ with bags $B_t\subseteq V$ ($t\in V(T)$) such that the bags cover $V$, each edge has both endpoints in some bag, and for each vertex $v$ the nodes whose bag contains $v$ induce a connected subtree. In this mission, as in the source, $k$ bounds the bag cardinality $|B_t|\le k$, so the treewidth bound is $k-1$.

A map $F:V\to\ell_1^m$ has distortion at most $C$ if $d_{G,\ell}(u,v)\le\|F(u)-F(v)\|_1\le C\,d_{G,\ell}(u,v)$.

Formalization targets

Goal: Theorem 1.1 (bounded-treewidth graph metrics in $L_1$)

For every integer $k\ge2$ there is a constant $C_k\ge1$ such that for every nonempty finite connected graph $G$ with a tree decomposition of bag size at most $k$ and every $\ell:E\to(0,\infty)$, there are $m$ and $F:V\to\ell_1^m$ with

$$d_{G,\ell}(u,v)\;\le\;\|F(u)-F(v)\|_1\;\le\;C_k\,d_{G,\ell}(u,v)\qquad(u,v\in V).$$

$C_k$ is independent of the number of vertices, the decomposition and all ratios of edge lengths; the goal asserts only its existence. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem settles the bounded-treewidth case of the GNRS conjecture. Through the GNRS equivalence, it gives $\lambda_*\le\phi_*\le C_k\lambda_*$ for every multicommodity instance on graphs of treewidth less than $k$. By the Robertson–Seymour excluded-planar-minor theorem it also covers every family excluding a fixed planar minor. Combined with known approximation algorithms for the minimum $L_1$ distortion (Gupta–Talwar–Witmer 2013; Cohen-Addad–Mömke–Verdugo 2024), it yields fixed-parameter-time embeddings of distortion $(2+\varepsilon)C_k$. With the planar companion preprint it covers the almost-embeddable families of Lee and Sidiropoulos.

Formalizing it. The proof constructs cut measures directly on a tree decomposition and combines them with padded random partitions from the literature. A formal proof would certify that the constants depend only on $k$, the point at which earlier approaches lost uniformity.

Difficulty

The successful pathwidth approach embeds the graph stochastically into dominating trees, but that route cannot work here: some series-parallel metrics require expected tree distortion $\Omega(\log n)$ (GNRS 2004, Theorem 5.6). Local-consistency approaches assume that small vertex sets admit compatible isometric cut representations, which a general bounded-treewidth metric need not provide. Multiscale constructions from padded partitions give good separation at each scale, but summing their contributions loses a factor growing with the number of scales. The construction must handle arbitrary branching of the decomposition tree and arbitrary edge-length ratios without such accumulation.

Formalization scope

• The vertex type V is any nonempty Fintype with decidable equality; G : SimpleGraph V is connected.
• HasTreeDecomposition G k: a tree T on Fin n, bags Fin n → Finset V covering all vertices and all edges, with the bags containing each vertex inducing a connected subgraph of T, and all bags of cardinality at most k.
• Edge lengths are ℓ : G.edgeSet → ℝ, strictly positive. shortestPathDistance is the sInf of lengths of paths (IsPath) from $u$ to $v$; this set is finite and nonempty for a connected finite graph, so the infimum is the true distance.
• The target is the finite-dimensional space PiLp 1 (Fin m → ℝ) with $m$ chosen per graph; this is the source's remark (p. 2) that the target can be taken to be finite-dimensional $\ell_1$, and it is at least as strong as an $L_1(\mu)$ target.
• The constant C depends only on k and is quantified before the graph.
• Infrastructure needed: tree decompositions, cut-measure representations of $\ell_1$ metrics, Markov flows on layered graphs, padded decompositions. Tree-decomposition and cut-metric infrastructure is reusable.

Selected references

• N. Robertson, P. D. Seymour, Graph minors. V. Excluding a planar graph, J. Combin. Theory Ser. B 41 (1986), 92–114. https://doi.org/10.1016/0095-8956(86)90030-4
• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15 (1995), 215–245. https://doi.org/10.1007/BF01200757
• Y. Aumann, Y. Rabani, An $O(\log k)$ approximate min-cut max-flow theorem and approximation algorithm, SIAM J. Comput. 27 (1998), 291–301. https://doi.org/10.1137/S0097539794285983
• A. Gupta, I. Newman, Y. Rabinovich, A. Sinclair, Cuts, trees and $\ell_1$-embeddings of graphs, Combinatorica 24 (2004), 233–269. https://doi.org/10.1007/s00493-004-0015-x
• A. Chakrabarti, A. Jaffe, J. R. Lee, J. Vincent, Embeddings of topological graphs: lossy invariants, linearization, and 2-sums, FOCS 2008, 761–770. https://doi.org/10.1109/FOCS.2008.79
• J. R. Lee, P. Raghavendra, Coarse differentiation and multi-flows in planar graphs, Discrete Comput. Geom. 43 (2010), 346–362. https://doi.org/10.1007/s00454-009-9172-4
• E. Chlamtáč, R. Krauthgamer, P. Raghavendra, Approximating sparsest cut in graphs of bounded treewidth, APPROX/RANDOM 2010, LNCS 6302, 124–137. https://doi.org/10.1007/978-3-642-15369-3_10
• J. R. Lee, A. Sidiropoulos, Pathwidth, trees, and random embeddings, Combinatorica 33 (2013), 349–374. https://doi.org/10.1007/s00493-013-2685-8
• I. Abraham, A. Filtser, A. Gupta, O. Neiman, Metric embedding via shortest path decompositions, SIAM J. Comput. 51 (2022), 290–314. https://doi.org/10.1137/19M1296021
• A. Filtser, T. Friedrich, D. Issac, N. Kumar, H. Le, N. Mallek, Z. Zeif, Optimal padded decomposition for bounded treewidth graphs, TheoretiCS 4 (2025), Article 22. https://doi.org/10.46298/theoretics.25.22
• OpenAI, $L_1$ Embeddings of Graphs of Bounded Treewidth, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/L1-Embeddings-of-Graphs-of-Bounded-Treewidth-September-23-2026/paper.pdf

Motivation: cut metrics, flows and the planar embedding conjecture

A finite metric space embeds into $L_1$ exactly when its metric is a nonnegative combination of cut metrics $\delta_S(x,y)=|\mathbf 1_S(x)-\mathbf 1_S(y)|$. For this reason the least distortion with which a graph metric embeds into $L_1$ governs the gap between multicommodity flow and sparsest cut: Linial, London and Rabinovich (1995) and Aumann and Rabani (1998) connected metric embeddings to the approximate max-flow/min-cut theorem, and Gupta, Newman, Rabinovich and Sinclair (2004) proved that the worst flow–cut gap on a fixed graph equals the worst $L_1$ distortion of its weighted shortest-path metrics. They conjectured (the GNRS conjecture) that every proper minor-closed graph family embeds into $L_1$ with uniformly bounded distortion. The planar case has been the central open instance.

Timeline

• 1981 — Okamura and Seymour: multicommodity flows in planar graphs with all terminals on one face (JCTB 1981), giving isometric $L_1$ representations of one-face metrics.
• 1993 — Klein, Plotkin and Rao: decompositions of graphs excluding a fixed minor (STOC 1993).
• 1999 — Rao: every $n$-vertex planar metric embeds into $L_1$ (via Euclidean space) with distortion $O(\sqrt{\log n})$ (SoCG 1999).
• 2003 — Newman and Rabinovich: series-parallel metrics may need $\Omega(\sqrt{\log n})$ distortion into Euclidean space, so the Euclidean route cannot give a constant (DCG 2003).
• 2004 — Gupta, Newman, Rabinovich and Sinclair: constant distortion for series-parallel graphs, and the GNRS conjecture (Combinatorica 2004).
• 2006 — Chekuri, Gupta, Newman, Rabinovich and Sinclair: $k$-outerplanar graphs, with a bound exponential in $k$ (SIDMA 2006).
• 2008–2010 — Chakrabarti, Jaffe, Lee and Vincent: sharp bound $2$ for series-parallel graphs (FOCS 2008); Lee and Raghavendra: matching lower bound (DCG 2010). Lee and Sidiropoulos relate the planar case to the full conjecture (STOC 2009).
• 2013 — Sidiropoulos: constant distortion for planar metrics realized in nonpositively curved simply connected surfaces (FOCS 2013).
• 2019–2025 — Face-cover bounds by Krauthgamer, Lee and Rika (SODA 2019) and Filtser (TALG 2025); Abraham, Filtser, Gupta and Neiman recover Rao's bound via shortest-path decompositions (SICOMP 2022).
• 2026 — An OpenAI preprint, Planar Graph Metrics Embed into $L_1$ with Constant Distortion (OpenAI Math Release, September 23, 2026), claims the planar case of the GNRS conjecture. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

Let $G$ be a finite connected simple graph on vertex set $V=\{0,\dots,n-1\}$ with symmetric edge lengths $\ell(u,v)=\ell(v,u)>0$ on edges. The graph metric $d_G(x,y)$ is the infimum of $\sum\ell(e)$ over walks from $x$ to $y$. $G$ is planar if it has a drawing in $\mathbb R^2$: distinct points for vertices and, for each edge, an injective arc between its endpoints whose interior avoids every vertex and meets the interior of no other edge.

A map $f:V\to L_1(\Omega,\mu)$ into the real $L_1$ space of some measure space has distortion at most $C$ if $d_G(x,y)\le\|f(x)-f(y)\|_1\le C\,d_G(x,y)$ for all $x,y$.

Formalization targets

Goal: Theorem 1.1 (planar graph metrics in $L_1$)

There is a constant $C\ge1$ such that for every $n$, every connected planar graph $G$ on $n$ vertices and every symmetric positive edge-length function $\ell$, there are a measure space $(\Omega,\mathcal F,\mu)$ and $f:V\to L_1(\Omega,\mathcal F,\mu;\mathbb R)$ with

$$d_G(x,y)\;\le\;\|f(x)-f(y)\|_1\;\le\;C\,d_G(x,y)\qquad(x,y\in V).$$

The constant is not fixed: the goal asserts only existence, so any improvement of the constant is compatible with it. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem settles the planar case of the GNRS conjecture. By the Gupta–Newman–Rabinovich–Sinclair equivalence it gives a universal constant bound on the fractional flow–cut gap for arbitrary demands in planar graphs. With the bounded-treewidth companion preprint it also yields constant distortion for the fixed-parameter almost-embeddable families of Lee and Sidiropoulos (Corollary 10.1 of the source). The general clique-sum closure needed for the full GNRS conjecture is not established.

Formalizing it. The statement is elementary (finite graphs, arcs in the plane, an $L^1$ space), yet the proof combines a geometric column model of planar graphs, random multiscale cut constructions and packing estimates. A formal proof would certify every scale-combination step, where errors in uniformity are easy to make.

Difficulty

Standard random-partition methods for planar graphs separate pairs at each distance scale with good probability, but naive summation over scales costs a factor proportional to the number of scales, which is unbounded when edge lengths vary. Embedding first into Euclidean space cannot work: Newman–Rabinovich show $\Omega(\sqrt{\log n})$ Euclidean distortion is necessary already for series-parallel graphs. The difficulty is to combine separations at different scales while keeping a single uniform upper bound on every edge.

Formalization scope

• Vertices are Fin n; the graph is a SimpleGraph (Fin n) with G.Connected (so $n\ge1$). Singletons are allowed.
• IsPlanar G asks for an injective vertex placement in ℝ × ℝ and, for each ordered adjacent pair, an injective continuous arc on the unit interval with the right endpoints, whose interior avoids all vertex points and meets the interior of another arc only if it is the same unoriented edge.
• Edge lengths are a function Fin n → Fin n → ℝ, symmetric, and positive on adjacent pairs; values on non-adjacent pairs are irrelevant. graphDistance is the sInf of walk lengths; for a connected graph with nonnegative edge lengths the set of walk lengths is nonempty and bounded below, so the infimum is the genuine shortest-path distance.
• The target space is MeasureTheory.Lp Ω ℝ 1 μ for an existentially chosen measure space, and the inequalities are stated without a rescaling factor (the rescaling is absorbed into $f$).
• Infrastructure needed: plane drawings and their combinatorial consequences (rotation systems, noncrossing column models), cut-metric representations of $L_1$ metrics, and the probabilistic multiscale construction. Plane-drawing and cut-metric infrastructure is reusable.

Selected references

• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15 (1995). https://doi.org/10.1007/BF01200757
• Y. Aumann, Y. Rabani, An $O(\log k)$ approximate min-cut max-flow theorem and approximation algorithm, SIAM J. Comput. (1998). https://doi.org/10.1137/S0097539794285983
• A. Gupta, I. Newman, Y. Rabinovich, A. Sinclair, Cuts, trees and $\ell_1$-embeddings of graphs, Combinatorica (2004). https://doi.org/10.1007/s00493-004-0015-x
• S. Rao, Small distortion and volume preserving embeddings for planar and Euclidean metrics, SoCG 1999. https://doi.org/10.1145/304893.304983
• I. Newman, Y. Rabinovich, A lower bound on the distortion of embedding planar metrics into Euclidean space, Discrete Comput. Geom. (2003). https://doi.org/10.1007/s00454-002-2813-5
• C. Chekuri, A. Gupta, I. Newman, Y. Rabinovich, A. Sinclair, Embedding $k$-outerplanar graphs into $\ell_1$, SIAM J. Discrete Math. (2006). https://doi.org/10.1137/S0895480102417379
• A. Chakrabarti, A. Jaffe, J. R. Lee, J. Vincent, Embeddings of topological graphs: lossy invariants, linearization, and 2-sums, FOCS 2008. https://doi.org/10.1109/FOCS.2008.79
• J. R. Lee, A. Sidiropoulos, On the geometry of graphs with a forbidden minor, STOC 2009. https://doi.org/10.1145/1536414.1536450
• A. Sidiropoulos, Non-positive curvature and the planar embedding conjecture, FOCS 2013. https://doi.org/10.1109/FOCS.2013.27
• I. Abraham, A. Filtser, A. Gupta, O. Neiman, Metric embedding via shortest path decompositions, SIAM J. Comput. (2022). https://doi.org/10.1137/19M1296021
• A. Filtser, A face cover perspective to $\ell_1$ embeddings of planar graphs, ACM Trans. Algorithms (2025). https://doi.org/10.1145/3686800
• OpenAI, Planar Graph Metrics Embed into $L_1$ with Constant Distortion, OpenAI Math Release preprint, September 23, 2026 (source of the goal; Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Planar-Graph-Metrics-Embed-into-L1-with-Constant-Distortion-September-23-2026/paper.pdf

Motivation

In the local model of differential privacy, each individual randomizes their own data before handing it to an untrusted learner. Local protocols are the deployed form of private data collection, and in practice every round of interaction with the population is expensive: the learner must broadcast new instructions and wait for new reports. Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith, What Can We Learn Privately? (arXiv:0803.0924v3, published in SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090; theorem numbers below are those of arXiv v3) show that local learning is equivalent to learning with statistical queries (SQ) in the sense of Kearns (1998), and that the equivalence maps noninteractive local learners to nonadaptive SQ learners. The question whether interaction is ever necessary in the local model therefore becomes the question whether adaptivity is ever necessary for SQ learning.

This mission formalizes the paper's answer (§5.3, Theorem 5.16): a concept class, MASKED-PARITY, that an adaptive SQ learner learns exactly with $d+1$ queries in two rounds, while every nonadaptive SQ learner with fewer than exponentially many queries fails against a specific valid oracle, under the uniform distribution on examples.

Setting

Fix $d$, a power of two. The domain is $D=\{0,1\}^d\times\{0,1\}^{\log d}\times\{0,1\}$, with points $u=(x,i,b)$, and examples are drawn from the uniform distribution $\mathcal D$ on $D$. For $r\in\{0,1\}^d$ and $a\in\{0,1\}$, the concept $c_{r,a}:D\to\{+1,-1\}$ is

$$c_{r,a}(x,i,b)=\begin{cases}(-1)^{r\odot x+a}&b=0,\\(-1)^{r_i}&b=1,\end{cases}$$

where $r\odot x$ is the inner product modulo 2. MASKED-PARITY is the class $\{c_{r,a}\}$: on the half $b=0$ it is the parity $r$ or its negation, according to the mask $a$; on the half $b=1$ it reveals the bit $r_i$.

A statistical query is a function $g(u,y)$ of an example and a label together with a tolerance $\tau$. The SQ oracle for the target $c$ answers with any real $v$ such that $|v-\mathbb E_{u\sim\mathcal D}[g(u,c(u))]|\le\tau$; the learner must succeed for every such answer. An SQ learner is nonadaptive if it fixes all its queries before receiving any answer, and adaptive otherwise. Write $\langle f,h\rangle=\mathbb E_{u\sim\mathcal D}[f(u)h(u)]$ and $\mathrm{err}(f,h)=\Pr_{u\sim\mathcal D}[f(u)\ne h(u)]$.

The lower bound uses the decomposition of a query into $f_g(u)=\frac{g(u,1)-g(u,-1)}2$ and $C_g=\frac12\mathbb E[g(u,1)+g(u,-1)]$, the restrictions $c^s_{r,a}$, $f^s_g$ of $c_{r,a}$ and $f_g$ to the half $b=s$ (equation (6)), and the oracle

$$\mathcal O_{c_{r,a},\mathcal D}(g,\tau)=\begin{cases}C_g+\langle f^1_g,c^1_{r,a}\rangle&\text{if }|\langle f^0_g,c^0_{r,a}\rangle|<\tau,\\ \mathbb E[g(u,c_{r,a}(u))]&\text{otherwise.}\end{cases}$$

Formalization targets

Goal: Theorem 5.16 (p. 27)

1. There is a two-round SQ learner ($d$ queries, then one), with $\{0,1\}$-valued queries of tolerance at least $\frac1{4d+1}$, that outputs $c_{r,a}$ for every target and every valid answers.
2. $\mathcal O$ is a valid SQ oracle, and every nonadaptive learner making $t$ queries with values $\pm1$ and tolerance at least $2^{-d/3}$, run against $\mathcal O$ on a uniformly random target, satisfies

$$\Pr_{c_{\bar r,\bar a}}\Bigl[\mathrm{err}(c_{\bar r,\bar a},h)\ge\tfrac14\Bigr]\ge\frac12-\frac t{2^{d/3+2}}.$$

Milestones

• Proposition 5.18 (p. 28): the learner $\mathcal A_{\mathrm{MP}}$ recovers $\hat r=r$ and $\hat a=a$ from every valid answers.
• Equation (7) (p. 29): $\mathbb E[g(u,c_{r,a}(u))]=C_g+\langle f^0_g,c^0_{r,a}\rangle+\langle f^1_g,c^1_{r,a}\rangle$.
• The oracle (p. 30): $\mathcal O$ is valid and answers identically on $c_{r,0}$ and $c_{r,1}$ when $|\langle f^0_g,c^0_{r,0}\rangle|<\tau$.
• Orthogonality (p. 30): $\langle c^0_{r,a},c^0_{r',a}\rangle$ is $1/2$ if $r=r'$ and $0$ otherwise.
• Bessel bound (p. 30): $\sum_{(r,a)}2\langle f^0_g,c^0_{r,a}\rangle^2\le1$ for $\pm1$-valued $g$.
• Counting (p. 30): at most $2^{2d/3-1}$ pairs $(r,a)$ have $|\langle f^0_g,c^0_{r,a}\rangle|\ge2^{-d/3}$.
• $\Pr[\mathit{Good}]\ge1-t/2^{d/3+2}$ (p. 30).

Significance

The result. Combined with the paper's equivalence between local and SQ learning (Theorem 5.14), Theorem 5.16 shows that interaction is sometimes necessary in local differential privacy: there is a class learnable by an interactive local protocol with polynomially many examples, but not by any noninteractive one with fewer than exponentially many (Corollary 5.17). The separation concerns strong learning under a fixed distribution; the paper notes that adaptive and nonadaptive SQ learning coincide for weak learning, and that a distribution-free separation was left open.

Formalizing it. The result is proved in the paper and has, to our knowledge, no machine-checked proof. The mission produces a self-contained Lean model of statistical query learning with labelled queries and adversarial oracles, a finite Fourier calculus for parities on $\{0,1\}^d$ (orthogonality and a Bessel inequality for $\pm1$-valued functions), and the counting and union-bound argument of SQ lower bounds. The proof of part (2) contains several printed slips (listed below); a formal proof settles the corrected argument.

Difficulty

The upper bound is a direct computation. The difficulty is in part (2): the learner's hypothesis may be any function, not a concept of the class, and the lower bound must hold for every nonadaptive strategy at once. A naive argument that each query "reveals little about $a$" fails, because the true answer to a query does depend on $a$; the argument needs an oracle that is valid (within tolerance of the truth) and yet independent of $a$ on most targets, and a quantitative bound on how many targets any single $\pm1$-valued query can correlate with on the half $b=0$. That bound is an $L^2$ statement over all $2^{d+1}$ concepts, not a pointwise one.

Formalization scope

• Domain and distribution. The index $i\in\{0,1\}^{\log d}$ is encoded as Fin d, and every theorem assumes $d=2^m$ (implicit in the paper). Vectors are Fin d → ZMod 2, with 0-based bits. Expectations are averages over the finite domain; probabilities over the target are counts of pairs $(r,a)$ divided by $2^{d+1}$.
• Values. Concepts, hypotheses and queries are real-valued; labels $\pm1$ are reals. Queries in part (1) take values in $\{0,1\}$, as $\mathcal A_{\mathrm{MP}}$'s do; queries in part (2) take values $\pm1$ on labels $\pm1$, as in the paper's proof. The paper allows non-Boolean queries (p. 19); a version of part (2) for real queries with values in $[-1,1]$ is a true strengthening that the same argument supports, and is not stated.
• Oracles. An SQ oracle is adversarial within the tolerance: the upper bound holds for every valid answer. Part (2) exhibits the paper's oracle $\mathcal O$ and asserts its validity for every $\tau>0$. Without that conjunct an "oracle" that ignores the tolerance would make part (2) trivial; the statement rules this out.
• Learners. Learners are deterministic structures (a nonadaptive learner is a list of queries and tolerances plus an output map; a two-round learner's second-round queries are functions of the first-round answers). A randomized learner is a mixture over its coins and the bounds hold coin by coin. "Efficient" is not modelled. The informal "with a polynomial number of queries" is formalized through its quantitative "Specifically" sentence.
• Real powers. $2^{d/3}$, $2^{2d/3-1}$ and $2^{d/3+2}$ are real powers; no natural-number division is used.
• Corrections of the proof (not of the theorem). The event $\mathit{Good}$ on p. 30 is printed with $c_{\bar r,\bar a}$ and $\le$; the milestone uses $c^0_{\bar r,\bar a}$ and the strict $<$, which is what the counting display and the oracle's test require. The quotient $2^{2d/3-1}/2^{d+1}$ is printed as $2^{-d/3}$ and equals $2^{-d/3-2}$; "$c^0_{r,0}=-c^0_{r,0}$" should read $c^0_{r,1}=-c^0_{r,0}$. The final display of the proof gives $\frac12(1-t/2^{d/3+2})$, which is at least the theorem's bound.

Contributions welcome: the Fourier facts for $\{0,1\}^d$ (reusable for any parity-based SQ lower bound), the general decomposition (7), and the probability bound of part (2) from the milestones.

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.
• 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.
• N. Bshouty, V. Feldman, On using extended statistical queries to avoid membership queries, J. Mach. Learn. Res. 2 (2002) 359–395. JMLR.

Motivation

In the local model of differential privacy, no trusted curator holds the data: each individual randomizes their own record before handing it to the analyst. This is the model of randomized response in survey statistics and of the privacy-preserving telemetry deployed by large software vendors. Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith, What Can We Learn Privately? (arXiv:0803.0924v3, published in SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090), asked which learning tasks remain possible in this model. Their answer (§5) is that local algorithms are exactly as powerful as statistical query (SQ) algorithms in the sense of Kearns (J. ACM 1998), up to polynomial factors. This mission formalizes one direction of that equivalence: every local algorithm run on i.i.d. data can be simulated by an SQ algorithm.

This is the fourth of five missions on the paper. Mission III formalizes the converse direction (Theorem 5.7). All theorem numbers refer to arXiv:0803.0924v3.

Setting

A database is $z=(z_1,\dots,z_n)\in D^n$. Here its entries are drawn i.i.d. from a probability distribution $P$ on $D$.

• An $\varepsilon$-local randomizer (Definition 5.1) is a randomized map $R:D\to W$ to a discrete set $W$ such that $\Pr[R(u)=w]\le e^{\varepsilon}\Pr[R(u')=w]$ for all $u,u'\in D$ and $w\in W$.
• An $\varepsilon$-local algorithm $A$ making $t$ queries (Definitions 5.2, 5.3) sees the database only through an LR oracle. At its $k$-th call it names an index $i_k$ and an $\varepsilon_k$-local randomizer $R_k$, both possibly depending on its earlier answers, and receives a fresh sample of $R_k(z_{i_k})$. For each index $i$ the budgets of the calls on $i$ sum to at most $\varepsilon$. $A$ is noninteractive if its calls do not depend on earlier answers. Its output is a function of the $t$ answers. Its output distribution is taken over $z\sim P^n$ and the randomizers' coins.
• An SQ oracle for $P$ (Definition 5.4) answers a query $(g,\tau)$, with $g:D\to[-1,1]$ and tolerance $\tau$, with any number $v$ such that $|v-\mathbb E_{u\sim P}[g(u)]|\le\tau$. It may choose its answers adversarially and adaptively.
• An SQ algorithm $B$ (Definition 5.5) accesses $P$ only through such an oracle. It may use its own coins, and the number of queries it makes may be random and unbounded.
• The statistical difference of two distributions on a discrete space (p. 8) is $\max_S|\mu(S)-\nu(S)|$.

Formalization targets

Goal: Lemma 5.8 (p. 21)

There is an absolute constant $C$ such that for every $\varepsilon$-local algorithm $A$ making $t$ queries there is an SQ algorithm $B$ with the following properties against every distribution $P$ and every valid oracle:

$$\tau=\frac{\beta}{3e^{2\varepsilon}t},\qquad \mathbb E[\#\text{queries of }B]\le C\,t\,e^{\varepsilon},\qquad \mathrm{SD}\bigl(B,\ A(z),\ z\sim P^n\bigr)\le\beta .$$

The constant $C$ is the paper's $O(\cdot)$. The tolerance is the proof's own choice.

Milestones

1. Display (5) (p. 22): a single query estimates $p(w)=\Pr_{z_i\sim P}[R(z_i)=w]$ within a factor $1\pm\beta/(3t)$, whatever valid answer the oracle gives.
2. One rejection-sampling iteration (p. 23): every iteration terminates with probability at least $\frac{1-\varphi}{1+\varphi}e^{-\varepsilon}$. Conditioned on terminating, it outputs $w$ with probability in $(1\pm3\varphi)p(w)$.
3. The interactive estimate (p. 24): two queries estimate the conditional probability of the next answer given earlier answers on the same entry, within a factor $1\pm3e^{2\varepsilon}\tau$.
4. Claim 5.9 (p. 22): the noninteractive case, with the explicit bound $2t\,e^{\varepsilon}$ on the expected number of queries.

Significance

The result. Lemma 5.8, combined with Theorem 5.7, shows that a concept class is learnable by a locally private algorithm if and only if it is learnable with statistical queries (Theorem 5.14). Every SQ lower bound therefore becomes a lower bound for local privacy. For instance, parity functions are privately learnable by a centralized algorithm (Theorem 4.4) but not by a local one, because parities need exponentially many statistical queries (Corollary 5.15, which also uses the SQ lower bound of Blum et al., STOC 1994).

Formalizing it. The result is proved on paper. As far as we know it has no machine-checked proof. The paper's proof is a few paragraphs and leaves the model implicit: what an SQ algorithm with a random number of queries is, how an adversarial oracle interacts with it, and in what sense the per-randomizer errors add up over $t$ adaptively chosen randomizers. The formal statement makes each of these explicit. The milestones isolate the estimates the proof uses, so they can be proved independently of the composition argument.

Difficulty

The estimates in the milestones are elementary inequalities. The difficulty is in the goal. First, the oracle's answers, and therefore the estimates $\tilde p(w)$, change from iteration to iteration, so the simulated distribution is not a fixed rejection sampler: the output law must be controlled iteration by iteration against an adversary. Second, the SQ algorithm has no bound on its number of steps. Its output law is a limit over an unbounded run, and its query count is an expectation that is finite only because every iteration terminates with probability bounded away from zero. Third, in the interactive case the randomizers applied to one entry are correlated through the entry. The simulation must sample from the conditional law given earlier answers on that entry, while the errors of all $t$ steps combine along adaptively chosen histories.

Formalization scope

• Local randomizers have discrete output: R u : PMF W. The simulation uses the point probabilities $\Pr[R(z_i)=w]$. Every map $u\mapsto\Pr[R(u)=w]$ is required to be measurable.
• A local algorithm makes exactly $t$ calls. Its index, randomizer and budget at call $k$ are functions of the earlier answers. The budget is required along every answer sequence. Its own coins are calls to $0$-local randomizers.
• An SQ algorithm is a state machine with a random start, random transitions depending on the answer, and an output on stopping. Its output law is a sub-probability mass function. Its expected query count lies in $[0,\infty]$ and counts every query, including those in rejected iterations.
• The oracle is an arbitrary deterministic function of the whole state trajectory, constrained only by Definition 5.4. The conclusions must hold for every valid oracle, not for the exact-mean oracle alone.
• $B$ is quantified before $P$ and sees $P$ only through answers, and every query of $B$ is a measurable $[-1,1]$-valued function with tolerance exactly $\beta/(3e^{2\varepsilon}t)$. Without these two constraints the statement would be trivial: $B$ could hard-code $P$, or rescale a query to shrink its effective tolerance.
• The constant $C$ is quantified outside every other object.
• The implicit hypotheses $\varepsilon>0$ (the queries divide by $e^{\varepsilon}-e^{-\varepsilon}$), $0<\beta\le1$ and $t\ge1$ (so that $\varphi=\beta/(3t)\le1/3$ and $\tau$ is defined) are stated. The paper's reference input $\mathbf 0$ is an arbitrary point $u_0\in D$.
• Claim 5.9 states "$t\cdot e^{\varepsilon}$ queries". Its proof gives at most $2t\,e^{\varepsilon}$, which is the bound stated.
• The paper's refinement "noninteractive $A$ yields nonadaptive $B$" is not formalized. The simulation decides from each answer whether to stop, and so which randomizer the next query belongs to. It therefore does not prepare its queries before receiving answers in the sense of Definition 5.5. The goal is the adaptive statement for all local algorithms, which contains the noninteractive case. Claim 5.10, whose statement coincides with this goal, is represented by its estimate (milestone 3) rather than restated.
• The statistical difference is valued in $[0,\infty]$, which avoids junk values of a real supremum.

Reusable beyond this mission: the SQ-algorithm state machine with expected query count, the statistical difference of sub-probability mass functions, and the model of interactive local algorithms. Welcome contributions include proofs of the estimate milestones, a general lemma bounding the statistical difference of sequentially composed approximate samplers, and the termination and expected-runtime analysis of rejection sampling with varying acceptance probabilities.

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; cited from arXiv:0803.0924v3. https://arxiv.org/abs/0803.0924 · https://doi.org/10.1137/090756090
• M. Kearns, Efficient noise-tolerant learning from statistical queries, J. ACM 45(6) (1998) 983–1006. https://doi.org/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, 253–262. https://doi.org/10.1145/195058.195147
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating noise to sensitivity in private data analysis, TCC 2006. https://doi.org/10.1007/11681878_14
• S. L. Warner, Randomized response: a survey technique for eliminating evasive answer bias, J. Amer. Statist. Assoc. 60 (1965) 63–69. https://doi.org/10.1080/01621459.1965.10480775

Motivation

The learning with errors (LWE) problem underlies much of post-quantum public-key cryptography, and its hardness rests on Regev's reduction from worst-case lattice problems to LWE (Regev, J. ACM 2009). Every step of that reduction is calibrated by the smoothing parameter $\eta_\epsilon(L)$ of Micciancio and Regev (SIAM J. Comput. 2007): the Gaussian width above which a discrete Gaussian on a lattice behaves like a continuous one. The approximation factors of the reduction are stated in terms of $\eta_\epsilon(L)$, and they are converted into factors for the standard lattice problems (GapSVP, SIVP) by comparing $\eta_\epsilon(L)$ with the successive minima of $L$ and of its dual.

Upper bounds on $\eta_\epsilon(L)$ (Lemmas 2.11 and 2.12 of the paper, from Micciancio–Regev) say the smoothing parameter is not too large. Claim 2.13 is the matching lower bound: the smoothing parameter cannot be much smaller than $1/\lambda_1(L^*)$, and hence than $\lambda_n(L)/n$. The second comparison goes through Banaszczyk's transference theorem (Banaszczyk, Math. Ann. 296 (1993)), $1 \le \lambda_1(L)\lambda_n(L^*) \le n$, which relates the geometry of a lattice to that of its dual.

This mission formalizes Claim 2.13 from the published J. ACM article (Article 34, 2009), together with the steps of its proof and the transference theorem it cites. The paper's main theorem, Theorem 3.1, is a quantum reduction about efficient algorithms; it is outside this series of missions.

Setting

Work in $\mathbb{R}^n$, $n \ge 1$, with the Euclidean norm $\|\cdot\|$ and inner product $\langle\cdot,\cdot\rangle$. A lattice $L \subset \mathbb{R}^n$ is the set of integer combinations of $n$ linearly independent vectors. Its dual is

$$L^* = \{y \in \mathbb{R}^n : \langle x, y\rangle \in \mathbb{Z} \text{ for all } x \in L\},$$

again a lattice, with $(L^*)^* = L$.

The successive minima used here are $\lambda_1(L)$, the length of a shortest nonzero vector of $L$, and $\lambda_n(L)$, the least $r$ such that $L$ contains $n$ linearly independent vectors of length at most $r$.

For $s > 0$ the Gaussian function is $\rho_s(x) = \exp(-\pi\|x/s\|^2)$ (Eq. (4)), and for a countable set $A$, $\rho_s(A) = \sum_{x\in A}\rho_s(x)$. In particular $\rho_{1/s}(y) = \exp(-\pi s^2\|y\|^2)$.

For $\epsilon > 0$ the smoothing parameter $\eta_\epsilon(L)$ is the smallest $s$ such that $\rho_{1/s}(L^*\setminus\{0\}) \le \epsilon$ (Definition 2.10).

Formalization targets

Goal: Claim 2.13 (p. 34:20)

For any lattice $L$ and any $\epsilon > 0$,

$$\eta_\epsilon(L) \;\ge\; \sqrt{\frac{\ln 1/\epsilon}{\pi}}\cdot\frac{1}{\lambda_1(L^*)} \;\ge\; \sqrt{\frac{\ln 1/\epsilon}{\pi}}\cdot\frac{\lambda_n(L)}{n}.$$

Both inequalities of the chain are part of the goal. The asymptotic "In particular" sentence of the claim ($\epsilon(n) = o(1)$, large enough $n$) is not.

Milestones, in attack order

1. The remark after Definition 2.10 (p. 34:19). The map $s \mapsto \rho_{1/s}(L^*\setminus\{0\})$ is continuous and strictly decreasing on $(0,\infty)$, tends to $\infty$ as $s \to 0$ and to $0$ as $s \to \infty$, and $\epsilon \mapsto \eta_\epsilon(L)$ is its inverse; in particular $\rho_{1/\eta_\epsilon(L)}(L^*\setminus\{0\}) = \epsilon$.
2. The display of the proof of Claim 2.13 (p. 34:20). For $s = \eta_\epsilon(L)$ and $v \in L^*$ of length $\lambda_1(L^*)$,

$$\epsilon = \rho_{1/s}(L^*\setminus\{0\}) \ge \rho_{1/s}(v) = \exp\bigl(-\pi(s\lambda_1(L^*))^2\bigr).$$

3. Lemma 2.3, Banaszczyk's transference theorem (p. 34:18). For any $n$-dimensional lattice $L$,

$$1 \le \lambda_1(L)\cdot\lambda_n(L^*) \le n .$$

Significance

The result. Claim 2.13 shows that the smoothing parameter for a negligible $\epsilon$ exceeds every constant multiple of $1/\lambda_1(L^*)$ and of $\lambda_n(L)/n$. Together with the upper bound $\eta_\epsilon(L) \le \sqrt{\ln(2n(1+1/\epsilon))/\pi}\,\lambda_n(L)$ of Lemma 2.12, it locates $\eta_\epsilon(L)$ within a polynomial factor of $\lambda_n(L)$. This is what lets the reduction's guarantees, phrased in $\eta_\epsilon(L)$, be read as approximation factors for SIVP and GapSVP. The transference theorem is used throughout the geometry of numbers and in lattice-based cryptography to pass between a lattice and its dual.

Formalizing it. The claim and its proof are classical and short, but neither is machine-checked. The mission produces formal definitions of the dual lattice, the successive minima $\lambda_1$, $\lambda_n$ and the smoothing parameter on EuclideanSpace ℝ (Fin n), a proof that Definition 2.10 is well posed, and a statement of Banaszczyk's transference theorem. The upper bound of the transference theorem is a substantial result in its own right (the paper cites it without proof), and a formal proof of it would be reusable well beyond this mission.

Difficulty

The first inequality of the goal is elementary once the smoothing parameter is known to be attained, with $\rho_{1/\eta}(L^*\setminus\{0\}) = \epsilon$ exactly. That step is not a formality: it needs the continuity and strict monotonicity of an infinite lattice sum in the scale parameter, and the fact that a shortest nonzero dual vector exists, both of which rest on the discreteness of $L^*$.

The second inequality is a single line in the paper, "by Lemma 2.3", but it uses the upper bound of Banaszczyk's theorem, applied to the dual lattice. The easy lower bound $1 \le \lambda_1(L)\lambda_n(L^*)$ does not suffice, and a Minkowski-type argument gives a bound worse than linear in $n$. Applying the lemma to $L^*$ also needs $L^*$ to be a lattice with dual $L$.

Formalization scope

• $\mathbb{R}^n$ is EuclideanSpace ℝ (Fin n). A lattice is L : Submodule ℤ _ with [DiscreteTopology L] [IsZLattice ℝ L]. The dual is LinearMap.BilinForm.dualSubmodule (innerₗ _) L.
• Every theorem assumes $0 < n$: the paper's lattices are $n$-dimensional with $n \ge 1$. This is the only added hypothesis.
• Gaussian sums are real tsums. They are summable over discrete subgroups, so no summability hypotheses are added.
• $\eta_\epsilon(L)$, $\lambda_1$ and $\lambda_n$ are infima (sInf). The paper's "smallest" is the attainment proved in milestones 1 and 2, not built into the definition. $\lambda_1$ and $\lambda_n$ are defined for every $\mathbb{Z}$-submodule, so they apply to $L^*$ without extra instances.
• For $\epsilon \ge 1$ the paper's $\sqrt{\ln(1/\epsilon)/\pi}$ is the square root of a non-positive number; Lean's Real.sqrt gives $0$ there and the goal reduces to true statements. No hypothesis $\epsilon < 1$ is added, since the page says "any $\epsilon > 0$".
• The goal is a conjunction of both inequalities of the chain, not only the outer comparison $\eta_\epsilon(L) \ge \sqrt{\ln(1/\epsilon)/\pi}\,\lambda_n(L)/n$, which would be weaker. Lemma 2.3 states both bounds; stating only the easy lower bound would leave the goal's second inequality without its milestone.
• No printed statement needed correction.

Contributions welcome: the attainment of $\lambda_1$ and $\lambda_n$ for IsZLattice (and for the dual), the identity $(L^*)^* = L$ in this setting, continuity and monotonicity of Gaussian lattice sums, and above all Banaszczyk's transference theorem.

Selected references

• O. Regev, On Lattices, Learning with Errors, Random Linear Codes, and Cryptography, J. ACM 56(6), Article 34, 2009. https://doi.org/10.1145/1568318.1568324
• W. Banaszczyk, New bounds in some transference theorems in the geometry of numbers, Math. Ann. 296, 625–635, 1993. https://doi.org/10.1007/BF01445125
• D. Micciancio, O. Regev, Worst-case to average-case reductions based on Gaussian measures, SIAM J. Comput. 37(1), 267–302, 2007. https://doi.org/10.1137/S0097539705447360

Motivation

Randomized load balancing asks how much a dispatcher gains from a little information. In the supermarket model, jobs arrive at $n$ servers and each job inspects a few servers chosen at random before joining one. With one random choice every server is an independent M/M/1 queue, and the expected time a job spends in the system is $1/(1-\lambda)$ at load $\lambda$. With two choices it is exponentially smaller as $\lambda \to 1^-$. This "power of two choices" underlies the design of distributed schedulers, hashing schemes and server farms, where querying every server is too expensive but querying two is cheap.

Timeline:

• 1994/1999. Azar, Broder, Karlin and Upfal proved the static version, balanced allocations: throwing $n$ balls into $n$ bins with $d \ge 2$ choices per ball gives a maximum load of $\log\log n/\log d + O(1)$ w.h.p., against $\Theta(\log n/\log\log n)$ for one choice (SIAM J. Comput. 1999).
• 1996. Vvedenskaya, Dobrushin and Karpelevich derived the dynamic limiting equations for $d = 2$ and showed convergence of their trajectories to the fixed point, without a rate (Problems of Information Transmission 32(1), 1996).
• 1996/2001. Mitzenmacher, independently, introduced the limiting system for general $d$, proved doubly exponential tails along every trajectory and exponential convergence to the fixed point in a weighted $L_1$ potential, and derived the limiting expected time $T_d(\lambda)$ (IEEE TPDS 2001). This mission formalizes Section 2 of that paper.

Setting

Customers arrive as a Poisson stream of rate $\lambda n$, $0<\lambda<1$, at $n$ FIFO servers. Each customer chooses $d$ servers independently and uniformly at random with replacement and joins the one holding the fewest customers; service times are exponential with mean $1$. Let $s_i(t)$ be the fraction of servers holding at least $i$ customers at time $t$.

A state is a sequence $s = (s_0, s_1, s_2, \dots)$ of reals with $s_0 = 1$, $s_i \ge 0$ and $s_0 \ge s_1 \ge s_2 \ge \cdots$. The empty state has $s_0 = 1$ and $s_i = 0$ for $i \ge 1$. As $n \to \infty$ the tails follow the limiting system

$$\frac{ds_i}{dt} = \lambda\,(s_{i-1}^d - s_i^d) - (s_i - s_{i+1}) \quad (i \ge 1), \qquad s_0 = 1. \tag{1}$$

A trajectory is a map $t \mapsto s(t)$, $t \ge 0$, whose values are states and whose coordinates satisfy (1) (from the right at $t = 0$). Throughout, $d \ge 2$ is an integer.

The fixed point is $\pi_i = \lambda^{(d^i - 1)/(d - 1)}$, so $\pi_0 = 1$, $\pi_1 = \lambda$, $\pi_2 = \lambda^{1+d}$. A customer arriving in state $s$ becomes the $i$-th customer of its queue with probability $s_{i-1}^d - s_i^d$ and then waits for $i$ services, so the expected time it spends in the system is

$$E(s) = \sum_{i=1}^{\infty} i\,(s_{i-1}^d - s_i^d).$$

The target constant is

$$T_d(\lambda) = \sum_{i=1}^{\infty} \lambda^{\frac{d^i - d}{d-1}}.$$

Formalization targets

Goal: Corollary 2

For $d \ge 2$ and $0 < \lambda < 1$, $T_d(\lambda) < \infty$, and:

$$\text{if } s_j(0) = 0 \text{ for some } j, \text{ then } E(s(t)) \xrightarrow[t\to\infty]{} T_d(\lambda);\qquad \text{if } s(0) \text{ is empty, then } E(s(t)) \le T_d(\lambda) \ \ \forall t \ge 0.$$

The hypothesis $s_j(0) = 0$ holds for every initial state that comes from a finite system.

Milestones, in the order the proof uses them

• Lemma 2. $\pi$ is the unique fixed point of (1) with $\sum_{i\ge1} s_i < \infty$.
• Theorem 2. If $s_j(0) = 0$ for some $j$, there are constants $N \ge 1$, $0<\alpha<1$, $\beta>1$, $\gamma>0$, independent of $t$, with $s_i(t) \le \gamma\,\alpha^{\beta^i}$ for all $i \ge N$, $t \ge 0$. From the empty state, $s_i(t) \le \pi_i$ for all $i$ and $t \ge 0$.
• Theorem 3. There are weights $w_i \ge 1$ such that $\Phi(t) = \sum_{i\ge1} w_i |s_i(t) - \pi_i|$ satisfies $\Phi(t) \le c_0 e^{-\delta t}$ ($\delta > 0$) whenever $\Phi(0) < \infty$, and in particular whenever $s_j(0) = 0$ for some $j$.
• Corollary 1. Under the conditions of Theorem 3 (weights $w_i \ge 1$ fixed before the trajectory, with $\Phi(0) < \infty$, or $s_j(0) = 0$ for some $j$), $\sum_{i\ge1} |s_i(t) - \pi_i| \le c_0 e^{-\delta t}$.
• Proof of Corollary 2, display. $\sum_{i\ge1} i(s_{i-1}^d - s_i^d) = \sum_{i\ge0} s_i^d$ for a state with $s_i \to 0$.
• Lemma 4. The drift of (1) is Lipschitz in $\ell^1$ on states, with constant $2 + 2d\lambda$.

Significance

The comparison $T_1(\lambda) = 1/(1-\lambda)$ against $T_d(\lambda)$ is the quantitative content of the power of two choices: the companion mission shows $T_d(\lambda)/\log T_1(\lambda) \to 1/\log d$ as $\lambda \to 1^-$, an exponential improvement. Corollary 2 is what connects that number to the dynamics: it says the fixed point's expected time is actually reached from realistic initial states, and is an upper bound from an empty start. Theorem 2's comparison argument and Theorem 3's weighted potential are reused across the mean-field analysis of load-balancing variants (threshold policies, heterogeneous servers, work stealing), so the formal statements here are templates for that literature.

All results are proved in the paper (Theorem 3's proof is written out for $d = 2$ with a remark that it extends). None has a machine-checked proof that we know of. The work is formalizing the known arguments for all $d \ge 2$, including the parts the paper delegates to a citation: quasimonotone comparison for countable ODE systems in Theorem 2, and the upper right Dini derivative handling of $|\epsilon_i|$ in Theorem 3.

Difficulty

The system is infinite-dimensional, so standard finite-dimensional ODE comparison and Lyapunov theorems do not apply as stated. Theorem 2 rests on a monotonicity property (raising the initial tails raises them for all time) that the paper justifies by a coupling intuition and a citation to a comparison theorem for quasimonotone systems; that theorem must be supplied for $\ell^\infty$-bounded countable systems. The plain $L_1$ distance is nonincreasing along trajectories but does not decay exponentially by a direct estimate; the weights $w_i$ must be built so that every coordinate's contribution to $d\Phi/dt$ is dominated by $-\delta w_i |\epsilon_i|$, while staying geometrically bounded so that $\Phi(0) < \infty$ under the doubly exponential tails of Theorem 2. Exchanging $t \to \infty$ with the infinite sum defining $E$ needs uniform tail control, which is again Theorem 2.

Formalization scope

• Namespace PowerTwoChoices.Limit; λ is lam : ℝ, $d : ℕ$ with $2 \le d$, $0 < \lambda < 1$ in every theorem.
• A state is x : ℕ → ℝ with x 0 = 1, nonnegative and antitone. A trajectory is s : ℝ → ℕ → ℝ, a state for every $t \ge 0$, with HasDerivWithinAt on Set.Ici 0 for each coordinate $i \ge 1$: right derivative at $t = 0$, two-sided for $t > 0$.
• Exponents are natural numbers: $\pi_i = \lambda^{\sum_{k<i} d^k}$, and $T_d$'s $i$-th term is $\lambda^{\sum_{1\le k<i} d^k}$.
• $\Phi$, the $L_1$ distance, $E$ and $T_d$ are sums in $[0,\infty]$, so a divergent series is $\infty$, never a default $0$. "Converges exponentially" (Definition 2) means $\Phi(t) \le c_0 e^{-\delta t}$ for all $t \ge 0$ with real $c_0$ and $\delta > 0$; $\delta$ may depend on the trajectory. The paper's $d(t)$ is renamed l1Dist.
• Time is real and $t \to \infty$ is Filter.atTop.
• Every theorem quantifies over trajectories; existence of a trajectory from a given state (Picard iteration, cited by the paper) is not part of the mission. The class is nonempty: the constant trajectory at $\pi$ is one.
• Ruled out: summing $E$ or $T_d$ as a real tsum (a divergent series would make the upper bound free and the limit attainable by a junk $0$), dropping the summability condition in Lemma 2 ($(1,1,\dots)$ is also a fixed point), choosing Theorem 3's weights after the trajectory, and stating anything for $d = 2$ only.
• Needed infrastructure: comparison principles for quasimonotone countable ODE systems, Dini-derivative Grönwall estimates, and interchange of limits and $\ell^1$ sums. All of these are reusable beyond this mission, and contributions of such lemmas as separate theorems are welcome.

Selected references

• M. Mitzenmacher, The Power of Two Choices in Randomized Load Balancing, IEEE Transactions on Parallel and Distributed Systems 12(10), 2001, pp. 1094–1104. https://doi.org/10.1109/71.963420
• Y. Azar, A. Z. Broder, A. R. Karlin, E. Upfal, Balanced Allocations, SIAM Journal on Computing 29(1), 1999, pp. 180–200. https://doi.org/10.1137/S0097539795288490
• N. D. Vvedenskaya, R. L. Dobrushin, F. I. Karpelevich, Queueing System with Selection of the Shortest of Two Queues: An Asymptotic Approach, Problems of Information Transmission 32(1), 1996, pp. 15–27.
• T. G. Kurtz, Approximation of Population Processes, SIAM, 1981. https://doi.org/10.1137/1.9781611970333