Theoretical Computer Science

Motivation

Many graph algorithms run in time proportional to the number of edges. A sparsifier of a weighted graph $G$ is a graph $H$ on the same vertices with far fewer edges that approximates $G$ for the purpose at hand, so that the algorithm can be run on $H$ instead. Benczúr and Karger (1996) showed that every graph has a sparsifier with $O(n\log n/\varepsilon^2)$ edges preserving the weight of every cut up to a factor $1\pm\varepsilon$. Spielman and Teng (2004) introduced the stronger spectral notion, in which the Laplacian quadratic form is preserved for every real vector, not only for cut indicators; their sparsifiers had $O(n\log^c n)$ edges for a large constant $c$ and were the first step of their nearly-linear-time solvers for symmetric diagonally dominant linear systems.

Spielman and Srivastava (arXiv:0803.0929, STOC 2008, SIAM J. Comput. 2011) proved that independent sampling of $O(n\log n/\varepsilon^2)$ edges, each edge with probability proportional to its weight times its effective resistance, yields a spectral sparsifier. The result improved both earlier bounds, replaced a recursive partitioning construction by a one-line sampling rule, and made effective resistance a standard tool in graph algorithms. Batson, Spielman and Srivastava (arXiv:0808.0163) later obtained $O(n/\varepsilon^2)$ edges deterministically, by a slower method built on the same matrix $\Pi$.

Setting

Let $G=(V,E,w)$ be a connected weighted undirected graph with $n=|V|$ vertices, $m=|E|$ edges and weights $w_e>0$. Orient every edge arbitrarily, so that it has a head and a tail (distinct vertices).

• The incidence matrix $B\in\mathbb R^{m\times n}$ has $B(e,v)=1$ if $v$ is the head of $e$, $-1$ if $v$ is its tail, and $0$ otherwise; $b_e$ denotes its row for $e$. $W$ is the diagonal $m\times m$ matrix with $W(e,e)=w_e$.
• The Laplacian is $L=B^{\mathsf T}WB$, with quadratic form $x^{\mathsf T}Lx=\sum_e w_e\,(x(\mathrm{head}\,e)-x(\mathrm{tail}\,e))^2$.
• $L^{+}$ is the Moore–Penrose pseudoinverse of $L$: if $L=\sum_{i=1}^{n-1}\lambda_iu_iu_i^{\mathsf T}$ over its nonzero eigenvalues, then $L^{+}=\sum_{i=1}^{n-1}\lambda_i^{-1}u_iu_i^{\mathsf T}$.
• The effective resistance of the edge $e$ is $R_e=b_eL^{+}b_e^{\mathsf T}$: the potential difference across $e$ when a unit current enters at one end and leaves at the other, the edges being resistors of conductance $w_e$.
• $\Pi=W^{1/2}BL^{+}B^{\mathsf T}W^{1/2}$ is an $m\times m$ matrix with $\Pi(e,e)=w_eR_e$.
• Sparsify$(G,q)$ draws $q$ edges independently with replacement, the edge $e$ with probability $p_e=w_eR_e/\sum_f w_fR_f$, and gives $e$ the weight $w_e/(qp_e)$ for each time it is drawn. Its output $H$ has Laplacian $\tilde L=B^{\mathsf T}W^{1/2}SW^{1/2}B$, where $S$ is the random diagonal matrix with $S(e,e)=\#\{\text{draws of }e\}/(qp_e)$.

Formalization targets

Goal: Theorem 1

There are an absolute constant $C$ and a threshold $N_0$ such that, for every $n\ge N_0$, every connected weighted graph on $n$ vertices and every $1/\sqrt n<\varepsilon\le1$, with $q=\lceil 9C^2n\log n/\varepsilon^2\rceil$, with probability at least $1/2$

$$\forall x\in\mathbb R^n:\qquad (1-\varepsilon)\,x^{\mathsf T}Lx\;\le\;x^{\mathsf T}\tilde Lx\;\le\;(1+\varepsilon)\,x^{\mathsf T}Lx .$$

The constant $C$ is left unfixed; the statement asserts the shape $q=O(n\log n/\varepsilon^2)$ with the paper's explicit dependence on $C$.

Milestones

1. Lemma 3 (four parts): $\Pi$ is an orthogonal projection; $\operatorname{im}\Pi=\operatorname{im}W^{1/2}B$; the eigenvalues of $\Pi$ are $1$ with multiplicity $n-1$ and $0$ with multiplicity $m-n+1$; $\Pi(e,e)=\|\Pi(\cdot,e)\|^2$.
2. Lemma 4: for a nonnegative diagonal $S$, $\|\Pi S\Pi-\Pi\Pi\|_2\le\varepsilon$ implies $(1-\varepsilon)x^{\mathsf T}Lx\le x^{\mathsf T}B^{\mathsf T}W^{1/2}SW^{1/2}Bx\le(1+\varepsilon)x^{\mathsf T}Lx$ for all $x$.
3. Lemma 5 (Rudelson–Vershynin): for independent samples $y_1,\dots,y_q$ of a random vector with $\|y\|_2\le M$ and $\|\mathbb E\,yy^{\mathsf T}\|_2\le1$, and $q\ge2$,

$$\mathbb E\Big\|\frac1q\sum_{j=1}^q y_jy_j^{\mathsf T}-\mathbb E\,yy^{\mathsf T}\Big\|_2\le CM\sqrt{\frac{\log q}{q}}\quad\text{whenever the right side is }<1.$$

Significance

Theorem 1 says that every weighted graph is spectrally approximated by a reweighted subgraph with $O(n\log n/\varepsilon^2)$ edges. A spectral approximation preserves cut weights, the eigenvalues of the Laplacian up to $1\pm\varepsilon$, effective resistances, and the condition number of $L$ as a preconditioner, so any algorithm whose output depends on these quantities can run on $H$. Combined with fast approximate computation of effective resistances (the second mission of this series), it gives a nearly-linear-time construction, and it is the sampling step used in Laplacian solvers, in sparsification of sums of rank-one matrices, and in leverage-score sampling for regression, where $w_eR_e$ is exactly the statistical leverage of a row.

The result is proved in the paper; to our knowledge no machine-checked proof exists. This mission formalizes the statement and the paper's proof structure: the linear algebra of $\Pi$ (Lemma 3), the deterministic reduction from quadratic forms to a spectral-norm bound (Lemma 4), and the matrix concentration inequality (Lemma 5), which is the substantive analytic input and is itself a reusable result about sums of independent rank-one matrices.

Difficulty

The deterministic part is linear algebra over the pseudoinverse. The obstacle is concentration: the expected Laplacian of $H$ equals $L$, but bounding the deviation uniformly over all $x\in\mathbb R^n$ is a statement about the spectral norm of a random matrix, and a union bound over a net of directions costs a factor of $n$ in the sample count rather than $\log n$. Scalar Chernoff bounds per cut, which suffice for cut sparsifiers, do not give the spectral statement. Lemma 5 is the matrix inequality that removes this loss, and no inequality of this kind (a concentration bound for the spectral norm of a sum of independent random matrices) is in Mathlib.

Formalization scope

All declarations sit in the namespace EffResSparsify.Sampling.

• Graphs. A structure WGraph V E with orientation maps head, tail : E → V, weights w : E → ℝ, and the fields head e ≠ tail e (no loops) and 0 < w e. Parallel edges are allowed; nothing in §3 uses simplicity. Connectivity is a separate hypothesis on the underlying simple graph and includes $V\ne\emptyset$. In Theorem 1 the vertex type is Fin n; the edge type is an arbitrary finite type.
• Pseudoinverse. $L^{+}$ is the matrix of the published Moore–Penrose pseudoinverse HarmonicGames.Decomposition.pinv of $x\mapsto Lx$ on Euclidean $\mathbb R^V$; it equals the spectral formula above and is the gauge-fixed inverse, never "some solution of $Lx=y$".
• Sampling. $p_e$ is defined as $w_eR_e/\sum_f w_fR_f$; the identity $\sum_f w_fR_f=n-1$ is part of the proof. An outcome of Sparsify is a sequence in $E^q$ with probability $\prod_i p_{s_i}$, and probabilities and expectations are finite sums over $E^q$, with no measure theory.
• Norms and logarithms. $\|\cdot\|_2$ is the $\ell_2$ operator norm on matrices (Matrix.Norms.L2Operator); vector norms in Lemma 5 are Euclidean; $\log$ is natural (the base is absorbed into $C$).
• Constants. In Theorem 1, $\exists C>0,\ \exists N_0,\ \forall n\ge N_0$ precede the graph and $\varepsilon$; the sample count is $\lceil 9C^2n\log n/\varepsilon^2\rceil$, rounded up because the printed value is not an integer. In Lemma 5, $\exists C>0$ precedes the dimension, the distribution, $M$ and $q$.
• Corrected statement. Lemma 5 as printed, with right side $\min(CM\sqrt{\log q/q},1)$, is false (at $q=1$ the bound is $0$). The formal milestone is Rudelson and Vershynin's own Theorem 3.1: $q\ge2$, and the bound $a=CM\sqrt{\log q/q}$ holds when $a<1$. It is stated for finitely supported distributions, which is all Theorem 1 uses. Theorem 1 applies it with $a\le\varepsilon/2$, so the correction does not affect the goal.
• Not a trivialization. Theorem 1 does not take Lemma 5, a bound on $\mathbb E\|\Pi S\Pi-\Pi\|_2$, or a free sample count as a hypothesis; a statement with any of these, or with "$\exists q$" in place of $\lceil 9C^2n\log n/\varepsilon^2\rceil$, is a different theorem.

Reusable beyond this mission: the weighted Laplacian with its pseudoinverse and effective resistances, and Lemma 5, which applies to any sampling scheme for sums of rank-one matrices (leverage-score sampling, column subset selection). Contributions toward a matrix Chernoff or Rudelson-type inequality in Mathlib are welcome.

Selected references

• D. A. Spielman, N. Srivastava, Graph Sparsification by Effective Resistances, arXiv:0803.0929v4, 2009; SIAM J. Comput. 40(6), 2011. https://arxiv.org/abs/0803.0929, https://doi.org/10.1137/080734029
• M. Rudelson, R. Vershynin, Sampling from large matrices: an approach through geometric functional analysis, J. ACM 54(4), 2007. https://doi.org/10.1145/1255443.1255449
• M. Rudelson, Random vectors in the isotropic position, J. Funct. Anal. 164(1), 1999. https://doi.org/10.1006/jfan.1998.3384
• A. A. Benczúr, D. R. Karger, Approximating s-t minimum cuts in Õ(n²) time, STOC 1996. https://doi.org/10.1145/237814.237827
• D. A. Spielman, S.-H. Teng, Spectral sparsification of graphs, SIAM J. Comput. 40(4), 2011 (arXiv:0808.4134). https://arxiv.org/abs/0808.4134
• J. Batson, D. A. Spielman, N. Srivastava, Twice-Ramanujan sparsifiers, SIAM J. Comput. 41(6), 2012 (arXiv:0808.0163). https://arxiv.org/abs/0808.0163

Motivation

The effective resistance between two vertices of a weighted graph is the voltage difference that appears between them when the graph is viewed as an electrical network, edge weights being conductances, and one unit of current is injected at one vertex and extracted at the other. Effective resistances drive the spectral sparsification algorithm of Spielman and Srivastava (arXiv:0803.0929): sampling each edge with probability proportional to its weight times its effective resistance yields a sparse graph whose Laplacian approximates the original one. They are also used as a distance on graphs in the analysis of social and small-world networks, where they reflect how many short paths connect two vertices.

Computing every effective resistance exactly requires the pseudoinverse of the Laplacian, which costs far more than the size of the graph. Section 4 of the paper shows that all of them can be approximated in nearly linear time: a random projection compresses the relevant vectors to $O(\log n)$ dimensions, and the projected vectors are obtained from $O(\log n)$ calls to a fast approximate Laplacian solver (Spielman–Teng). This mission formalizes the deterministic statement that makes this procedure correct, Lemma 9: approximate solves, at a stated accuracy, do not destroy the approximation that the random projection provides.

Setting

Let $G=(V,E,w)$ be a connected, simple, weighted undirected graph with $n=|V|$ vertices, edge set $E$ and edge weights $w_e>0$. Orient every edge arbitrarily, so that it has a head and a tail. The signed incidence matrix $B\in\mathbb R^{E\times V}$ has $B(e,v)=1$ if $v$ is the head of $e$, $-1$ if $v$ is its tail, and $0$ otherwise. With $W$ the diagonal matrix of weights, the Laplacian is $L=B^{\mathsf T}WB$, a symmetric positive semidefinite matrix whose kernel is spanned by the all-ones vector when $G$ is connected. Its Moore–Penrose pseudoinverse is $L^+=\sum_{\lambda_i\neq 0}\lambda_i^{-1}u_iu_i^{\mathsf T}$, where $u_i$ are orthonormal eigenvectors of $L$ with nonzero eigenvalues $\lambda_i$.

For a vertex $u$ let $\chi_u$ be its indicator vector. The effective resistance between $u$ and $v$ is

$$R_{uv}=(\chi_u-\chi_v)^{\mathsf T}L^+(\chi_u-\chi_v),$$

and $R_e=R_{ab}$ for an edge $e$ with endpoints $a,b$. The $L$-norm of $y\in\mathbb R^V$ is $\|y\|_L=\sqrt{y^{\mathsf T}Ly}$. Let $w_{\min}$ and $w_{\max}$ be the smallest and largest edge weights.

A resistance sketch is a $k\times n$ matrix $Z$ (columns indexed by $V$) with

$$(1-\varepsilon)R_{uv}\le\|Z(\chi_u-\chi_v)\|^2\le(1+\varepsilon)R_{uv}\quad\text{for all }u,v,$$

where $\|\cdot\|$ is the Euclidean norm. In the paper, $Z=QW^{1/2}BL^+$ for a random $\pm1/\sqrt k$ matrix $Q$ with $k=O(\log n/\varepsilon^2)$, and the Johnson–Lindenstrauss lemma makes it a sketch with high probability. Write $z_i$ and $\tilde z_i$ for the $i$-th rows of $Z$ and of an approximation $\widetilde Z$, as vectors in $\mathbb R^V$.

Formalization targets

Goal: Lemma 9 (p. 11)

Let $0<\varepsilon<1$. If $Z$ is a resistance sketch, if every row satisfies

$$\|z_i-\tilde z_i\|_L\le\delta\|z_i\|_L,\tag{4}$$

and if

$$\delta\le\frac{\varepsilon}{3}\sqrt{\frac{2(1-\varepsilon)w_{\min}}{(1+\varepsilon)n^3w_{\max}}},\tag{5}$$

then for every pair $u,v$

$$(1-\varepsilon)^2R_{uv}\le\|\widetilde Z(\chi_u-\chi_v)\|^2\le(1+\varepsilon)^2R_{uv}.$$

The lemma is stated for arbitrary $k$, $Z$ and $\widetilde Z$: nothing about the random projection or the solver enters beyond (4) and the sketch property.

Milestones

• Trace identity (§3, p. 8): $\sum_{e}w_eR_e=n-1$ for a connected graph.
• Proposition 10 (p. 12): $R_{uv}\ge 2/(nw_{\max})$ for distinct vertices $u\neq v$ of a connected simple graph.

Significance

Lemma 9 is the correctness half of the paper's Theorem 2: together with a Johnson–Lindenstrauss lemma and the Spielman–Teng solver it yields a data structure, built in $\widetilde O(m\log r/\varepsilon^2)$ time, that returns any effective resistance to within a factor $(1\pm\varepsilon)^2$ in $O(\log n/\varepsilon^2)$ time. This in turn makes the effective-resistance sampling of the paper's Theorem 1 run in nearly linear time, and the same sketch-and-solve pattern has been reused in later work on Laplacian solvers, graph sparsification and electrical-flow algorithms.

The result is proved in the paper. Formalizing it produces machine-checked statements of three facts that recur throughout spectral graph theory: the trace identity $\sum_e w_eR_e=n-1$ (Foster's theorem in its weighted form), the lower bound on effective resistances by comparison with the complete graph, and the stability of a resistance sketch under relative $L$-norm errors. Neither Mathlib nor this platform states any of them for the linear-algebraic definition of effective resistance used here.

Difficulty

The hypothesis (4) controls the error row by row, in the $L$-norm on $\mathbb R^V$, while the conclusion concerns the columns of $\widetilde Z$ applied to $\chi_u-\chi_v$, in the Euclidean norm on $\mathbb R^k$, and it is a relative bound for every pair at once. A relative bound cannot hold unless $R_{uv}$ is bounded below uniformly over all pairs of distinct vertices, which is where the factors $n^3$, $w_{\min}$ and $w_{\max}$ of (5) come from. Such a lower bound is false for multigraphs, whose parallel edges can make $R_{uv}$ arbitrarily small, and the relation between the $L$-norm of a row and the Euclidean norms of the columns involves every edge of the graph, not only a path between $u$ and $v$.

Proposition 10 is classically derived from Rayleigh's monotonicity law. Its standard formal statement on this platform concerns the probabilistic definition of effective resistance through hitting probabilities of a random walk, which is a different definition from $(\chi_u-\chi_v)^{\mathsf T}L^+(\chi_u-\chi_v)$; no theorem relating the two is available.

Formalization scope

The graph is a structure WGraph V E over finite types $V$ (vertices, $n=$ Fintype.card V) and $E$ (edges), with head, tail : E → V, head e ≠ tail e, weights w : E → ℝ with 0 < w e. Connectivity is that of the underlying simple graph (Mathlib's SimpleGraph.Connected, which includes $V\neq\emptyset$); simplicity means that no two edges join the same unordered pair. Matrices are Mathlib matrices indexed by $E$ and $V$. $L^+$ is the published Moore–Penrose pseudoinverse HarmonicGames.Decomposition.pinv of $x\mapsto Lx$ on the Euclidean space $\mathbb R^V$, converted back to a matrix; for symmetric $L$ this is the spectral pseudoinverse of §2.2. $\|Z x\|^2$ is the sum of squares of the coordinates, not Lean's sup norm. $n^3$ is the real number $n^3$.

Choices committed to, relative to the page:

• $w_{\min}$, $w_{\max}$ are any reals with $0<w_{\min}\le w_e\le w_{\max}$ for all edges; the exact extremes are an instance, and looser bounds only make (5) and Proposition 10 weaker.
• $\varepsilon$ is assumed to satisfy $0<\varepsilon<1$; the paper gives no range, and for $\varepsilon\ge1$ the square root in (5) has a non-positive argument.
• The graph is assumed simple in Lemma 9 and Proposition 10. Proposition 10 is false for multigraphs (two parallel unit edges give $R=1/2<1=2/(nw_{\max})$), and the proof of Lemma 9 uses it.
• Proposition 10 is stated for $u\neq v$. As printed it claims all $u,v$, which fails at $u=v$ since $R_{uu}=0$.
• The trace identity requires connectivity only.

A trivializing formalization is ruled out: the goal does not assume the intermediate inequality $|\|Zx\|-\|\widetilde Zx\||\le(\varepsilon/3)\|Zx\|$ of the proof, nor a stronger condition on $\delta$ than (5); its hypotheses are satisfiable (for example $\widetilde Z=Z$ with $Z=W^{1/2}BL^+$ and $\delta=0$), and its conclusion is not vacuous for $n\ge2$.

Infrastructure that a complete development needs, and that is reusable beyond this mission: the identity $L^+LL^+=L^+$ and $LL^+$ as the projection onto $\mathbf 1^\perp$ for a connected Laplacian; the trace identity; Loewner-order monotonicity of $R_{uv}$ in the edge weights; and the effective resistances of the complete graph. Contributions of any of these as separate lemmas are welcome. The random projection (Johnson–Lindenstrauss) and the solver's running time are outside this mission.

Selected references

• D. A. Spielman, N. Srivastava, Graph Sparsification by Effective Resistances, arXiv:0803.0929v4, 2009; SIAM J. Comput. 40(6), 2011. https://arxiv.org/abs/0803.0929, https://doi.org/10.1137/080734029
• D. A. Spielman, S.-H. Teng, Nearly-linear time algorithms for preconditioning and solving symmetric, diagonally dominant linear systems, arXiv:cs/0607105. https://arxiv.org/abs/cs/0607105
• D. Achlioptas, Database-friendly random projections: Johnson–Lindenstrauss with binary coins, J. Comput. Syst. Sci. 66(4), 2003. https://doi.org/10.1016/S0022-0000(03)00025-4
• P. G. Doyle, J. L. Snell, Random Walks and Electric Networks, MAA, 1984. https://arxiv.org/abs/math/0001057

Motivation

In the local model of differential privacy, no trusted curator ever sees the raw data: each individual randomizes their own record before handing it to the analyst. This is how private telemetry is collected in practice (randomized response and its descendants), and it raises a basic question: which learning tasks remain possible when the learner only sees locally randomized records?

Kasiviswanathan, Lee, Nissim, Raskhodnikova and Smith answered it in What Can We Learn Privately? (arXiv:0803.0924v3, the accepted version of SIAM J. Comput. 40(3) (2011) 793–826, DOI 10.1137/090756090; theorem numbers below are the arXiv v3's). They showed that local private learning is equivalent, up to polynomial factors, to learning in Kearns' statistical query (SQ) model (Kearns 1998), where an algorithm sees a distribution only through approximate expectations. This mission formalizes one direction of that equivalence: every SQ algorithm can be run by a local algorithm (§5.1.1, Theorem 5.7). The other direction (Lemma 5.8) is a separate mission of this series.

Timeline. Blum, Dwork, McSherry and Nissim (PODS 2005) observed that SQ algorithms can be simulated by a trusted curator adding noise to sums. Dwork, McSherry, Nissim and Smith (TCC 2006) introduced the Laplace mechanism. Kasiviswanathan et al. (FOCS 2008; journal version 2011) showed the simulation works even in the local model, with each record entering a single randomizer.

Setting

A database is a vector $z=(z_1,\dots,z_n)\in D^n$; two databases are neighbors if they differ in exactly one entry. A randomized algorithm $A$ 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 measurable sets $S$ of outputs. An $\varepsilon$-local randomizer is an $\varepsilon$-differentially private map applied to a single record: $\Pr[R(u)\in S]\le e^{\varepsilon}\Pr[R(u')\in S]$ for all $u,u'$.

The Laplace distribution $\mathrm{Lap}(s)$ has density $\frac1{2s}e^{-|x|/s}$.

An SQ oracle $SQ_P$ for a distribution $P$ on $D$ receives a query $g:D\to[-b,b]$ and a tolerance $\tau$, and may return any $v$ with $|v-\mathbb E_{u\sim P}[g(u)]|\le\tau$. An SQ algorithm with $t$ queries asks $(g_0,\tau_0),\dots,(g_{t-1},\tau_{t-1})$, where $(g_k,\tau_k)$ may depend on the earlier answers $a_0,\dots,a_{k-1}$ (adaptive), and outputs a function of all answers. A vector $a$ is a valid transcript against $SQ_P$ if every $a_k$ is within $\tau_k$ of the true mean of the query $g_k$ asked at that point.

For one query $g$, the randomizer $R_g(u)=g(u)+\eta$ with $\eta\sim\mathrm{Lap}(2b/\varepsilon)$ is applied to each record, and the local algorithm $\mathcal A_g$ outputs the average $\frac1n\sum_i(g(z_i)+\eta_i)$. The simulation of an SQ algorithm answers its $k$-th query $g_k$ by running $\mathcal A_{g_k}$ on the $k$-th block of $m$ fresh entries $z_{km},\dots,z_{km+m-1}$ and finally outputs what the SQ algorithm outputs on these answers.

Formalization targets

Goal: Theorem 5.7 (local simulation of SQ)

There is an absolute constant $c>0$ such that, for every SQ algorithm with $t$ queries into $[-b,b]$, and every $\varepsilon>0$; the accuracy claim further takes every tolerance at least $\tau$, $\varepsilon\le1$, $\varepsilon\tau\le4b$ and $0<\beta<1$:

$$\text{the simulation is }\varepsilon\text{-differentially private for every block size }m\text{ and every }n\ge tm,$$ $$m\ \ge\ c\,\frac{\ln(t/\beta)\,b^2}{\varepsilon^2\tau^2},\ z\sim P^n\ \Longrightarrow\ \Pr\bigl[\text{the simulated answers are a valid transcript against }SQ_P\bigr]\ \ge\ 1-\beta .$$

On that event the simulation outputs exactly what the SQ algorithm outputs against a valid oracle. The constant is left unspecified, as in the paper.

Milestones

1. $R_g$ is an $\varepsilon$-local randomizer; $\mathcal A_g$ is $\varepsilon$-differentially private (p. 20).
2. Hoeffding's bound for the empirical mean of $g$: $\Pr[|\frac1n\sum g(u_i)-v|\ge\tau/2]\le2e^{-\tau^2n/(8b^2)}$.
3. The average of $n$ i.i.d. $\mathrm{Lap}(2b/\varepsilon)$ variables lies in $[-\tau/2,\tau/2]$ with probability at least $1-\beta/2$ once $n\ge c\ln(1/\beta)b^2/(\varepsilon^2\tau^2)$.
4. Lemma 5.6: $\mathcal A_g$ approximates $\mathbb E_P[g]$ within $\pm\tau$ with probability $1-\beta$ from $n\ge c\ln(1/\beta)b^2/(\varepsilon^2\tau^2)$ samples.

Significance

Theorem 5.7 is the inclusion "SQ ⊆ local" in the paper's characterization of local private learning: every concept class learnable with statistical queries is learnable by an $\varepsilon$-local algorithm, with sample size growing like $t\log(t/\beta)b^2/(\varepsilon^2\tau^2)$. Combined with the converse simulation (Lemma 5.8), it identifies local private learnability with SQ learnability (Theorem 5.14). It thereby transfers the known SQ lower bounds, such as the one for parity, to the local model. It also shows that nonadaptive SQ algorithms become noninteractive local protocols.

The result is proved in the paper; to our knowledge it has no machine-checked proof. A formalization fixes what "the simulation gives the same output" means against an adversarial oracle and an adaptive algorithm. It also supplies reusable Lean objects for local differential privacy, Laplace noise and SQ algorithms.

Difficulty

The privacy half is the easy-looking part, but it is adaptive: the query asked in block $k$ depends on the noisy answers from blocks $0,\dots,k-1$. A database change in block $k$ therefore changes the law of all later answers, not only $a_k$. The argument must use that every entry enters exactly one randomizer and compose along the adaptive transcript.

The accuracy half has the same adaptivity issue: the union bound over queries needs, for each $k$, the failure probability of block $k$ conditioned on everything before it. That is where the fresh blocks and measurability are used. The concentration step for Laplace averages is sub-exponential, not sub-Gaussian. The naive use of the paper's appendix lemma (A.3) fails: it is stated as an equality for every deviation $\delta>0$, but its proof only covers deviations of order the Laplace scale.

Formalization scope

Databases are Fin n → D (0-based). Randomized algorithms are identified with the laws of their outputs (Measure); differential privacy is required on all measurable sets. An SQ algorithm is a deterministic adaptive strategy (SQAlg): a randomized one is a mixture over its coins, to which the result transfers. "At most $t$ queries" is "exactly $t$" after padding with dummy queries. Queries are real valued with $|g|\le b$, as the paper allows after Definition 5.4. Block $k$ consists of the database indices $km,\dots,km+m-1$, so the blocks are disjoint by construction, and the simulated answers are a deterministic function of the database and the $t\times m$ noise array. The natural logarithm replaces the paper's base 2, which only changes $c$. Constants are existential and quantified before everything else.

Explicit choices, each recorded in the item that makes it:

• $\varepsilon\tau\le4b$ in Lemma 5.6, the Laplace step and Theorem 5.7. Without it the printed statements are false: for $\varepsilon\tau/b$ large a single sample is allowed, and its Laplace noise exceeds $\tau$ too often.
• $\varepsilon\le1$ in Lemma 5.6 and in the accuracy half of Theorem 5.7 (the privacy half holds for every $\varepsilon>0$). Without it the threshold $c\ln(1/\beta)b^2/(\varepsilon^2\tau^2)$ can be smaller than the sample size needed to estimate $\mathbb E[g]$ at all. The paper's own remark about an $O(\varepsilon^{-2})$ factor presumes $\varepsilon=O(1)$.
• $\beta\le1/2$ in the Laplace step, which is false for $\beta$ near $1$.
• Each query is jointly measurable in (earlier answers, record), and the output map is measurable for the privacy claim.
• "Gives the same output as $\mathcal A_{SQ}$" is "the simulated answers are a valid transcript against $SQ_P$". Accuracy bounds the measure of the failure event by $\beta$.
• "Noninteractive if nonadaptive" and "efficient" are not formalized.

A trivializing formalization is ruled out: the oracle is not replaced by the exact expectation, accuracy is required for every query actually asked (not only the first), privacy holds for every database (not only i.i.d. samples), and the constant $c$ cannot depend on $t$, $\beta$, $\varepsilon$, $\tau$, $b$ or the algorithm.

Needed infrastructure: the Laplace distribution as a probability measure and its moment generating function, a Hoeffding bound for bounded i.i.d. variables, the Laplace mechanism, and adaptive composition along a transcript. All of these are reusable beyond this mission. Proofs of the milestones, of standalone Laplace and composition lemmas, and of the goal are welcome.

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, https://arxiv.org/abs/0803.0924 ; DOI 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
• C. Dwork, F. McSherry, K. Nissim, A. Smith, Calibrating noise to sensitivity in private data analysis, TCC 2006, LNCS 3876, 265–284. https://doi.org/10.1007/11681878_14
• A. Blum, C. Dwork, F. McSherry, K. Nissim, Practical privacy: the SuLQ framework, PODS 2005, 128–138. https://doi.org/10.1145/1065167.1065184
• W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

Motivation

Inversion gates create domains of definition as well as nonzero-value conditions. A rational hitting list must find a point where every inverse exists and where the final value is invertible. The source manuscript presents the surrounding research claim.

Setting

A noncommutative rational formula over ℚ has variables, constants, sums, ordered products and inverse gates, with tree-node size. Evaluation is a relation requiring genuine two-sided inverses. Admissible means defined at some positive-dimensional rational matrix tuple; nonzero means one such defined value is nonzero.

Formalization target

Construct one deterministic finite-state Turing machine and positive integers C,k which, on unary n,s≥1, outputs a list H of common positive-dimensional rational tuples with

$$\dim H,\quad|\operatorname{encode}(H)|,\quad\operatorname{time}(H)\le C(n+s+1)^k,$$

and every admissible nonzero size-s formula has a defined invertible value at some tuple in H.

The selected formal target is OAI.RationalHitting.main.

Significance and status

The output-length bound controls the full binary representation, including rational entries and all tuples. No separate inverse-depth or coefficient-height parameter is added. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

A tuple detecting one rational expression may encounter a singular inverse in another. Definedness and invertibility must be guaranteed at a list point for every eligible formula.

Formalization scope

Matrices and constants are rational; scalars use the algebra map. The fixed TM0 alphabet and state space, self-delimiting binary output and unary parameter input are explicit. The matrix dimension is shared across the entire list and required positive.

Selected references

• OpenAI, Polynomial Hitting Lists for Noncommutative Rational Formulas, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Online selection must commit before all values arrive, while the offline optimum sees the full vector. The mission asks how much one independent sample per item can recover under a matroid feasibility constraint. The source manuscript presents the surrounding research claim.

Setting

A matroid on Fin n specifies feasible independent subsets. An online rule sees the full initial sample vector, a finite random seed and the arriving label/value prefix. Sample and value coordinates are jointly independent, corresponding marginals agree, and the seed is independent of all of them.

Formalization target

For every labeled matroid, construct a distribution-independent rule and seed law such that every prefix is feasible and, for every measurable arrival permutation,

$$\mathbb E[\operatorname{reward}]\ge2^{-310}\mathbb E[\operatorname{OPT}].$$

The arrival order may depend on all samples, all values and the entire seed. Reward integrability is also required.

The selected formal target is OAI.MatroidProphet.one_sample.

Significance and status

The rule and its seed distribution depend only on the known matroid. The allowed adversary is stronger than an order chosen before the values or random seed are revealed. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Independence of the input coordinates does not imply independence of the adversarial order. The guarantee must survive an order selected with full information while decisions remain irrevocable.

Formalization scope

Values are nonnegative almost surely, and only the actual offline optimum is assumed integrable. The hidden-vector target with ratio 2⁻²⁹³ provides an available supporting milestone. The duplicated one-sample formulation and secretary consequence remain references in their independent source group.

Selected references

• OpenAI, One Sample Suffices for Matroid Prophet Inequalities against an Almighty Adversary, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation

Rectangular matrix products arise when the two outer dimensions are much larger than the inner dimension. The dual exponent records the largest inner growth rate compatible with arithmetic exponent two. The source manuscript presents the surrounding research claim.

Setting

For k∈[0,1], ω_ℂ(1,k,1) is the infimum of exponents for multiplying an n×⌈nᵏ⌉ matrix by a ⌈nᵏ⌉×n matrix over ℂ. The dual exponent α is the supremum of k for which this infimum equals two.

Formalization target

Prove the strict bound

$$\alpha_{\mathbb C}>\frac{93}{200}=0.465.$$

The additional published rectangular endpoint asserts ω_ℂ(1,709/1000,1)<523/250=2.092.

The selected formal target is OAI.MatrixMultiplication.complex_alpha_gt_93_div_200.

Significance and status

Strictness is part of both statements. The supplied goal concerns the complex dual exponent; the manuscript title’s square bound and broader field claims are not attached formal targets. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

An algorithm for one size does not establish an asymptotic exponent. The definition quantifies over every positive slack and all positive sizes with one bound constant for each slack.

Formalization scope

Algorithms are division-free arithmetic programs with constants and input gates of cost zero and addition, subtraction and multiplication of cost one. Correctness is quantified over all input matrices. The dual exponent is a real supremum of exact exponent-two shapes, using the prescribed inner-dimension ceiling.

Selected references

• OpenAI, Complex Matrix Multiplication Below 2.258 and Rectangular Bounds, preprint, 2026. Pinned manuscript.
• OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

Motivation: does having a normal form imply termination?

Pure type systems (PTSs) are a uniform framework covering the simply typed λ-calculus, System F, the calculus of constructions and the type theories behind proof assistants such as Coq and Lean. A system is specified by its sorts (like $\ast$ and $\square$), axioms ($\ast:\square$) and product rules (which dependent function types may be formed). Normalization is the key metatheoretic property: it underlies logical consistency and decidability of type checking. There are two versions. A term is weakly normalizing if some sequence of β-reductions reaches a normal form, and strongly normalizing if every reduction sequence is finite. Strong normalization is what implementations need (any evaluation strategy terminates) but it is much harder to prove. The Barendregt–Geuvers–Klop conjecture asserts that, for pure type systems, the system-wide weak property already implies the strong one.

Timeline

• 1989 — Girard's Proofs and Types presents the Tait–Girard reducibility method for strong normalization (book).
• 1993 — Geuvers states the system-wide conjecture for β and βη reduction in his thesis (Logics and Type Systems, Nijmegen, Conjecture 8.1.2) (thesis).
• 1997 — Sørensen proves the implication for generalized nondependent, clean, negatable systems via continuation-passing translations (thesis, Copenhagen, Theorem 3.5.20).
• 2001 — Barthe, Hatcliff and Sørensen prove a uniform nondependent version (TCS 2001).
• 2006 — Barthe and Coquand show that erasing λ-domain annotations can identify non-convertible terms in non-normalizing PTSs (JFP 2006), a constraint on erasure-based approaches.
• 2014 — Roux and van Doorn develop a structural theory of PTSs, preserving weak normalization under sums and added rules (RTA–TLCA 2014).
• 2023 — Mull reduces the conjecture within tiered systems to an irrelevance-eliminating translation (TYPES 2022, LIPIcs 2023) and extends the nondependent results in his thesis (Chicago, 2023).
• 2025 — Roux proposes internal strong-normalization proofs for specific systems (TYPES 2025 abstract).
• 2026 — An OpenAI preprint, Weak and strong normalization in pure type systems (OpenAI Math Release, September 25, 2026), claims the β-version of the conjecture for every PTS, with no functionality assumption. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

A specification consists of a type $S$ of sorts, an axiom relation $\mathcal A\subseteq S^2$ and a rule relation $\mathcal R\subseteq S^3$; neither is assumed functional. Expressions are

$$M,N,A,B ::= x\mid s\mid MN\mid \lambda x{:}A.\,M\mid \Pi x{:}A.\,B,\qquad s\in S,$$

up to renaming of bound variables. β-reduction is the compatible closure of $(\lambda x{:}A.M)N\to_\beta M[x:=N]$, with steps allowed everywhere, including inside the annotation $A$ of a λ and both parts of a Π. Typing $\Gamma\vdash M:A$ is generated by the seven standard PTS rules (axiom, variable, weakening, product, abstraction, application, conversion up to $=_\beta$). A context is valid if each declared type is typed by a sort in the preceding prefix, and $M$ is legal in $\Gamma$ if $\Gamma\vdash M:A$ or $\Gamma\vdash A:M$ for some $A$.

The system is weakly (strongly) normalizing if every legal expression in every valid context is weakly (strongly) normalizing.

Formalization targets

Goal: β-Barendregt–Geuvers–Klop (Theorem 1)

For every specification $\mathcal P=(S,\mathcal A,\mathcal R)$,

$$\bigl(\forall \Gamma\ \text{valid},\ \forall M\ \text{legal in }\Gamma:\ M\ \text{is weakly }\beta\text{-normalizing}\bigr) \ \Longrightarrow\ \bigl(\forall \Gamma\ \text{valid},\ \forall M\ \text{legal in }\Gamma:\ M\ \text{is strongly }\beta\text{-normalizing}\bigr).$$

Both quantifiers range over the whole system; the theorem does not claim that an individual weakly normalizing term is strongly normalizing, and it says nothing about η-reduction. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. For any PTS, a proof that every legal term has a normal form now yields termination of every β-reduction strategy, including reductions inside types and annotations that may continue after the computational body is normal. Earlier results needed nondependent products, cleanliness, negatability, a tiered sort hierarchy, or a translation requiring extra product rules; the general case — arbitrary sorts and nonfunctional rules — was not covered by any earlier result since Geuvers' 1993 formulation.

Formalizing it. The statement is entirely syntactic and finitary, so it is a natural target for a proof assistant, and the relevant objects (de Bruijn syntax, substitution, typing derivations) are standard formalization material. The proof in the source is long (over 70 pages) and combines reducibility candidates with a fixed-point construction over sort profiles; a machine check would substantially raise confidence. A formal PTS metatheory library (substitution lemmas, confluence, subject reduction) would be reusable for other type-theory formalizations.

Difficulty

The obvious route — reducibility candidates à la Tait–Girard — needs a model of types built by recursion on sorts, which fails for impredicative or nonfunctional specifications where a type can have several sorts and no hierarchy is available. Translation methods (CPS or irrelevance elimination) need specific product rules to preserve typing, which a general specification may lack. Weak normalization of one term cannot be used alone; the argument must exploit normal forms of other open expressions. Annotations add a further complication: erasing them can change the equational theory (Barthe–Coquand), so reduction inside annotations must be tracked rather than erased.

Formalization scope

• Expressions use de Bruijn indices (Expr S with var, sort, app, lam, pi), so α-equivalence is syntactic; substitution is parallel substitution with lifting.
• Beta is full compatible closure, including lam_domain, pi_domain and pi_body steps; conversion is Relation.EqvGen Beta.
• HasType has exactly the seven PTS rules; contexts are lists stored newest-first, each declaration typed in its prefix (ValidContext). Legal includes expressions occurring as types.
• Weak normalization is reduction to a normal form; strong normalization is accessibility for the converse of Beta.
• The sort type S is arbitrary (any universe), and axioms and rules are arbitrary relations: no functionality, finiteness or hierarchy assumptions.
• Needed infrastructure: renaming/substitution lemmas, confluence of β, subject reduction for PTSs, reducibility candidates. All are reusable for any PTS formalization.

Selected references

• J. H. Geuvers, Logics and Type Systems, PhD thesis, Katholieke Universiteit Nijmegen, 1993. https://www.cs.ru.nl/~herman/PUBS/Proefschrift.pdf
• J.-Y. Girard, Proofs and Types, Cambridge University Press, 1989. https://www.paultaylor.eu/stable/prot.pdf
• M. H. B. Sørensen, Normalization in λ-Calculus and Type Theory, PhD thesis, University of Copenhagen, 1997. https://di.ku.dk/forskning/Publikationer/tekniske_rapporter/tekniske-rapporter-1997/97-27.pdf
• G. Barthe, J. Hatcliff and M. H. Sørensen, Weak normalization implies strong normalization in a class of non-dependent pure type systems, Theoret. Comput. Sci. (2001). https://doi.org/10.1016/S0304-3975(01)00012-3
• G. Barthe and T. Coquand, Remarks on the equational theory of non-normalizing pure type systems, J. Funct. Programming (2006). https://doi.org/10.1017/S0956796803004726
• C. Roux and F. van Doorn, The structural theory of pure type systems, RTA–TLCA 2014. https://doi.org/10.1007/978-3-319-08918-8_25
• N. Mull, An irrelevancy-eliminating translation of pure type systems, TYPES 2022, LIPIcs, 2023. https://doi.org/10.4230/LIPIcs.TYPES.2022.7
• OpenAI, Weak and strong normalization in pure type systems, OpenAI Math Release preprint, September 25, 2026 (source of the goal; Theorem 1, p. 3). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026/paper.pdf

Motivation

A logic for unordered finite structures (graphs, databases, relational inputs given up to isomorphism) must give answers that do not depend on how the input elements are named. Many polynomial-time algorithms nevertheless make arbitrary intermediate choices, for example the pivot in Gaussian elimination, without changing their final answer. Choiceless polynomial time with counting (CPT), introduced by Blass, Gurevich and Shelah (1999), forbids such choices entirely: it computes with hereditarily finite sets over the input elements and can count, but can never pick one element from a set merely because the set is nonempty.

Witnessed symmetric choice (WSC), in the form of Lichter and Schweitzer (2022, arXiv version 3), adds a controlled form of choice: the logic may pick an element of a set provided it also constructs automorphisms of the input showing that all elements of that set are interchangeable, so the answer cannot depend on which one was picked. Lichter and Schweitzer asked whether CPT + WSC is strictly more expressive than CPT. This mission concerns a proof that it is.

Timeline

• 1992. Cai, Fürer and Immerman construct graph pairs that hide a global parity obstruction from bounded-variable counting logic (doi:10.1007/BF01305232).
• 1998. Gire and Hoang introduce a fixpoint logic with a symmetry-based choice construct (doi:10.1006/inco.1998.2712).
• 1999, 2002. Blass, Gurevich and Shelah introduce choiceless polynomial time and its counting extension, and study CFI and linear-algebra instances (doi:10.1016/S0168-0072(99)00005-6, doi:10.2178/jsl/1190150152).
• 2003. Dawar and Richerby define a fixed-point logic with symmetric choice, with parameters and nesting (doi:10.1007/978-3-540-45220-1_16).
• 2008. Dawar, Richerby and Rossman show that preordered CFI queries are CPT-definable, and that bounded-rank CPT fails on them (doi:10.1016/j.apal.2007.11.011).
• 2014–2021. Abu Zaid, Grädel, Grohe and Pakusa, and Lichter and Schweitzer, obtain CPT canonization for structures with small abelian, dihedral or cyclic colour classes (doi:10.1007/978-3-662-44522-8_5, doi:10.4230/LIPIcs.CSL.2021.31).
• 2010–2023. Rossman and Pago prove functional lower bounds for CPT (doi:10.1007/978-3-642-15025-8_28, doi:10.4230/LIPIcs.CSL.2021.33, doi:10.4230/LIPIcs.MFCS.2023.73).
• 2022–2023. Lichter and Schweitzer define CPT + WSC, show that definable isomorphism testing yields canonization, and ask whether WSC strictly adds expressive power (arXiv:2205.14003).

The source of this mission is an OpenAI preprint dated September 24, 2026; its companion preprint (September 23, 2026) proves that CPT does not capture polynomial time.

Setting

Let $A$ be a finite set of atoms and $\mathrm{HF}(A)$ the hereditarily finite sets over $A$. CPT terms are built from variables, $\emptyset$, $\mathrm{Atoms}$, $\mathrm{Pair}(a,b)=\{a,b\}$, $\mathrm{Union}$, $\mathrm{Unique}$ (the member of a singleton, else $\emptyset$), $\mathrm{Card}$ (the von Neumann ordinal $|a|$), comprehensions $\{s(\bar a,u):u\in t(\bar a),\ \theta(\bar a,u)\}$ and iteration from $\emptyset$; formulas use input relations, equality and Boolean connectives. A sentence $(\Phi,p)$ pairs a closed formula with a polynomial $p$ that bounds the number of iteration steps and the hereditary size of all intermediate objects on inputs with $n$ atoms; exceeding the bounds yields a default or a failure value $\dagger$.

A WSC operator iterates a step term in which, at each stage, a choice term proposes a nonempty set $D$; one element is chosen, and a witness term must produce automorphisms of the entire input that fix the parameters and all earlier stages and map any element of $D$ to any other. If the witnesses are valid along every possible choice sequence, the output formula's value on the terminal state is returned; otherwise the value is $\dagger$.

The true-model class of a sentence is the set of finite structures on which it returns true; false and $\dagger$ are both outside it.

Formalization targets

Goal: Theorem 1.1

For the fixed vocabulary $\tau$ of eight binary relations there is a CPT + WSC sentence $(\Phi,p)$ with exactly one WSC occurrence such that

$$\text{(i)}\ (\Phi,p)\ \text{returns true or false on every finite }\tau\text{-structure;}\qquad \text{(ii)}\ \mathrm{TrueModels}(\Phi,p)\neq\mathrm{TrueModels}(\Psi,q)\ \text{for every CPT sentence }(\Psi,q).$$

The Lean statement OAI.WitnessedChoice.main (via BGS.MainStatement) is open on the platform.

Significance

Since every CPT sentence is a CPT + WSC sentence, Theorem 1.1 gives a strict inclusion of definable Boolean queries and answers the expressiveness question posed by Lichter and Schweitzer in the true-model sense. The separation holds against CPT with counting and sets of arbitrary finite rank, not a rank-restricted fragment. It leaves open whether CPT + WSC captures polynomial time and the effect of nesting WSC operators.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.

Difficulty

Two different tasks must be done. The upper bound requires a legal WSC definition on all inputs, not only on the intended grid structures: witnesses must be genuine automorphisms of the whole input fixing the full history, which the sentence must check, with a fallback when the input is not of the intended shape. The lower bound must defeat every CPT sentence, including those that build nested sets of large rank; rank-sensitive support arguments (Dawar–Richerby–Rossman) do not suffice. The paper uses a nonabelian automorphism group whose central subgroup has rank-independent small supports, then a counting equivalence and a bounded-width description of complete CPT evaluations.

Formalization scope

• Syntax is a mutual inductive Term n / Formula n with de Bruijn-style Fin n variables, including iterate and the wsc formula; wscCount counts WSC occurrences.
• Evaluation returns Option (none is $\dagger$). resource p n = ⌊p(n)⌋ bounds iteration length and transitive-closure size.
• WSC validity (GoodWSC) quantifies over all choice prefixes; witnesses are permutationGraph g for permutations g that are input automorphisms, fix the free parameters and every earlier stage, and act transitively on the choice set.
• FiniteInput packs any finite carrier type with the eight-symbol relations (Ed, Cf, EB, VB, I, Z δ, δ : ZMod 3). Sentence.isCPT means wscCount = 0.

A complete development needs hereditarily finite sets with permutation actions, support and counting-equivalence theory, and the grid structures; much of this is shared with the companion CPT noncapture mission. Contributions formalizing Proposition 4.4 (a total all-input definition), Proposition 5.3 (transitivity for every parameter tree), Theorem 5.5 (opposite grid answers), Proposition 6.3 (small-orbit support bound), Theorem 8.1 (transfer through small supports) and Theorem 9.3 (eventual equality for every CPT sentence) are welcome.

Selected references

• OpenAI, Witnessed symmetric choice is strictly stronger than choiceless polynomial time with counting, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Witnessed-symmetric-choice-is-strictly-stronger-than-choiceless-polynomial-time-with-counting-September-24-2026/paper.pdf
• OpenAI, Choiceless polynomial time with counting does not capture polynomial time, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Choiceless-polynomial-time-with-counting-does-not-capture-polynomial-time-September-23-2026/paper.pdf
• M. Lichter, P. Schweitzer, Choiceless polynomial time with witnessed symmetric choice, 2023 (arXiv v3). https://arxiv.org/abs/2205.14003
• A. Blass, Y. Gurevich, S. Shelah, Choiceless polynomial time, Ann. Pure Appl. Logic, 1999. https://doi.org/10.1016/S0168-0072(99)00005-6
• A. Blass, Y. Gurevich, S. Shelah, On polynomial time computation over unordered structures, J. Symbolic Logic, 2002. https://doi.org/10.2178/jsl/1190150152
• A. Dawar, D. Richerby, B. Rossman, Choiceless polynomial time, counting and the Cai–Fürer–Immerman graphs, Ann. Pure Appl. Logic, 2008. https://doi.org/10.1016/j.apal.2007.11.011
• J.-Y. Cai, M. Fürer, N. Immerman, An optimal lower bound on the number of variables for graph identification, Combinatorica, 1992. https://doi.org/10.1007/BF01305232
• F. Gire, H. K. Hoang, An extension of fixpoint logic with a symmetry-based choice construct, Inform. and Comput., 1998. https://doi.org/10.1006/inco.1998.2712
• A. Dawar, D. Richerby, A fixed-point logic with symmetric choice, CSL, 2003. https://doi.org/10.1007/978-3-540-45220-1_16

Motivation

Descriptive complexity asks whether complexity classes can be characterized by logics, without reference to machines. Immerman and Vardi (1982) showed that on ordered finite structures, first-order logic with a least fixed-point operator expresses exactly the polynomial-time queries. On unordered structures, such as graphs given only up to isomorphism, an algorithm must not depend on an arbitrary ordering of the input, and whether some logic captures polynomial time there is a central open question (Chandra–Harel 1982, Gurevich 1988).

Choiceless polynomial time with counting (CPT), introduced by Blass, Gurevich and Shelah (1999), was for decades the strongest candidate: it computes with hereditarily finite sets built over the input elements, can count, and is invariant under automorphisms by construction. Blass, Gurevich and Shelah conjectured that CPT is still a proper fragment of polynomial time. This mission concerns a proof of that conjecture.

Timeline

• 1982. Immerman and Vardi capture polynomial time on ordered structures by fixed-point logic (doi:10.1145/800070.802187, doi:10.1145/800070.802186); Chandra and Harel raise the unordered question (doi:10.1016/0022-0000(82)90012-5).
• 1988. Gurevich formulates the question of a logic capturing polynomial time and conjectures that none exists.
• 1992. Cai, Fürer and Immerman construct polynomial-time graph queries beyond fixed-point logic with counting (doi:10.1007/BF01305232).
• 1999, 2002. Blass, Gurevich and Shelah introduce choiceless polynomial time and study CFI and linear-algebra instances as potential separating examples (doi:10.1016/S0168-0072(99)00005-6, doi:10.2178/jsl/1190150152).
• 2000. Shelah claims noncapture for counting extensions; later accounts continue to list the problem as open.
• 2008. Dawar, Richerby and Rossman show that CFI queries over ordered base graphs are CPT-definable, and that bounded-rank CPT with counting fails on them (doi:10.1016/j.apal.2007.11.011).
• 2010–2023. Rossman and Pago prove functional lower bounds for CPT (no construction of hyperplanes, no fine preorders on hypercubes) (doi:10.1007/978-3-642-15025-8_28, doi:10.4230/LIPIcs.CSL.2021.33); Grädel, Pakusa, Schalthöfer and Kaiser characterize CPT by iterated first-order interpretations (doi:10.1109/LICS.2015.68).
• 2025. Dawar, Grädel, Kullmann and Pago still record the capture problem as open (doi:10.4230/LIPIcs.MFCS.2025.40).

The source of this mission is an OpenAI preprint dated September 23, 2026.

Setting

Fix the field $\mathbb F=\mathbb F_3$ and the vocabulary of eight binary relation symbols $\tau=\{\mathrm{Ed},\mathrm{Cf},\mathrm{EB},\mathrm{VB},I,Z_0,Z_1,Z_2\}$. For a finite $\tau$-structure $A$ put

$$Y=\{y:\mathrm{Ed}(y,y)\},\quad X=\{a:\mathrm{Cf}(a,a)\},\quad X_t=\{a\in X:\mathrm{VB}(t,a)\}\ (t\in X),$$ $$C(y,a)=\sum_{x\in Y,\ I(a,x)}\ \sum_{\delta\in\mathbb F,\ Z_\delta(y,x)}\delta .$$

With unknowns $(\lambda_a)_{a\in X}$ and $(\mu_y)_{y\in Y}$ (separate families), the system consists of

$$\sum_{a\in X_t}\lambda_a=1\quad(t\in X),\qquad \mu_y=\sum_{a\in X_t}\lambda_a\,C(y,a)$$

for every $(t,y)\in X\times Y$ such that some $a\in X_t$ and $x\in Y$ satisfy $I(a,x)$ and $\mathrm{EB}(y,x)$. The query $Q(A)$ says this system is consistent over $\mathbb F_3$. No promise is imposed on the input.

A CPT program is a fixed finite set of rules that updates dynamic functions whose values are hereditarily finite sets over the atoms of $A$, using pairing, union, comprehension, equality, membership, the input relations, and the cardinality operation (which returns a von Neumann ordinal). A program defines $Q$ if for fixed polynomials $T,S$, on every input of size $n$ it halts within $T(n)$ steps, touches at most $S(n)$ hereditarily finite objects, and accepts exactly when $Q(A)$ holds. No bound on set rank is imposed.

Formalization targets

Goal: Theorem 1

$$Q\ \text{is isomorphism-invariant},\qquad Q\in\mathrm{P}\ \text{(from an ordered encoding)},\qquad Q\notin\mathrm{CPT}.$$

The Lean statement OAI.CPTSeparation.main is the conjunction of these three clauses. It is open on the platform.

Significance

The theorem confirms the Blass–Gurevich–Shelah noncapture conjecture for the full counting formalism: CPT does not capture polynomial time on unordered structures. It removes the leading candidate logic from Gurevich's question, which itself remains open. Because $Q$ is expressible in fixed-point logic with a solvability or rank operator over $\mathbb F_3$ (Corollary 3, p. 3), it also shows that neither of those logics is contained in CPT. The lower bound holds for programs of arbitrary set rank, unlike the bounded-rank lower bounds of Dawar–Richerby–Rossman.

The result is proved in an OpenAI preprint, which has not been peer reviewed. No machine-checked proof exists.

Difficulty

The polynomial-time upper bound is Gaussian elimination. The obstacle is the lower bound against every CPT program, including those that build sets of unbounded rank. Bounded-variable counting games handle fixed-point logic with counting but do not by themselves control CPT, which is strictly stronger (it decides CFI queries over ordered base graphs). Rank-dependent support arguments give lower bounds only for each fixed rank. The paper needs support bounds independent of rank, for which it uses a nonabelian automorphism group acting on grid structures, then a counting equivalence for all supported objects, and finally a transfer to complete computations via an interpretation characterization of CPT.

Formalization scope

• Input A gives a Boolean-valued binary relation for each Symbol (Ed, Cf, EB, VB, I, Z δ with δ : ZMod 3). Input.query is the existence of λ, μ satisfying the normalization and consistency equations exactly as above; an empty system is consistent.
• OrdinaryPolynomialTime asks for a function on ordered tables and a Turing.TM2ComputableInPolyTime machine with finite alphabets computing it from the cell-by-cell table encoding, agreeing with the query for every ordering of every structure.
• FullCPT defines terms and rules over hereditarily finite sets (Lists quotient), a state of finitely many nonempty locations, synchronous consistent updates, halt/accept flags, and the set of occurring objects (active elements plus roots of evaluated terms). EvaluationDefinable Q asks for one program and polynomials time, space that accept exactly the inputs satisfying Q, halting within time and with at most space occurring objects.
• This is the original operational formulation; the paper's proof passes through the interpretation characterization of CPT (Grädel–Pakusa–Schalthöfer–Kaiser), which a formal proof must either formalize or bypass.

A complete development needs: hereditarily finite sets and automorphism actions on them, support theory, counting equivalence games, the grid structures with their automorphism group, and a CPT-to-interpretation translation. Contributions formalizing Proposition 2 (polynomial-time decidability), Proposition 8 (small-orbit support bound), Proposition 13 (quantitative homogeneity) and Theorem 14 (transfer through small supports) are welcome.

Selected references

• OpenAI, Choiceless polynomial time with counting does not capture polynomial time, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Choiceless-polynomial-time-with-counting-does-not-capture-polynomial-time-September-23-2026/paper.pdf
• A. Blass, Y. Gurevich, S. Shelah, Choiceless polynomial time, Ann. Pure Appl. Logic, 1999. https://doi.org/10.1016/S0168-0072(99)00005-6
• A. Blass, Y. Gurevich, S. Shelah, On polynomial time computation over unordered structures, J. Symbolic Logic, 2002. https://doi.org/10.2178/jsl/1190150152
• J.-Y. Cai, M. Fürer, N. Immerman, An optimal lower bound on the number of variables for graph identification, Combinatorica, 1992. https://doi.org/10.1007/BF01305232
• A. Dawar, D. Richerby, B. Rossman, Choiceless polynomial time, counting and the Cai–Fürer–Immerman graphs, Ann. Pure Appl. Logic, 2008. https://doi.org/10.1016/j.apal.2007.11.011
• E. Grädel, W. Pakusa, S. Schalthöfer, Ł. Kaiser, Characterising choiceless polynomial time with first-order interpretations, LICS, 2015. https://doi.org/10.1109/LICS.2015.68
• B. Rossman, Choiceless computation and symmetry, 2010. https://doi.org/10.1007/978-3-642-15025-8_28
• B. Pago, Choiceless computation and symmetry: limitations of definability, CSL, 2021. https://doi.org/10.4230/LIPIcs.CSL.2021.33
• N. Immerman, Relational queries computable in polynomial time, STOC, 1982. https://doi.org/10.1145/800070.802187
• A. K. Chandra, D. Harel, Structure and complexity of relational queries, J. Comput. System Sci., 1982. https://doi.org/10.1016/0022-0000(82)90012-5

Motivation: removal lemmas and property testing for ordered matrices

A removal lemma says that an object far from having a forbidden substructure must contain many copies of it. Such statements are the combinatorial backbone of property testing: if every matrix that is $\epsilon$-far from avoiding a pattern $H$ contains at least $c_H\epsilon^{C_H}n^{2k}$ copies of $H$, then sampling a number of rows and columns polynomial in $1/\epsilon$ detects the pattern with constant probability. Whether removal bounds are polynomial determines whether testers are efficient. For binary matrices whose rows and columns carry a fixed order, qualitative removal is known, and the polynomial version was conjectured.

Timeline

• 2007 — Alon, Fischer and Newman prove polynomial-query testing for fixed finite forbidden families of binary matrices when row and column order is ignored, and raise the ordered question (SIAM J. Comput. 2007, §7).
• 2007 — Fischer and Rozenberg obtain nonpolynomial lower bounds for a fixed $2\times2$ pattern in ternary host matrices, order ignored (APPROX–RANDOM 2007).
• 2017 — Alon, Ben-Eliezer and Fischer establish qualitative removal for ordered graphs and matrices: a positive copy density exists for each fixed positive distance (FOCS 2017).
• 2020 — Alon and Ben-Eliezer prove polynomial removal for families closed under row (or column) permutations and polynomial bounds for many entry-disjoint copies, and pose the polynomial removal question for finite families of ordered binary matrices (Problem 1.4) (Order 2020).
• 2022 — Gishboliner and Tomon classify polynomial induced removal for ordered graphs, a different single-order symmetric model (Combinatorial Theory 2022).
• 2025 — The singleton version appears as Conjecture 4.5 in the survey of Gishboliner and Shapira (Comput. Sci. Rev. 2025).
• 2026 — An OpenAI preprint, Polynomial removal fails for ordered binary matrices (OpenAI Math Release, September 25, 2026), claims a fixed $66\times66$ binary pattern for which no polynomial removal bound holds. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

A binary matrix of order $n$ is a map $A:[n]\times[n]\to\{0,1\}$ (in Lean BinaryMatrix n := Fin n → Fin n → Bool). For a $k\times k$ binary pattern $H$, an ordered copy of $H$ in $A$ is a pair of strictly increasing maps $r,c:[k]\to[n]$ with $A(r_i,c_j)=H(i,j)$ for all $i,j$: zeros must match as well as ones, and rows and columns are chosen independently. $N_H(A)$ is the number of ordered copies, and $A$ is $H$-free if $N_H(A)=0$. The normalized distance to $H$-freeness is

$$\operatorname{dist}_H(A)=\frac1{n^2}\min_{B\ H\text{-free}}\bigl|\{(r,c):A(r,c)\neq B(r,c)\}\bigr|,$$

where every cell may be changed in either direction.

The polynomial ordered binary matrix-removal conjecture asserts that for each fixed $H$ there are $c_H,C_H>0$ such that $N_H(A)\ge c_H\epsilon^{C_H}n^{2k}$ whenever $\operatorname{dist}_H(A)\ge\epsilon$, for all $n\ge1$ and $0<\epsilon<1$.

The pattern $H$ is explicit: with $s=64$ and $\eta_b(a)=\lfloor a/2^{5-b}\rfloor\bmod 2$, the $64\times64$ anchor $S$ has $S(u,v)=\eta_{v-59}(u-33)$ for $33\le u\le 64$, $60\le v\le 64$, and $S(u,v)=\mathbf 1[u\neq v]$ otherwise, and

$$H=\begin{pmatrix} S & e_1 & e_2\\ e_1^{\mathsf T} & 1 & 0\\ e_2^{\mathsf T} & 1 & 1\end{pmatrix}\in\{0,1\}^{66\times66}.$$

Formalization targets

Goal: no polynomial removal bound for $H$

For every $c,C>0$ there exist $n\ge1$, $\epsilon\in(0,1)$ and a binary $n\times n$ matrix $A$ with

$$\operatorname{dist}_H(A)\ge\epsilon\qquad\text{and}\qquad N_H(A)<c\,\epsilon^{C}\,n^{132}.$$

This is the "consequently" clause of Theorem 1.1 of the source, i.e. the negation of the conjecture for this fixed $H$ (here $2k=132$). The source proves more: for every $h\ge1$, with $n_h=(386h+2)2^h$ and $\epsilon_h=(386h+2)^{-2}$, an explicit $A_h$ has $\operatorname{dist}_H(A_h)\ge\epsilon_h$ and $N_H(A_h)\le\epsilon_h2^{-h}n_h^{132}$. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. A single explicit pattern shows that ordered binary matrix removal can be super-polynomial, answering the finite-family question of Alon and Ben-Eliezer negatively and disproving the singleton conjecture recorded by Gishboliner and Shapira. It also gives a testing lower bound (Corollary 5.1): a canonical row–column sampler needs $q\ge\exp(\Omega(\epsilon_h^{-1/2}))$ sampled positions per axis on these examples. Earlier non-polynomial examples needed a third symbol in the host; here the host is binary. The example separates hitting all existing copies (a set of $2^h$ cells meets them) from repairing the matrix (at least $4^h$ edits are needed).

Formalizing it. The statement is fully finite and explicit, so a formal proof would certify both the construction and the two counting estimates. The construction is intricate (tree-indexed blocks with interleaved orders, a 66-cell pattern), which is exactly where a machine check adds confidence.

Difficulty

Two estimates pull in opposite directions. The distance bound must hold against every binary repair, including repairs that create new copies elsewhere; the obvious argument — delete one cell per copy — fails because changing cells can create copies, and the source must show any repair needs at least $m^2$ edits. The copy bound requires locating every ordered copy of the 66-cell pattern in the unedited host, not only the designated anchors, which forces a rigidity analysis of how the anchor $S$ can embed.

Formalization scope

• Matrices are Fin n → Fin n → Bool; ordered copies are pairs of StrictMono maps Fin k → Fin n, counted by copyCount. fixedH : BinaryMatrix 66 encodes $H$ with 0-based indices (the anchor rule becomes etaBit (u-32) (v-58) for $32\le u$, $59\le v$).
• fixedMinEdits A is the minimum Hamming distance from $A$ to an $H$-free matrix (the all-zero matrix is $H$-free, so the minimum is attained by a genuine matrix, and the sentinel $n^2+1$ is never selected); fixedDistance divides by $n^2$.
• The bound $c\,\epsilon^C n^{132}$ uses Real.rpow; $c,C$ are arbitrary positive reals, and $n,\epsilon,A$ are existentially chosen, so the statement is exactly the failure of the conjectured inequality for this $H$. It is weaker than the explicit quantitative family of Theorem 1.1; a stronger milestone recording $n_h,\epsilon_h$ and the bound $\epsilon_h2^{-h}$ would be welcome.
• Needed infrastructure: the explicit tree matrices $A_h$, counting of ordered copies, and a lower bound for Hamming distance to $H$-freeness.

Selected references

• N. Alon, E. Fischer and I. Newman, Efficient testing of bipartite graphs for forbidden induced subgraphs, SIAM J. Comput. (2007). https://doi.org/10.1137/050627915
• E. Fischer and E. Rozenberg, Lower bounds for testing forbidden induced substructures in bipartite-graph-like combinatorial objects, APPROX–RANDOM 2007. https://doi.org/10.1007/978-3-540-74208-1_34
• N. Alon, O. Ben-Eliezer and E. Fischer, Testing hereditary properties of ordered graphs and matrices, FOCS 2017. https://doi.org/10.1109/FOCS.2017.83
• N. Alon and O. Ben-Eliezer, Efficient removal lemmas for matrices, Order (2020). https://doi.org/10.1007/s11083-019-09494-3
• L. Gishboliner and I. Tomon, Polynomial removal lemmas for ordered graphs, Combinatorial Theory (2022). https://doi.org/10.5070/C62359151
• L. Gishboliner and A. Shapira, Polynomial property testing, Computer Science Review (2025). https://doi.org/10.1016/j.cosrev.2025.100806
• OpenAI, Polynomial removal fails for ordered binary matrices, OpenAI Math Release preprint, September 25, 2026 (source of the goal; Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Polynomial-removal-fails-for-ordered-binary-matrices-September-25-2026/paper.pdf

Motivation

A thin spanning tree of a graph is a spanning tree that uses only a small fraction of the edges of every cut. Thin trees were introduced for the asymmetric traveling salesman problem: Asadpour, Goemans, Mądry, Oveis Gharan and Saberi showed that a thin tree of low cost can be augmented into a cheap tour, giving an $O(\log n/\log\log n)$-approximation (doi:10.1287/opre.2017.1603). Goddyn conjectured that high edge connectivity forces thin trees; the strong thin tree conjecture asks for thinness $C/k$ in every $k$-edge-connected multigraph. For applications one wants not just existence but an efficient algorithm that finds such a tree, also when parallel-edge multiplicities are huge and written in binary.

Background. The maximum-entropy rounding of Asadpour et al. constructs $O(\log n/(k\log\log n))$-thin trees. Oveis Gharan and Saberi constructed $O(1/k)$-thin trees on planar and bounded-genus graphs (2011, doi:10.1137/1.9781611973082.75). Anari and Oveis Gharan proved existence of $\mathrm{poly}(\log\log n)/k$-thin trees in general (2015, arXiv:1411.4613), without a polynomial-time construction. Klein and Olver (2023, doi:10.1109/FOCS57990.2023.00011) and Klein, Olver and Yeoh (2026, doi:10.4230/LIPIcs.ICALP.2026.129) handled laminar families and near-minimum cuts. A companion OpenAI preprint claims the existence statement of the strong conjecture.

The source of this mission, an OpenAI preprint dated September 23, 2026, claims a deterministic polynomial-time construction.

Setting

Graphs are finite undirected loopless multigraphs; parallel copies count separately. For $\varnothing\ne S\subsetneq V(G)$, $\delta_G(S)$ is the multiset of edges with exactly one endpoint in $S$, and $G$ is $k$-edge-connected if $|\delta_G(S)|\ge k$ for every such $S$. A spanning tree $T$ is $\alpha$-thin if $|\delta_T(S)|\le\alpha|\delta_G(S)|$ for all such $S$. Two input formats are allowed: an explicit list of labelled edge copies, or a list of endpoint pairs with multiplicities written in binary (so the number of edges can be exponential in the input length). Running time is measured in the total binary input length.

Formalization targets

Goal: Theorem 1.1 (algorithmic strong thin trees)

There is an absolute constant $C$ and a deterministic algorithm that, given $k\ge1$ and a $k$-edge-connected multigraph $G$ on at least one vertex (in either format), returns in time polynomial in the input length a spanning tree $T$ with

$$|\delta_T(S)|\le\frac Ck\,|\delta_G(S)|\qquad(\varnothing\ne S\subsetneq V(G)),$$

returning the empty tree for a one-vertex graph. Lean: OAI.AlgorithmicThinTrees.algorithmic_strong_thin_trees, open on the platform.

Significance

The theorem would give an algorithmic resolution of the strong thin tree conjecture: not only do $C/k$-thin trees exist, they can be found deterministically in polynomial time, even for exponentially many parallel edges. It also yields simultaneous cost-and-cut rounding (Corollary 7.1): from a fractional point whose mass on every cut is at least one, a tree in its support with every cut load and total cost within constant factors, with no metric assumption on costs. The order $1/k$ is optimal. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

Existence proofs for thin trees go through the Marcus–Spielman–Srivastava interlacing-families theorem and a fixed-point argument, neither of which is constructive: they show that some choice works without locating it. The algorithm must replace these by explicit, rational, polynomially sized computations (checked signings, rational positive semidefinite decompositions, bounded denominators) and must work with binary multiplicities, where even listing the edges is exponential. Certifying thinness on all exponentially many cuts must also be done without enumerating them.

Formalization scope

• Graphs: StrongThinTree.MultiGraph n m (vertices Fin n, edges Fin m, loopless). Inputs are ExplicitInput or BinaryInput (ordered, distinct endpoint pairs with multiplicities); a binary input's edge copies are Σ i, Fin (multiplicity i).
• Valid x: $n\ge1$, $k\ge1$ and EdgeConnected k.
• The machine model is CurrentKS.Machine: a deterministic machine with finitely many binary stacks and a finite instruction table, run for a fuel bound. Inputs and outputs are self-delimiting binary encodings (CurrentKS.encodeNat).
• AlgorithmicStrongThinTrees: ∃ C > 0, ∃ M a degree, 0 < a ∧ ∀ x, Valid x → after a * (len + 1)^degree steps M has halted and its output stack encodes a duplicate-free edge list forming a ThinTree C k; for $n=1$ the output is empty.
• One machine and one polynomial serve all inputs in both formats.

Needed infrastructure: the existence theory of the companion mission, a model of deterministic computation with polynomial-time bounds, exact rational linear algebra, and constructive spectral sparsification. Contributions formalizing Proposition 2.5, Proposition 3.1, Lemma 6.1, Theorem A.1 (rational rank-one signing) or Corollary 7.1 are welcome.

Selected references

• OpenAI, A polynomial-time construction of strong thin trees, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-polynomial-time-construction-of-strong-thin-trees-September-23-2026/paper.pdf
• OpenAI, The strong thin tree conjecture, preprint, September 23, 2026.
• A. Asadpour, M. X. Goemans, A. Mądry, S. Oveis Gharan, A. Saberi, An O(log n/log log n)-approximation algorithm for the asymmetric traveling salesman problem, Oper. Res., 2017. https://doi.org/10.1287/opre.2017.1603
• N. Anari, S. Oveis Gharan, Effective-resistance-reducing flows, spectrally thin trees, and asymmetric TSP, FOCS, 2015. https://arxiv.org/abs/1411.4613
• S. Oveis Gharan, A. Saberi, The asymmetric traveling salesman problem on graphs with bounded genus, SODA, 2011. https://doi.org/10.1137/1.9781611973082.75
• N. Klein, N. Olver, Thin trees for laminar families, FOCS, 2023. https://doi.org/10.1109/FOCS57990.2023.00011
• N. Klein, N. Olver, Z. S. Yeoh, Thin trees for near minimum cuts, ICALP, 2026. https://doi.org/10.4230/LIPIcs.ICALP.2026.129
• O. Svensson, J. Tarnawski, L. A. Végh, A constant-factor approximation algorithm for the asymmetric traveling salesman problem, J. ACM, 2020. https://doi.org/10.1145/3424306

Motivation

A spanning tree keeps a graph connected with as few edges as possible. A spanning tree is thin if, in addition, it uses only a small fraction of the edges of every cut. Thin trees were introduced as a tool for the asymmetric traveling salesman problem (ATSP): Asadpour, Goemans, Mądry, Oveis Gharan and Saberi showed that thin trees, together with cost control, can be augmented cheaply into tours, which gave an $O(\log n/\log\log n)$-approximation (doi:10.1287/opre.2017.1603). Goddyn's thin tree conjecture asks whether high edge connectivity alone forces an $\varepsilon$-thin spanning tree, independently of the number of vertices; the strong form asks for thinness $C/k$ in a $k$-edge-connected graph.

Background. Goddyn recorded the conjecture in a 2004 problem list. The Nash–Williams–Tutte theorem (1961) gives $\lfloor k/2\rfloor$ edge-disjoint spanning trees in a $k$-edge-connected graph (doi:10.1112/jlms/s1-36.1.445, doi:10.1112/jlms/s1-36.1.221), so each cut is used about $2/k$ times on average, but no single tree need be good for every cut. Oveis Gharan and Saberi proved the bound for planar and bounded-genus graphs (2011, doi:10.1137/1.9781611973082.75). Anari and Oveis Gharan obtained thinness $\mathrm{poly}(\log\log n)/k$ in general (2015, arXiv:1411.4613), using the Marcus–Spielman–Srivastava interlacing-families method (doi:10.4007/annals.2015.182.1.8). Klein and Olver handled any prescribed laminar family of cuts (2023, doi:10.1109/FOCS57990.2023.00011), and Klein, Olver and Yeoh controlled all near-minimum cuts (2026, doi:10.4230/LIPIcs.ICALP.2026.129). Constant-factor ATSP approximations were obtained by other means (Svensson–Tarnawski–Végh 2020, doi:10.1145/3424306; Traub–Vygen 2022, doi:10.1137/20M1339313), but the thin tree question stayed unresolved.

The source of this mission, an OpenAI preprint dated September 23, 2026, claims the strong thin tree conjecture.

Setting

Let $G=(V,E)$ be a finite undirected multigraph without loops; parallel edges are counted separately. For a nonempty proper subset $\varnothing\ne S\subsetneq V$, let $\delta_G(S)$ be the set of edges with exactly one endpoint in $S$. $G$ is $k$-edge-connected if $|\delta_G(S)|\ge k$ for every such $S$. For an edge set $T\subseteq E$, $\delta_T(S)=\delta_G(S)\cap T$. A spanning tree $T$ is $\alpha$-thin if $|\delta_T(S)|\le\alpha|\delta_G(S)|$ for every nonempty proper $S$.

Formalization targets

Goal: Theorem 1.1 (strong thin trees)

There is a universal constant $C>0$ such that for every $k\ge1$, every finite loopless $k$-edge-connected multigraph with at least two vertices has a spanning tree $T$ with

$$|\delta_T(S)|\le\frac{C}{k}\,|\delta_G(S)|\qquad(\varnothing\ne S\subsetneq V).$$

Lean: OAI.StrongThinTree.strongThinTree, open on the platform.

Significance

The order $1/k$ is optimal (two vertices joined by $k$ parallel edges). The theorem would settle both Goddyn's thin tree conjecture and its strong form, removing the $\mathrm{poly}(\log\log n)$ loss of Anari–Oveis Gharan. It shows that connectivity alone controls all cuts at once, and gives a structural route to ATSP integrality-gap bounds through thin trees. An algorithmic version (deterministic polynomial-time construction) is the subject of the companion mission in this family. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

Averaging over a Nash–Williams–Tutte packing controls each cut on average but not all cuts simultaneously: there are exponentially many cuts and a union bound over them loses a factor depending on $n$. Spectral approaches control all cuts via a matrix inequality, but spectrally thin trees need not exist when some edges have large effective resistance, which is why previous spectral arguments lost $\log\log n$ factors. One must instead keep a large tree packing on low-resistance edges through a sequence of sparsifications whose relative losses stay bounded.

Formalization scope

• MultiGraph n m: vertices Fin n, edges Fin m with endpoint maps and a looplessness proof; parallel edges are distinct edges.
• cut G T S: the edges of T with exactly one endpoint in S. Connected G T: every nonempty proper S is crossed by T. SpanningTree G T: T connected and every proper deletion disconnects.
• EdgeConnected G k: every nonempty proper cut has at least k edges.
• MainStatement: ∃ C > 0, ∀ k ≥ 1, ∀ n ≥ 2, ∀ G k-edge-connected, ∃ T spanning tree, ∀ S nonempty proper, |cut T S| ≤ (C/k)|cut G S| (real arithmetic).

Needed infrastructure: graph Laplacians and effective resistance, the Nash–Williams–Tutte theorem, the Marcus–Spielman–Srivastava mixed-characteristic-polynomial bound, and a Brouwer-type fixed point theorem (the paper proves the finite-dimensional case via Sperner's lemma). Contributions formalizing Theorem 2.3 (Nash–Williams–Tutte), Theorem 3.2, Theorem 4.1, Proposition 6.2 or Theorem A.1 are welcome.

Selected references

• OpenAI, The strong thin tree conjecture, preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-strong-thin-tree-conjecture-September-23-2026/paper.pdf
• L. A. Goddyn, Some open problems I like, problem list, 2004.
• A. Asadpour, M. X. Goemans, A. Mądry, S. Oveis Gharan, A. Saberi, An O(log n/log log n)-approximation algorithm for the asymmetric traveling salesman problem, Oper. Res., 2017. https://doi.org/10.1287/opre.2017.1603
• N. Anari, S. Oveis Gharan, Effective-resistance-reducing flows, spectrally thin trees, and asymmetric TSP, FOCS, 2015. https://arxiv.org/abs/1411.4613
• A. W. Marcus, D. A. Spielman, N. Srivastava, Interlacing families II: mixed characteristic polynomials and the Kadison–Singer problem, Ann. of Math., 2015. https://doi.org/10.4007/annals.2015.182.1.8
• S. Oveis Gharan, A. Saberi, The asymmetric traveling salesman problem on graphs with bounded genus, SODA, 2011. https://doi.org/10.1137/1.9781611973082.75
• N. Klein, N. Olver, Thin trees for laminar families, FOCS, 2023. https://doi.org/10.1109/FOCS57990.2023.00011
• N. Klein, N. Olver, Z. S. Yeoh, Thin trees for near minimum cuts, ICALP, 2026. https://doi.org/10.4230/LIPIcs.ICALP.2026.129
• C. St. J. A. Nash-Williams, Edge-disjoint spanning trees of finite graphs, J. London Math. Soc., 1961. https://doi.org/10.1112/jlms/s1-36.1.445