Complexity Theory

Motivation

A vertex cover of a graph is a set of vertices meeting every edge; $\tau(G)$ denotes the minimum size of one. Computing $\tau(G)$ exactly is NP-hard, but a two-line algorithm — take both endpoints of a maximal matching — always returns a cover of size at most $2\tau(G)$. Whether any polynomial-time algorithm achieves a fixed factor $2-\varepsilon$ is one of the best-known questions in approximation algorithms. Unconditional NP-hardness was known below $10\sqrt5-21\approx1.36$ and, after the 2-to-2 Games Theorem, below $\sqrt2$; factor-two hardness was known only under Khot's Unique Games Conjecture.

This mission asks for a machine-checked proof that every fixed approximation factor below two is NP-hard, as claimed in an OpenAI preprint dated September 23, 2026 (source, Corollary 1.2, p. 1). The preprint's direct reduction starts from ordinary perfect-completeness Label Cover. It has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Timeline

• 1972 — Karp proves Node Cover NP-complete (Karp 1972); the maximal-matching algorithm gives factor $2$.
• 1992–1998 — Feige–Goldwasser–Lovász–Safra–Szegedy (JACM 1996) link proof checking to approximation; the PCP theorem (Arora–Safra, JACM 1998; Arora–Lund–Motwani–Sudan–Szegedy, JACM 1998) gives a constant gap; Raz's parallel repetition (SICOMP 1998) yields Label Cover with arbitrarily small soundness.
• 2001 — Håstad: NP-hard below factor $7/6$ (JACM 2001).
• 2005 — Dinur–Safra: NP-hard below $10\sqrt5-21\approx1.36068$ (Annals 2005).
• 2002–2008 — Khot's Unique Games Conjecture (STOC 2002); Khot–Regev prove factor-$(2-\varepsilon)$ hardness assuming it (JCSS 2008).
• 2009 — Karakostas's algorithm achieves $2-\Theta(1/\sqrt{\log n})$ (TALG 2009), a saving that vanishes with $n$.
• 2017–2023 — The 2-to-2 Games programme (Khot–Minzer–Safra, ToC 2025; Dinur–Khot–Kindler–Minzer–Safra, ToC 2025; Barak–Kothari–Steurer, ITCS 2019; Khot–Minzer–Safra expansion, Annals 2023) gives NP-hardness below $\sqrt2$.
• 2026 — The OpenAI preprint claims NP-hardness for every fixed factor below $2$.

Setting

A graph is finite, simple, undirected and unweighted, given explicitly by its vertex count $n$ and a duplicate-free list of edges $\{u,v\}$ with $u<v$. A set $S$ of vertices is a cover if every edge has an endpoint in $S$, and $\tau(G)$ is the least size of a cover. An $\alpha$-approximation algorithm is a deterministic polynomial-time machine that, on every graph, outputs a duplicate-free list of vertices that covers all edges and has length at most $\alpha\,\tau(G)$.

3SAT inputs are bit strings decoding canonically to a conjunction of three-slot clauses; malformed strings are NO instances. A 3SAT decider is a deterministic polynomial-time machine answering membership correctly on every input.

Formalization targets

Milestone: the explicit cover gap (Theorem 1.1, p. 1)

For every integer $m\ge4$ there is a deterministic polynomial-time reduction $\varphi\mapsto G_\varphi$ from 3SAT to explicit simple graphs with

$$\varphi\text{ satisfiable}\Rightarrow \tau(G_\varphi)<\Bigl(\tfrac12+\tfrac1m\Bigr)|V(G_\varphi)|,\qquad \varphi\text{ unsatisfiable}\Rightarrow \tau(G_\varphi)>\Bigl(1-\tfrac1m\Bigr)|V(G_\varphi)|.$$

The ratio of the thresholds is $2-6/(m+2)\to2$. In Lean: OAI.VertexCover.explicit_cover_gap.

Goal: factor-two threshold (Corollary 1.2, p. 1)

For every real $\alpha$ with $1\le\alpha<2$, an $\alpha$-approximation algorithm for Vertex Cover yields a polynomial-time 3SAT decider:

$$\forall\,\alpha\in[1,2):\quad \mathrm{Approximation}(\alpha)\;\Longrightarrow\;\mathrm{ThreeSATDecision}.$$

In Lean: OAI.VertexCover.every_fixed_factor_below_two. The preprint derives it from Theorem 1.1 in its final section (pp. 23–24) by choosing $m$ from $\alpha$ and comparing the returned cover with an exact rational threshold. Together with the matching algorithm, it identifies $2$ as the approximation threshold unless P = NP.

Significance

The result itself. The statement removes the Unique Games hypothesis from the Khot–Regev theorem and closes the gap between the elementary factor-$2$ algorithm and hardness. The density gap of Theorem 1.1 is also a statement about independent sets: YES graphs have independent sets of density nearly $1/2$, NO graphs have none of density above $1/m$.

Formalizing it. No machine-checked proof of any super-constant Vertex Cover hardness bound is known to exist. A complete development requires the perfect-completeness Label Cover theorem (Theorem 2.1, p. 4; PCP theorem plus parallel repetition, used as an external input), the explicit graph construction and its polynomial-time implementation (Proposition 3.3, p. 7), and the preprint's analytic soundness argument. The Label Cover input and a library for polynomial-time gap reductions on TM2 machines are reusable for many other hardness missions.

Difficulty

Soundness requires extracting short lists of candidate labels from an arbitrary large independent set, where each list may depend only on its own position's query. If a list also sees the opposite endpoint of a constraint or its occurrence index, the pair-decoding argument against Label Cover soundness breaks down (Introduction, pp. 3–4). Classical approaches either need the stronger Unique Games source promise (Khot–Regev) or only reach densities near $1-1/\sqrt2$ (the 2-to-2 route), which gives factor $\sqrt2$ rather than $2$. Averaging to impose the information restriction can erase all variance; the analytic core is retaining it without any dependence on the label alphabet sizes.

Formalization scope

• Graphs are VertexCover.ExplicitGraph: n : ℕ and a Nodup list of pairs in Fin n × Fin n with e.1 < e.2; coverNumber is the least cardinality of a covering Finset (always defined since univ covers).
• Encodings: inputs are raw bits; graphs are encoded by ExplicitGraph.bits (vertex count, all vertex names, edge count, edge endpoints, each with prefix-free binary framing); an approximation's output list is encoded by natListBits.
• Approximation α bundles a polynomial-time TM2 program on graph encodings with finite tape alphabets, whose output is duplicate-free, in range, covers every edge and has length at most α * coverNumber. ThreeSATDecision is a polynomial-time TM2 decider correct on every input.
• The goal is an implication from an algorithm to a decider: no assumption P ≠ NP is built in, and the hypothesis $1\le\alpha<2$ is satisfied by real algorithms only if 3SAT is easy, which is exactly the content. It cannot be discharged trivially because Approximation α must be correct on every graph.
• The milestone's thresholds are compared in ℝ with strict inequalities as in the source.

Welcome contributions: Label Cover hardness (PCP theorem + parallel repetition), Efron–Stein decompositions and variance inequalities on product spaces, and general complexity-theoretic infrastructure for Turing.TM2ComputableInPolyTime.

Selected references

• OpenAI, The Factor-Two Hardness Threshold for Vertex Cover, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Factor-Two-Hardness-Threshold-for-Vertex-Cover-September-23-2026/paper.pdf
• R. M. Karp, Reducibility among combinatorial problems, Complexity of Computer Computations, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9
• J. Håstad, Some optimal inapproximability results, J. ACM 48 (2001). https://doi.org/10.1145/502090.502098
• I. Dinur, S. Safra, On the hardness of approximating minimum vertex cover, Ann. of Math. 162 (2005). https://doi.org/10.4007/annals.2005.162.439
• S. Khot, O. Regev, Vertex cover might be hard to approximate to within 2−ε, J. Comput. Syst. Sci. 74 (2008). https://doi.org/10.1016/j.jcss.2007.06.019
• G. Karakostas, A better approximation ratio for the Vertex Cover problem, ACM Trans. Algorithms (2009). https://doi.org/10.1145/1597036.1597045
• R. Raz, A parallel repetition theorem, SIAM J. Comput. (1998). https://doi.org/10.1137/S0097539795280895
• S. Khot, D. Minzer, M. Safra, Pseudorandom sets in Grassmann graph have near-perfect expansion, Ann. of Math. 198 (2023). https://doi.org/10.4007/annals.2023.198.1.1
• I. Dinur, S. Khot, G. Kindler, D. Minzer, M. Safra, Towards a proof of the 2-to-1 games conjecture?, Theory of Computing 21 (2025). https://doi.org/10.4086/toc.2025.v021a011
• S. Khot, On the power of unique 2-prover 1-round games, STOC 2002. https://doi.org/10.1145/509907.510017

Motivation

Max-Cut asks for a partition of the vertices of a graph that maximizes the number of edges crossing it. Its decision version is one of Karp's original NP-complete problems, so the natural question is how well it can be approximated in polynomial time. Goemans and Williamson's semidefinite-programming algorithm with random-hyperplane rounding achieves ratio approaching

$$\alpha_{\mathrm{GW}}=\min_{-1\le\rho<1}\frac{2\arccos\rho}{\pi(1-\rho)}=0.878567\ldots$$

(GW 1995). Whether any polynomial-time algorithm can beat this constant is a central question of approximation algorithms: unconditional NP-hardness was known only above $16/17$, and optimality of $\alpha_{\mathrm{GW}}$ was known only under Khot's Unique Games Conjecture.

This mission asks for a machine-checked proof that approximating Max-Cut within any fixed ratio $\alpha\in(\alpha_{\mathrm{GW}},1]$ is NP-hard, even on simple unweighted graphs, as claimed in an OpenAI preprint dated September 23, 2026 (source, Theorem 1.1, p. 1). The preprint gives a direct reduction from the 2-to-1 Games Theorem, not via the Unique Games Conjecture. It has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Timeline

• 1972 — Karp lists Max-Cut among the original NP-complete problems (Karp 1972).
• 1995 — Goemans and Williamson give the SDP algorithm with ratio $\alpha_{\mathrm{GW}}$ (JACM 1995).
• 2000–2001 — Håstad's optimal inapproximability results (JACM 2001) combined with the gadgets of Trevisan, Sorkin, Sudan and Williamson (SICOMP 2000) rule out ratios above $16/17$.
• 2002 — Feige and Schechtman show the SDP integrality gap approaches $\alpha_{\mathrm{GW}}$ (RSA 2002); Khot formulates the Unique Games Conjecture (STOC 2002).
• 2007–2010 — Khot, Kindler, Mossel and O'Donnell prove that $\alpha_{\mathrm{GW}}$ is optimal assuming the UGC, conditional on Majority Is Stablest (SICOMP 2007), which Mossel, O'Donnell and Oleszkiewicz prove (Annals 2010) via Borell's Gaussian noise-stability bound (1985). O'Donnell–Wu (STOC 2008) and Raghavendra (STOC 2008) extend the UG-based picture.
• 2017–2025 — The Grassmann-graph programme establishes the 2-to-1 Games Theorem with imperfect completeness: Khot–Minzer–Safra (ToC 2025), Dinur–Khot–Kindler–Minzer–Safra (ToC 2025), Barak–Kothari–Steurer (ITCS 2019), Khot–Minzer–Safra expansion (Annals 2023).
• 2026 — The OpenAI preprint claims unconditional NP-hardness at every ratio above $\alpha_{\mathrm{GW}}$.

Setting

A simple unweighted graph on $N$ vertices is given by a symmetric, loopless Boolean adjacency table. A cut is a map $c$ from the vertices to $\{0,1\}$; its size is the number of unordered edges $\{u,v\}$ with $c(u)\ne c(v)$, and $\mathrm{MaxCut}(G)$ is the largest cut size. An algorithm is an $\alpha$-approximation if it always returns a cut of size at least $\alpha\cdot\mathrm{MaxCut}(G)$.

3SAT inputs are bit strings decoding canonically to a conjunction of three-slot clauses (repeated variables and literals allowed); malformed strings are NO instances. A gap reduction for $\alpha$ consists of rationals $Y>0$ and $N\ge0$ with $N<\alpha Y$, and a deterministic polynomial-time map $\varphi\mapsto(G_\varphi,Q_\varphi)$ outputting a graph together with a positive integer scale $Q_\varphi$ such that

$$\varphi\in\mathrm{3SAT}\Rightarrow \frac{\mathrm{MaxCut}(G_\varphi)}{Q_\varphi}\ge Y,\qquad \varphi\notin\mathrm{3SAT}\Rightarrow \frac{\mathrm{MaxCut}(G_\varphi)}{Q_\varphi}\le N.$$

Given such a reduction, an $\alpha$-approximation algorithm would decide 3SAT by comparing its output with $N Q_\varphi$.

Formalization targets

Goal: optimal Max-Cut hardness (Theorem 1.1, p. 1)

For every real $\alpha$ with $\alpha_{\mathrm{GW}}<\alpha\le1$, a gap reduction for $\alpha$ from 3SAT to simple unweighted Max-Cut exists:

$$\forall\,\alpha\in(\alpha_{\mathrm{GW}},1]:\quad \mathrm{GapReduction}(\alpha)\ne\varnothing.$$

In Lean this is OAI.OptimalMaxCut.main : OptimalMaxCut.MainStatement. The preprint proves it from a sharper weighted gap (Theorem 1.2, p. 2): for rational $t\in(0,1)$, $B(t)=\tfrac{2}{\pi}\arcsin t$ and $0<\varepsilon<(t-B(t))/4$, it is NP-hard to distinguish $\mathrm{Val}\ge\frac{1+t}{2}-\varepsilon$ from $\mathrm{Val}\le\frac{1+B(t)}{2}+\varepsilon$ on graphs with a rational edge distribution; Appendix B (p. 35) converts weighted graphs to simple unweighted ones.

Significance

The result itself. Theorem 1.1 shows that the Goemans–Williamson algorithm is optimal among polynomial-time algorithms unless P = NP, removing the Unique Games hypothesis from the result of Khot, Kindler, Mossel and O'Donnell. It is the most prominent instance of an SDP-tight threshold, and the gap form (Theorem 1.2) gives a whole curve of completeness/soundness pairs.

Formalizing it. No machine-checked proof of any optimal inapproximability result for Max-Cut exists. A full development requires the 2-to-1 Games Theorem in the affine form stated as Proposition 2.2 (p. 6) and derived in Appendix A, the Majority Is Stablest theorem (Lemma 2.1, p. 5), and the paper's new ingredients: tree-code Fourier analysis (Section 5), a vector-valued affine hashing lemma (Lemma 6.1, p. 14), dimension-independent extraction (Proposition 7.1, p. 18) and decoding (Proposition 8.4, p. 24). Several of these — Majority Is Stablest, Boolean Fourier analysis, polynomial-time gap reductions on Turing machines — are reusable libraries in their own right.

Difficulty

The classical long-code test for Max-Cut, analysed via Majority Is Stablest, identifies an influential coordinate of an arbitrary cut. Under the Unique Games Conjecture that coordinate is directly a label of the source game. Starting instead from 2-to-1 games, the influential coordinate is indexed by a gate input of the test, not by a source-game label, and the two endpoints of a source edge cannot in general reconstruct a common context without knowing their projection. The decoding loss must also be independent of the source alphabet, because the alphabet dimension is chosen after the target soundness; a dimension-dependent loss would make the parameter choice circular (Introduction, pp. 3–4).

Formalization scope

• Graphs are OptimalMaxCut.Graph: a vertex count with a symmetric loopless Bool adjacency function; maxCut maximizes cutSize over all Fin n → Bool, counting each unordered crossing edge once.
• The output is a ScaledGraph with an explicit positive integer scale; the YES/NO bounds compare maxCut / scale in ℝ, and 0 < scale rules out division by zero.
• alphaGW is defined as the sInf of $2\arccos\rho/(\pi(1-\rho))$ over $\rho\in[-1,1)$; this set is nonempty and bounded below, so the infimum is the true constant.
• The reduction is a Turing.TM2ComputableInPolyTime machine with finite tape alphabets, from raw input bits (identity encoding) to ScaledGraph.bits (delimited vertex count and scale, then the full adjacency table); the rational bounds and the machine are fixed before the input.
• The hypothesis $\alpha_{\mathrm{GW}}<\alpha\le1$ is satisfiable, and the conclusion requires an actual strict gap noBound < α * yesBound with 0 < yesBound, so there is no trivial reading. No assumption P ≠ NP is built in.

Welcome contributions: Boolean and Gaussian Fourier analysis (noise stability, influences, Borell's theorem), Majority Is Stablest, the 2-to-1 Games Theorem, and a reusable library for polynomial-time gap reductions on TM2 machines.

Selected references

• OpenAI, A Direct Proof of Optimal Max-Cut Hardness, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Direct-Proof-of-Optimal-Max-Cut-Hardness-September-23-2026/paper.pdf
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42 (1995). https://doi.org/10.1145/227683.227684
• J. Håstad, Some optimal inapproximability results, J. ACM 48 (2001). https://doi.org/10.1145/502090.502098
• L. Trevisan, G. Sorkin, M. Sudan, D. Williamson, Gadgets, approximation, and linear programming, SIAM J. Comput. 29 (2000). https://doi.org/10.1137/S0097539797328847
• S. Khot, G. Kindler, E. Mossel, R. O'Donnell, Optimal inapproximability results for MAX-CUT and other 2-variable CSPs?, SIAM J. Comput. 37 (2007). https://doi.org/10.1137/S0097539705447372
• E. Mossel, R. O'Donnell, K. Oleszkiewicz, Noise stability of functions with low influences: invariance and optimality, Ann. of Math. 171 (2010). https://doi.org/10.4007/annals.2010.171.295
• U. Feige, G. Schechtman, On the optimality of the random hyperplane rounding technique for MAX CUT, Random Structures Algorithms 20 (2002). https://doi.org/10.1002/rsa.10036
• I. Dinur, S. Khot, G. Kindler, D. Minzer, M. Safra, Towards a proof of the 2-to-1 games conjecture?, Theory of Computing 21 (2025). https://doi.org/10.4086/toc.2025.v021a011
• S. Khot, D. Minzer, M. Safra, Pseudorandom sets in Grassmann graph have near-perfect expansion, Ann. of Math. 198 (2023). https://doi.org/10.4007/annals.2023.198.1.1
• S. Khot, On the power of unique 2-prover 1-round games, STOC 2002. https://doi.org/10.1145/509907.510017

Motivation

A Unique Game is a system of constraints between pairs of variables, each constraint saying that the label of one endpoint is a fixed permutation of the label of the other. Deciding whether all constraints can be satisfied is easy (propagate labels along a spanning tree), so the interesting question is approximate: given an instance in which almost all constraints can be satisfied, can a polynomial-time algorithm find a labeling that satisfies even a small fraction?

Khot's Unique Games Conjecture (UGC, 2002) asserts that it cannot, unless P = NP. The conjecture matters because many optimal approximation thresholds have been proved conditionally on it: the Goemans–Williamson ratio for Max-Cut (KKMO 2007), the factor $2$ for Vertex Cover (Khot–Regev 2008), the basic-SDP threshold for every constraint satisfaction problem (Raghavendra 2008), and hardness for ordering, multicut/sparsest-cut and correlation-clustering problems. An unconditional proof would turn all of these into NP-hardness results.

This mission asks for a machine-checked proof of the Unique Games Theorem as stated in an OpenAI preprint dated September 23, 2026 (source), which claims a positive resolution of the conjecture. The preprint has not been peer reviewed, and its claim has not been independently verified; on the platform the Lean goal below is open.

Timeline

• 2001 — Håstad proves optimal inapproximability for linear equations mod 2 with near-perfect completeness (JACM 2001); this gap is the hardness input used by the preprint.
• 2002 — Khot introduces Unique Games and formulates the conjecture (STOC 2002).
• 2005–2008 — Conditional optimal hardness for Max-Cut (Khot, Kindler, Mossel, O'Donnell, SICOMP 2007), Vertex Cover (Khot–Regev, JCSS 2008) and every CSP (Raghavendra, STOC 2008). Khot–Vishnoi build SDP integrality gaps (JACM 2015, FOCS 2005).
• 2005–2010 — Algorithms that delimit the conjecture's quantifiers: Trevisan (ToC 2008), Charikar–Makarychev–Makarychev with value $1-O(\sqrt{\epsilon\log q})$ (STOC 2006), and the subexponential algorithm of Arora–Barak–Steurer (FOCS 2010).
• 2017–2018 — The 2-to-2 Games programme: Khot–Minzer–Safra (STOC 2017; ToC 2025), Dinur–Khot–Kindler–Minzer–Safra (STOC 2018; ToC 2025), Barak–Kothari–Steurer's shortcode formulation (ITCS 2019), and the Grassmann expansion theorem of Khot–Minzer–Safra (Annals 2023). Together these give NP-hardness of Unique Games with completeness near $1/2$ and arbitrarily small soundness.
• 2026 — The OpenAI preprint claims completeness arbitrarily close to $1$, i.e. the full conjecture (Theorem 1.1, p. 2).

Setting

Fix a finite alphabet $K$. An instance $G$ has a finite vertex set and a nonempty list of oriented constraints $e=(u_e,v_e,\pi_e)$ with $\pi_e$ a permutation of $K$; repeated list entries count with multiplicity, and no weights are allowed. A labeling $a$ assigns a label to every vertex and satisfies $e$ when $a(v_e)=\pi_e(a(u_e))$. The value of $a$ is the fraction of satisfied constraints and $\mathrm{val}(G)$ is the maximum over labelings.

An instance is simple bipartite if its vertices split into two sides, every constraint goes from the first side to the second, and no two list entries join the same ordered pair. It is a translation instance over $K=\mathbb F_2^s$ if every constraint has the form $a(v_e)=a(u_e)+c_e$.

3SAT inputs are bit strings decoding to a conjunction of clauses with exactly three literal slots (repeated variables and literals allowed); the input is a YES instance when it decodes to a satisfiable formula.

Formalization targets

Goal: the Unique Games Theorem (Theorem 1.1, p. 2)

For every $\varepsilon,\delta\in(0,1/2)$ there exist $s\ge1$ and a deterministic polynomial-time map $\varphi\mapsto G_\varphi$ to simple bipartite translation instances over $\mathbb F_2^s$ such that

$$\varphi\in\mathrm{3SAT}\;\Longrightarrow\;\mathrm{val}(G_\varphi)\ge 1-\varepsilon,\qquad \varphi\notin\mathrm{3SAT}\;\Longrightarrow\;\mathrm{val}(G_\varphi)\le \delta .$$

The alphabet, the program and the running-time polynomial depend only on $(\varepsilon,\delta)$; the two errors are chosen independently, before the alphabet. In Lean this is OAI.UniqueGamesTheorem.theorem11, which asserts that the structure BinaryGapReduction ε δ is inhabited.

Significance

The result itself. The conjecture is the hypothesis behind a large body of tight approximation thresholds; the preprint's Section 8 (pp. 39–43) records how Theorem 1.1 feeds the earlier reductions for Max-Cut, Vertex Cover, Raghavendra's CSP theorem, ordering CSPs, multicut/sparsest cut and correlation clustering. Those reductions and thresholds are due to their original authors. The statement also fixes the conjecture's quantifier order (errors first, then alphabet), which is exactly what the known algorithms above do not contradict.

Formalizing it. No machine-checked proof of the UGC, or of the 2-to-2 theorem it builds on, is known to exist. A complete development would have to formalize Håstad's parity gap, classical parallel repetition for projection games, the Khot–Minzer–Safra Grassmann/shortcode inverse theorem (used as an external input via Theorem 5.1, p. 22 of the preprint), and the preprint's new latent-alphabet gadget and matrix test. Each of these is reusable well beyond this mission.

Difficulty

The central obstacle, identified in the preprint's introduction (pp. 2–4), is completeness: in a unique constraint every label permits exactly one reply, so the natural codeword tests lose a constant fraction of constraints even on honest proofs. For example, on the rank-one matrix shortcode the evaluation $M\mapsto Mz$ is preserved by a random rank-one update only with probability about $1/2$. The 2-to-2 theorem gives soundness but only near-$1/2$ completeness, and pushing completeness to $1-\varepsilon$ while keeping soundness $\delta$ independent of the alphabet is a separate problem that the earlier programme left open.

Formalization scope

• Instances are Foundations.Target.Instance q over alphabet Fin q, with constraints given by explicit forward/inverse permutation tables and a nonemptiness proof; the value is countSatisfied / constraints.length in ℝ, so division by zero cannot occur.
• The reduction is a Turing.TM2ComputableInPolyTime program from raw input bits (identity encoding, so runtime is measured in the raw input length including sparse variable names) to the bit encoding gameBits; its tape alphabets must be finite.
• coordinates : Fin alphabet ≃ (Fin s → ZMod 2) fixes the $\mathbb F_2^s$ structure, and translations requires every constraint to be a translation in these coordinates; simpleBipartite gives the orientation and the no-parallel-edge condition on list positions.
• The 3SAT language is BinaryLanguage.language: inputs that decode (canonically) to a satisfiable three-slot formula. Malformed inputs are NO instances and must be mapped to low-value games.
• The hypotheses $0<\varepsilon,\delta<1/2$ are satisfiable and the conclusion is a data-carrying structure, so there is no vacuous reading; the completeness clause requires an actual labeling, and soundness quantifies over all labelings.

Welcome contributions: a reusable Lean library for PCP-style gap reductions on TM2 machines, Fourier analysis over $\mathbb F_2^n$, parallel repetition for projection games, and the Grassmann expansion theorem.

Selected references

• OpenAI, The Unique Games Theorem, OpenAI Math Release preprint, September 23, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Unique-Games-Theorem-September-23-2026/paper.pdf
• S. Khot, On the power of unique 2-prover 1-round games, STOC 2002. https://doi.org/10.1145/509907.510017
• S. Khot, On the Unique Games Conjecture, CCC 2010. https://doi.org/10.1109/CCC.2010.19
• S. Khot, G. Kindler, E. Mossel, R. O'Donnell, Optimal inapproximability results for MAX-CUT and other 2-variable CSPs?, SIAM J. Comput. 37 (2007). https://doi.org/10.1137/S0097539705447372
• S. Khot, O. Regev, Vertex cover might be hard to approximate to within 2−ε, J. Comput. Syst. Sci. 74 (2008). https://doi.org/10.1016/j.jcss.2007.06.019
• P. Raghavendra, Optimal algorithms and inapproximability results for every CSP?, STOC 2008. https://doi.org/10.1145/1374376.1374414
• J. Håstad, Some optimal inapproximability results, J. ACM 48 (2001). https://doi.org/10.1145/502090.502098
• B. Barak, P. Kothari, D. Steurer, Small-set expansion in shortcode graph and the 2-to-2 conjecture, ITCS 2019. https://doi.org/10.4230/LIPIcs.ITCS.2019.9
• S. Khot, D. Minzer, M. Safra, Pseudorandom sets in Grassmann graph have near-perfect expansion, Ann. of Math. 198 (2023). https://doi.org/10.4007/annals.2023.198.1.1
• S. Arora, B. Barak, D. Steurer, Subexponential algorithms for Unique Games and related problems, FOCS 2010. https://doi.org/10.1109/FOCS.2010.59

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

Let $G$ be a connected graph and $T$ a set of vertices of even cardinality. A $T$-join is a set of edges $F$ in which exactly the vertices of $T$ have odd degree. A $T$-cut is a cut $\delta(X)$ with $|X\cap T|$ odd. Write $\tau(G,T)$ for the minimum size of a $T$-join and $\nu(G,T)$ for the maximum number of pairwise disjoint $T$-cuts. Every $T$-cut meets every $T$-join, so $\nu(G,T)\le\tau(G,T)$. When equality holds is a central question of combinatorial optimization because of its links to integral multiflows. Seymour (1981) proved equality for all $T$ in bipartite graphs. Middendorf and Pfeiffer (1998) showed that deciding equality is NP-complete.

Korach and Penn (1992) proved that a minimum $T$-join $F$ with $k$ connected components satisfies

$$\tau(G,T)-k+1\ \le\ \nu(G,T)\ \le\ |F|.$$

So a minimum $T$-join with few components certifies a large packing of $T$-cuts, and a connected one certifies $\nu=\tau$. Sebő and Tannier (Math. Oper. Res. 2004) therefore study the problem MTSC: given $G$, $T$ and an integer $k$, is there a minimum $T$-join with at most $k$ connected components? They show it can be solved in polynomial time for $k=1$ and is NP-complete in general (their Theorem 5). The hardness proof reduces three-dimensional matching (3DM) to MTSC. This mission formalizes the correctness of that reduction.

Setting

Three-dimensional matching. An instance consists of three pairwise disjoint sets $W$, $X$, $Y$, each of cardinality $q$, and a set of triples $H\subseteq W\times X\times Y$. A matching is a subset $M\subseteq H$ in which every element of $W\cup X\cup Y$ occurs in exactly one triple.

The graph $G$. Take a further set $Z$ of $q$ points and put $T:=W\cup X\cup Y\cup Z$, so $|T|=4q$. The graph $G$ has as vertices the points of $T$, the triples of $H$, and one new vertex $p_{ab}$ for every unordered pair $\{a,b\}$ of distinct points of $T$. Its edges are:

1. $a\,p_{ab}$ and $p_{ab}\,b$ for every such pair, so any two points of $T$ are joined by a path of length 2;
2. $hw$, $hx$, $hy$ and $hz$ for every $h=(w,x,y)\in H$ and every $z\in Z$.

There are no other edges. In Lean, $G$ is gadget q H and $T$ is gadgetT q H.

$T$-joins and components. For $F\subseteq E(G)$ and a vertex $v$, $\deg_F(v)$ is the number of edges of $F$ at $v$. $F$ is a $T$-join (IsTJoin) if $\deg_F(v)$ is odd exactly for $v\in T$. It is a minimum $T$-join (IsMinTJoin) if no $T$-join of $G$ is smaller. The connected components of $F$ are those of the graph $(V(F),F)$, where $V(F)$ is the set of endpoints of edges of $F$. Their number is numComponents F.

Formalization targets

Goal: the Claim in the proof of Theorem 5 (p. 391)

$$\exists\,F \text{ minimum } T\text{-join of } G \text{ with at most } q \text{ components}\quad\iff\quad \exists\,M\subseteq H \text{ a matching.}$$

This statement is quantified over every $q$ and every $H$, and it is the full mathematical content of the reduction.

Milestones (p. 391, in the order the proof uses them)

1. Every $T$-join $F$ of $G$ has $|F|\ge 4q$, with equality iff each $t\in T$ lies in exactly one edge of $F$.
2. If $M$ is a matching, $Z$ can be indexed as $\{z_m: m\in M\}$, and for every such indexing $\bigcup_{m=(w,x,y)\in M}\{mw,mx,my,mz_m\}$ is a minimum $T$-join with exactly $q$ components.
3. Every minimum $T$-join $F$ has $|F|=4q$, and each $t\in T$ lies in exactly one edge of $F$.
4. Every minimum $T$-join has at least $q$ components. It has exactly $q$ iff each component contains a vertex of $H$ and exactly one vertex of each of $W$, $X$ and $Y$.

Significance

The result. The Claim shows that minimizing the number of components of a minimum $T$-join is NP-hard. A Korach–Penn certificate for a large packing of $T$-cuts therefore cannot in general be found by optimizing the component count. This sets the $k=1$ case, which Sebő and Tannier solve in polynomial time through isometric embeddings of tree metrics, apart from the general case.

Formalizing it. The Claim is proved in the paper, in one paragraph. No machine-checked version is known, and the platform has no $T$-join library. The mission produces a reusable vocabulary for $T$-joins, minimum $T$-joins and the components of an edge set, together with a checked proof that a concrete gadget is correct. One sentence of the published argument is false as written (see Difficulty); a formal proof settles the conclusion independently of it.

Difficulty

The direction from a matching to a $T$-join is a direct verification. The converse has to control an arbitrary minimum $T$-join: its size, the shape of each of its components, and how the components meet $W$, $X$ and $Y$. A first reading of the printed proof suggests that every vertex outside $T$ that carries edges of $F$ is adjacent to at most one vertex of each of $W$, $X$, $Y$. This is false for the inner vertex of a path joining two vertices of the same class, and the construction joins every pair of points of $T$, including pairs inside $W$. Such components really occur in minimum $T$-joins, so the count of components has to cover them as well. The stated conclusion (at least $q$ components, with equality only in the matching-like configuration) remains true.

On the Lean side, the components of an edge set are not the components of the graph with that edge set on all vertices: there every untouched vertex would be a component, and the Claim would become false.

Formalization scope

• 3DM. $W$, $X$, $Y$ are three copies of $\{0,\dots,q-1\}$ (Fin q), so their disjointness holds by construction. $H$ and $M$ are finite sets of triples in Fin q × Fin q × Fin q. IsMatching q M requires each element of each class to be the corresponding coordinate of exactly one triple of $M$, and $M\subseteq H$ is a separate hypothesis. A covering-only or at-most-one version would be a different problem.
• The graph. Its vertex type has three kinds of vertices: $T$-vertices $(i,j)$ with class $i\in\{0,1,2,3\}$ ($W,X,Y,Z$), one midpoint per non-diagonal unordered pair of $T$-vertices, and one vertex per element of $H$. The adjacency is exactly the two bullets of p. 390. The graph is fixed by the definition, not described by properties.
• $T$-joins. Edges are unordered pairs (Sym2) and $F$ is a Finset of edges of $G$. Parity uses $\deg_F$. Minimality is "$|F|\le|F'|$ for all $T$-joins $F'$", never an infimum on $\mathbb N$.
• Components. A component of $F$ is a component of the graph with edge set $F$ that contains an endpoint of an edge of $F$. Isolated vertices are never counted, and the empty edge set has $0$ components.
• The degenerate case $q=0$ is included: the graph is empty, $F=\emptyset$ is a minimum $T$-join with $0$ components, and $M=\emptyset$ is a matching.
• Not formalized. Membership of MTSC in NP, polynomial-time computability of the construction, and NP-completeness itself. The platform has no complexity-theory substrate. The Claim is the mathematical statement those rest on.
• Ruled out. The Claim must not be weakened to "exactly $q$ components" or to minimality among $T$-joins with few components, and components must not be counted on the whole vertex type. Each of these changes the statement.

Contributions welcome: proofs of the milestones, general lemmas on $T$-joins (a $T$-join in a graph where $T$ is independent has at least $|T|$ edges), and lemmas on the components of an edge set, which are reusable well beyond this mission.

Selected references

• A. Sebő, E. Tannier, On Metric Generators of Graphs, Mathematics of Operations Research 29(2):383–393, 2004. https://doi.org/10.1287/moor.1030.0070
• E. Korach, M. Penn, Tight integral duality gap in the Chinese postman problem, Mathematical Programming 55:183–191, 1992.
• P. D. Seymour, On odd cuts and plane multicommodity flows, Proceedings of the London Mathematical Society 42:178–192, 1981.
• M. Middendorf, F. Pfeiffer, On the complexity of the edge-disjoint path problem, Combinatorica (cited by Sebő and Tannier as 1998, vol. 8, pp. 103–116) — NP-completeness of deciding $\nu=\tau$.
• M. R. Garey, D. S. Johnson, Computers and Intractability, W. H. Freeman, San Francisco, 1979 — NP-completeness of 3DM.
• A. Frank, A survey on T-joins, T-cuts, and conservative weightings, in Combinatorics, Paul Erdős is Eighty, Vol. 2, 1996, pp. 213–252.
• Related platform item, not reused: UnrelatedSched.ThreeHalves.ThreeDimMatching (Lenstra–Shmoys–Tardos) encodes 3DM with an indexed family of triples and the covering form of a matching, a different encoding from the paper's set $H$ with "exactly one".

Motivation

Programs often reveal information through the memory locations they touch, even when the contents of those locations are hidden. An oblivious RAM simulation aims to conceal this access pattern. Goldreich and Ostrovsky studied the cost of doing so for arbitrary RAM programs and showed that the access sequence itself imposes a lower bound on simulation overhead. Their 1996 paper gives an upper-bound construction as well as the lower-bound theorem targeted here. The issue matters when a storage observer can see which addresses are accessed but must learn nothing about the program's private requests.

Theorem 6.1 of the paper states that simulating $t$ steps requires at least the initial memory size and, asymptotically, a multiple of $t\log t$ accesses. Its proof introduces a simpler ball-and-cell game that grants the player more information and freedom than the RAM simulation. The mission formalizes that game and its lower bound. This makes the combinatorial content of the published argument a precise theorem about randomized behavior and visible observations. The paper's earlier Theorem 1.2.2 on p. 437 is labeled informal and has a different explicit bound; the target here is Theorem 6.1 on pp. 469–470.

Setting

There are $m$ numbered balls and $m$ numbered cells. Cell $i$ initially contains ball $i$, and a player's hand is empty. Each cell can hold at most one ball and the hand can hold at most $b$ balls. In one access, the player names a cell and secretly takes its ball into a nonfull hand, places one held ball into an empty cell, or leaves the cell unchanged. Taking from an empty cell and placing into an occupied cell are illegal. The observer sees the named cell at each access but not the hidden operation. A run of $q$ accesses is written $a=((v_1,h_1),\ldots,(v_q,h_q))$, and its visible sequence is $V(a)=(v_1,\ldots,v_q)$.

A request sequence $r=(r_1,\ldots,r_t)$ names a ball for each of $t$ rounds. A run satisfies $r$ if it is legal and there are indices $1\le j_1\le\cdots\le j_t=q$ such that ball $r_i$ is in the player's hand after the first $j_i$ accesses. Equal indices are permitted: several rounds may finish after the same access. The player may know the entire request sequence in advance. That assumption is part of the paper's game, and the paper notes that its lower bound does not require an online player.

A randomized player assigns each request sequence a probability distribution over finite runs. It is correct if every run with positive probability satisfies its requests. It is oblivious if the distribution of $V(a)$ is identical for every pair of request sequences of length $t$. Thus the observer cannot infer the requested balls from the accessed cells, even statistically. These conditions quantify over all request sequences, not a selected input or a single deterministic access pattern.

Formalization targets

Theorem 6.1: access lower bound

For every correct oblivious player and every run in the support of its response, the mission targets

$$q\ge m\quad(t\ge1),\qquad q\ge c_b t\log t\quad(m=t,\ t\ge T_b),$$

where $c_b>0$ and $T_b$ depend only on the fixed hand size $b$. This is the paper's $\max\{m,\Omega(t\log t)\}$ form, with $m$ representing the number $|y|$ of initially occupied memory words. It asserts a bound on every possible run, rather than only on average access count. No numerical constant is prescribed by the paper.

Intermediate counting targets

The milestones record the first-round $m$ bound, the at-most-$(b+2)^q$ count of legal hidden action sequences compatible with a visible sequence, and the implication from obliviousness that one visible sequence can serve every request sequence. They then state the corrected finite counting bounds

$$|\{r:a\models r\}|\le\operatorname{multichoose}(q,t)b^t, \qquad m^t\le(b+2)^q\operatorname{multichoose}(q,t)b^t.$$

These preserve the paper's non-strict round ends. The milestone source text records the published formulas, while the formal statements and descriptions identify the corrections.

Significance

The result limits how cheaply a simulator can hide a program's memory access pattern when the observer sees addresses. In the game, a player is even allowed to remember the entire ball placement without cost, know the future requests, and randomize its actions. A lower bound under these permissive conditions applies to the more constrained access-pattern problem that motivated the game, subject to the paper's reduction from simulation to the game. The $m$ term also accounts for the initially occupied memory, independently of the asymptotic term.

The theorem is a published mathematical result, but the mission's Lean declarations are statements with proof holes until solvers supply machine-checked proofs. Formalizing the game creates reusable definitions for legal hidden operations, request satisfaction, randomized players, and visible distributions. Formalizing the corrected counting targets also makes explicit a discrepancy in the printed proof rather than silently relying on an invalid intermediate inequality.

Difficulty

The main difficulty is accounting for requests when several rounds end at the same access. The paper's observation that a fixed $q$-access run serves at most $b^q$ request sequences is false under its own non-strict indices. A run that fetches every ball it can hold may answer many later rounds without making another access. Likewise, the alternative binomial count in footnote 29 assumes distinct completion points and fails when $t>q$. The final asymptotic result still has a valid corrected counting target, but a proof cannot quote the published intermediate formulas literally. Randomized behavior adds another precise requirement: equality of visible distributions must support conclusions about runs with positive probability for each request sequence.

Formalization scope

The Lean carrier is the paper's ball-and-cell game from §6, rather than the interactive RAM machine model of §2. The game relaxes the simulation by giving the player free memory of ball locations and advance knowledge of requests. Balls, cells, and rounds use finite types Fin m and Fin t; these are zero-based encodings of the paper's $[m]$ and round labels. Action steps are counted from one, with the initial state at step zero. PMF represents the player's discrete probability distributions, and equality of PMF.map visible represents observer independence. Every positive-probability run must be legal and satisfy its requests. The visible and hidden sequences have the same finite length $q$.

The two printed estimates $b^q$ and $b^q(b+2)^q>m^t$ are false: with $m=b=q=2$ and $t=7$, taking both balls in two accesses satisfies all $2^7=128$ request sequences, while the printed product is $64$. Footnote 29's $\binom qt b^t$ also vanishes in this example. The formal milestones use Nat.multichoose q t to accommodate repeated round ends; at $q=t=0$ its value is defined directly, so no negative binomial upper index is used. The logarithm in the goal is the natural logarithm, and a threshold $T_b$ handles small $t$.

Correctness and legality are part of the player type, so an unrestricted sequence of cell names cannot satisfy the mission by bypassing the hand and cell rules. Obliviousness uses equality of full distributions, and the goal quantifies over every supported run. The required development includes finite-state transition reasoning, finite combinatorial counts, PMF support and mapping, and real logarithm estimates. These components, especially the game interface and support lemmas, can be reused by later access-pattern formalizations.

Selected references

• Oded Goldreich and Rafail Ostrovsky, Software protection and simulation on oblivious RAMs, Journal of the ACM 43(3):431–473, 1996. DOI: 10.1145/233551.233553. Theorem 6.1 and its proof are on pp. 469–470; the informal Theorem 1.2.2 is on p. 437.

Why multi-level programs are hard

Multi-level programs model a hierarchy of decision makers: a leader commits to a decision, a follower optimises given it, a follower of the follower optimises given both, and so on. Bilevel programs are the standard model of Stackelberg competition, toll setting, network interdiction and many other leader–follower problems in operations research (Candler and Townsley 1982; Bard and Falk 1982). When every level has a linear criterion and the constraints are linear, each player's problem looks like a linear program, and it is natural to hope that the whole hierarchy is solvable in polynomial time.

R. G. Jeroslow's 1985 paper (Math. Programming 32, 146–164) shows that this hope fails at every level of the polynomial hierarchy: a $(p+1)$-level linear program with fixed criteria can encode the truth of a $\Sigma_p$ quantified Boolean sentence. The result places multi-level linear programming in the polynomial hierarchy and is widely cited for the $\Sigma_p$-hardness of such programs; NP-hardness of bilevel linear programs (Corollary 4.6) is its special case $p=1$.

Setting

A multi-level program has real variables $x=(x^1,\dots,x^p)$, a feasible set $S_0$ (a polyhedron $\{x: \sum_i A^ix^i\ge b\}$ in the linear case), and players $p,p-1,\dots,1$ who move in that order; player $i$ controls $x^i$ and minimises a fixed linear criterion $c^ix$. The solution sets are defined from the last mover upwards: $S_1$ is the set of $x\in S_0$ at which player 1's criterion is minimal given the choices of all earlier movers, and in general $S_{j}$ keeps the points of $S_{j-1}$ minimising $c^jx$ among the points of $S_{j-1}$ that agree with $x$ on $x^{j+1},\dots,x^p$. The value is $c^px$ on $S_p$, when $S_p\neq\emptyset$. The sets $S_j$ can be empty even when $S_0$ is a nonempty polytope: the paper's four-level Example has $S_4=\emptyset$ because $S_3$ is not closed.

A propositional formula $F$ over blocks of atoms $X_1,\dots,X_p$ (block $X_k$ has $n_k$ atoms) is encoded by the linear system $L_F$: one variable $x(G)\in[0,1]$ per non-atomic subformula, with the inequalities (3.1a)–(3.1c) for $\vee$, $\wedge$, $\neg$. The quantifier of block $X_k$ is $Q_k=\exists$ when $p-k$ is even, so

$$(\exists X_p)(\forall X_{p-1})\cdots(Q_1X_1)\,[F(X_1,\dots,X_p)=1] \qquad (3.3)$$

is a $\Sigma_p$ sentence.

The game $J'(F)$ adds a bookkeeper, player $0$, who moves last. Player $k\ge1$ controls the atoms of $X_k$, and player $1$ also controls auxiliary variables $y$; the bookkeeper controls the $x(G)$, a variable $u$ fixed to $1$, and auxiliary variables $z$. Two gadgets, (4.1) and (4.6), let the bookkeeper and player 1 turn the linear criteria into the piecewise-linear functions $Z_k=1-x(F)+2\sum_jP(x_{kj})$ (or $x(F)+\dots$ for universal $Q_k$) and $Z_1=(1-x(F))+fr(1-x(F))+10L\sum_j fr(x_{1j})+\dots$, where $L$ is the length of $F$, $fr(x)=\min\{x,1-x\}$, and $P(x)=1$ at $x\in\{0,1\}$, $2$ otherwise.

Formalization targets

Goal: Theorem 4.5 ($p\ge2$)

Let $S$ be the set of optimal solutions $S_{p+1}$ of $J'(F)$. Then $S\neq\emptyset$; at every optimum all atom variables and all $x(G)$ are binary; and

$$x(F)=1 \iff (3.3)\ \text{holds},\qquad \text{value}(J'(F)) = 2n_p+1-x(F).$$

Moreover, when (3.3) holds, $v\in\mathbb R^{n_p}$ is player $p$'s block in some optimum iff $v$ is binary and the $\Pi_{p-1}$ sentence (4.17) holds at the truth valuation of $v$.

Milestones

In attack order: Lemma 3.1 (correctness of $L_F$ on binary inputs); Lemma 4.1 (robustness of $L_F$ near binary inputs); Lemmas 4.2 and 4.3 (the bottom two levels of a bounded linear multi-level program are solvable, via LP duality); the bookkeeper identities $z=|2y-x|$ and $z=fr(x)$ in $S_1$; (4.2) and (4.3) (player 1's and player $k$'s responses on the gadgets); Lemma 4.4 (the induction on $k$ with the higher blocks fixed). Companion theorems: Corollary 4.6 (the bilevel case: value $0$ iff $(\exists X_1)F$), the §2 Example, and Proposition 3.2 (the pure binary game $J(F)$).

Significance

The theorem shows that deciding the value of a $(p+1)$-level linear program with fixed criteria is at least as hard as deciding $\Sigma_p$ sentences, so known exact algorithms for multi-level linear programs cannot be expected to run in polynomial time once $p\ge2$, and even recognising an optimal move is $\Pi_{p-1}$-hard. The bilevel case is an early NP-hardness proof for bilevel linear programming, and the construction (a bookkeeper player and absolute-value gadgets that force binary choices) is a template for hardness reductions to leader–follower problems.

The result is proved in the paper but, to our knowledge, has no machine-checked formalization. A formal development makes precise the solution concept (conditional rather than lexicographic minimisation), which the literature states in several inequivalent ways, and checks a proof whose printed version leaves cases to the reader (the $\wedge$, $\neg$ cases of Lemma 4.1, the universal cases of Lemma 4.4) and applies Lemma 4.3 to a feasible set that is unbounded (the (4.1) variable $z$ has no upper bound).

Difficulty

The obvious argument, "each existential player picks a satisfying assignment and each universal player a counterexample", works for the pure binary game $J(F)$ (Proposition 3.2) but not for continuous variables: a player may choose fractional values, and the solution sets of a multi-level program need not exist (the §2 Example). The work is in showing that every player is forced to binary choices. Player 1's fractional choices are ruled out only through the robustness estimate of Lemma 4.1 with the weight $10L$, and the existence of optimal solutions at every level has to be established along the induction, since it fails for general three-level programs.

Formalization scope

• Players are indexed from $0$; player $i$ optimises at level $i+1$. In $J'(F)$ the players are $0,\dots,p$ as in the paper; in the §2 Example and in $J(F)$ the paper's player $i$ is index $i-1$. Blocks are 0-based: block k : Fin p is the paper's $X_{k+1}$, owned by player $k+1$ in $J'(F)$.
• solSet encodes the conditional minimisation of (3.7), p. 152. HasValue N w requires $S_N\neq\emptyset$; the value $+\infty$ is not modelled.
• Formulas use $\neg,\wedge,\vee$ (the paper rewrites $\to$ as $\neg G_1\vee G_2$); the length counts atoms and connectives. Data are real; the paper's rationality assumption plays no role in the statements.
• The bookkeeper controls the $x(G)$ and has criterion "$+z$ on (4.1) gadgets, $-z$ on (4.6) gadgets, and $+x(G)$ for each non-atomic subformula," as stated on p. 155. The (4.1) variable $z$ has no upper bound. The constant $1$ of (4.4)/(4.7) is the variable $u$ with $u=1$.
• "Binary value, zero iff $F\in B_p$" is stated exactly: the value is $2n_p+1-x(F)$, and $x(F)=1$ iff (3.3). "All optimal solutions are binary" covers the atom variables and the $x(G)$, not the gadget variable $z$, which equals $2$ at $y=1$, $\xi=0$.
• The goal is not trivialisable: its first conjunct asserts that the optimal set is nonempty, which fails for general multi-level programs (the §2 Example), so the remaining conjuncts are not vacuous.

A complete development needs a linear-programming duality argument for Lemma 4.2 (Mathlib has IsExtreme and Set.extremePoints; LP duality is on the platform as a single-level theorem) and an induction over the levels of the game. The definitions MultilevelProgram, solSet and the formula encoding LSys are reusable for other complexity results on hierarchical optimisation. Proofs of any milestone, including the generic Lemmas 4.2–4.3 and the formula Lemmas 3.1 and 4.1, are welcome independently.

Selected references

• R. G. Jeroslow, The polynomial hierarchy and a simple model for competitive analysis, Mathematical Programming 32 (1985) 146–164. https://doi.org/10.1007/BF01586088
• W. Candler and R. Townsley, A linear two-level programming problem, Computers & Operations Research 9 (1982) 59–76. https://doi.org/10.1016/0305-0548(82)90006-5
• J. F. Bard and J. E. Falk, An explicit solution to the multi-level programming problem, Computers & Operations Research 9 (1982) 77–100. https://doi.org/10.1016/0305-0548(82)90007-7
• L. J. Stockmeyer, The polynomial-time hierarchy, Theoretical Computer Science 3 (1976) 1–22. https://doi.org/10.1016/0304-3975(76)90061-X

Motivation

A Markov decision process is the standard model of sequential decision making under uncertainty: a controller observes the state of a finite system, chooses a decision, pays a cost, and the system moves to a random next state. In many applications (maintenance, inventory with unreliable records, robotics, medical treatment) the controller does not see the state itself, only partial information about it. This is the partially observed problem, and the usual way to solve it is to replace the state by the conditional distribution of the state given the observations (Åström 1965; Bertsekas). That reformulation has an infinite state space, and Smallwood and Sondik (1973) showed that the finite-horizon cost-to-go is nevertheless piecewise linear, but with a number of pieces that may grow exponentially with the horizon.

Papadimitriou and Tsitsiklis (Math. Oper. Res. 12(3), 1987) asked whether this blow-up is an artefact of the reformulation or intrinsic to the problem. Their Theorem 6 answers it: deciding whether a partially observed process can achieve a given expected cost is PSPACE-hard, already for stationary processes and horizons shorter than the number of states. This mission formalizes the reduction behind that theorem.

Setting

A partially observed stationary Markov decision process has a finite state set $S$, a partition $\Pi$ of $S$, and an initial state $s_0$. For a state $s$ write $z(s) \in \Pi$ for the set containing it. Each set $z$ carries a nonempty finite set $D_z$ of decisions; decision $i \in D_z$ costs $c(z, i)$ and moves a current state $s \in z$ to the next state $s'$ with probability $p(s, s', i)$. The controller sees only the sequence of sets visited, so a policy $\pi$ maps each observation sequence $z_0, \dots, z_t$ to a decision in $D_{z_t}$. For a horizon $T$, the expected cost of $\pi$ is

$$J_\pi(T) = \mathbb{E}_\pi\Bigl[\sum_{t=0}^{T} c\bigl(z(s_t), \pi(z(s_0), \dots, z(s_t))\bigr)\Bigr],$$

and the optimal cost is $\inf_\pi J_\pi(T)$.

A quantified Boolean formula is $Q_1 x_1 \cdots Q_n x_n\, F(x_1, \dots, x_n)$ with each $Q_j \in \{\exists, \forall\}$ and $F$ a conjunction of $m$ clauses $C_1, \dots, C_m$, each a set of literals $x_j$ or $\neg x_j$. It is true if there is a value of $x_1$ such that for all values of $x_2$, and so on, $F$ comes out true. Deciding truth (QSAT) is PSPACE-complete (Stockmeyer and Meyer 1973).

From a formula with $m \ge 1$ clauses the paper builds a process $M_\varphi$: an initial state, six states $A_{ij}, A'_{ij}, T_{ij}, T'_{ij}, F_{ij}, F'_{ij}$ per clause $i$ and variable $j$, end states $A_{i,n+1}, A'_{i,n+1}$, and one absorbing state, so $|S| = 6mn + 2m + 2$. The first transition chooses a clause uniformly; primed states record that the chosen clause is not yet satisfied; existential variables are set by decisions and universal ones by fair coins; the only nonzero cost, $1$, is paid at $A'_{i,n+1}$. The horizon is $T = 2n + 2$.

Formalization targets

Goal: the reduction is correct

For every formula $\varphi$ in the paper's QSAT class (an alternating prefix beginning with $\exists x_1$ and ending with $\forall x_n$, and three literals per clause), with $m \ge 1$ clauses and $T = 2n+2$,

$$T < |S|, \qquad \bigl(\exists \pi:\ J_\pi(T) = 0\bigr) \iff \varphi \text{ is true}, \qquad \inf_\pi J_\pi(T) \le 0 \iff \varphi \text{ is true}.$$

The goal states all three claims the paper makes: the horizon bound (p. 448), the existence of a zero-cost policy (p. 449), and the bound on the optimum (p. 448).

Milestones

1. The cost splits over the clause chosen at time 1: each clause is chosen with probability $1/m$, and a policy has zero expected cost iff it has zero cost for every choice of clause.
2. If a trajectory of positive probability ends in $A'_{i,n+1}$, the expected cost is at least $2^{-n}/m$.
3. A zero-cost policy makes the formula true.
4. A true formula yields a zero-cost policy.

Significance

Theorem 6 locates the partially observed finite-horizon problem in the complexity landscape: unless P = PSPACE there is no polynomial-time algorithm for it, even for stationary processes with short horizons. The paper's Corollary 1 strengthens this into evidence that no polynomial-size precomputed controller exists either. Together these results explain why exact algorithms for partially observed processes are exponential and motivated the later work on approximation and on restricted policy classes.

The formalization adds a machine-checked proof of the correctness of the reduction, the step on which the hardness claim rests, together with a reusable definition of a finite partially observed process with observation-history policies and of quantified Boolean formulas. The paper's argument is a short paragraph; a formal proof has to make precise how a policy that only sees observation sequences determines a strategy for the existential player. As far as we know, no machine-checked proof of this reduction exists.

Difficulty

The "if" direction is a direct translation of a winning strategy into a policy. The "only if" direction is where the work is. A zero-cost policy acts on observation sequences, and the paper argues that it never learns which clause was chosen. Under the paper's own partition this is not literally true: the sets $T_j$ and $T'_j$ differ, so the observations reveal whether the chosen clause was already satisfied. The existential strategy must therefore be extracted from the policy's behaviour on the observation histories in which the clause is still unsatisfied, and one must check that it is a single strategy, independent of the clause, that satisfies every clause against every choice of the universal variables. The bound of milestone 2 also requires tracking the probability of a single trajectory through the coin flips.

Formalization scope

The process is a Lean structure POMDP S Z with an observation map obs : S → Z encoding the partition, nonempty finite decision types D z, real costs c z i, and next-state laws given as Mathlib PMFs, so every transition row is a probability vector. A policy is a function List Z → (z : Z) → D z of the earlier observations and the current one. The expected cost is a finite sum over trajectories $x_0, \dots, x_T$ of their probability times $\sum_{t=0}^{T} c$, and the optimum is the infimum over all policies. Paper clause $C_i$ and variable $x_j$ are Lean indices $i - 1$ and $j - 1$.

Choices made explicit:

• Horizon. The paper prints $T = 2m + 2$ but says it is "just enough time for the process to reach one of $A_{i,n+1}$ or $A'_{i,n+1}$", which happens at time $2n+1$. With the printed value and $m < n$ the cost is never paid and every formula would map to a zero-cost process. We use $T = 2n+2$.
• The set $A_j$. The partition sentence puts all $A_{ij}$ and $A'_{ij}$ in one set $A_j$; the decision sentence mentions "the set $A'_j$". We follow the partition sentence.
• The new state reached from $A_{i,n+1}$ and $A'_{i,n+1}$ is unspecified; it gets its own set, one zero-cost decision and a self-loop.
• Formulas. The general QBF definition allows any quantifier prefix and clause width. Every theorem assumes IsPaperQSAT, which requires the paper's alternating prefix $\exists x_1 \forall x_2 \cdots \forall x_n$ with $n>0$ even and three literals per clause. Clauses are sets of literals; three witnesses allow repetitions. $m \ge 1$ is also a hypothesis.
• Decisions are nonempty; rows are probability vectors.

Policies see only observation sequences. A formalization in which the policy reads the state would make the "only if" direction false and the reduction meaningless; one in which it sees only the current observation would make the "if" direction false. Neither is admissible.

Not formalized: PSPACE-hardness itself (Mathlib has no PSPACE or polynomial-time reductions), the polynomial-time computability of the construction, the membership of the problem in PSPACE (sketched on p. 449), Corollary 1 (a $\Sigma_2^p$ collapse) and Corollary 2 (NP-completeness of the unobserved case, stated without proof).

The definitions of partially observed processes and quantified Boolean formulas are reusable. Contributions of lemmas on trajectory sums (marginalising later coordinates, the probability of a fixed prefix) are welcome; they also serve the other missions of this series.

Selected references

• C. H. Papadimitriou and J. N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 1987, 441–450. https://doi.org/10.1287/moor.12.3.441
• L. J. Stockmeyer and A. R. Meyer, Word problems requiring exponential time, Proc. 5th ACM STOC, 1973, 1–9. https://doi.org/10.1145/800125.804029
• R. D. Smallwood and E. J. Sondik, The optimal control of partially observable Markov processes over a finite horizon, Operations Research 21(5), 1973, 1071–1088. https://doi.org/10.1287/opre.21.5.1071
• K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10, 1965, 174–205. https://doi.org/10.1016/0022-247X(65)90154-X
• D. P. Bertsekas, Dynamic Programming: Deterministic and Stochastic Models, Prentice-Hall, 1987.