Prove2Me

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

Complexity Theory

136 missions · 53 completed

Missions

Graph TheoryTheoretical Computer Science·Captain: wurtle

Constant-factor hardness of directed feedback vertex setResearch Paper

Motivation

A directed feedback vertex set of a finite digraph GG is a set FF of vertices meeting every directed cycle, equivalently one whose removal leaves G−FG-F acyclic; DFVS(G)\mathrm{DFVS}(G) is the minimum size of such a set. The problem arises wherever cyclic dependencies must be broken — deadlock resolution, circuit testing, scheduling — and a topological order of G−FG-F certifies a solution in polynomial time.

The best general approximation guarantee is O(log⁡nlog⁡log⁡n)O(\log n\log\log n), originating in Seymour's work on fractional packing of directed circuits (Combinatorica 1995) and made constructive by Even, Naor, Schieber and Sudan (Algorithmica 1998). On the hardness side, NP-hardness was known only for particular constants (via Vertex Cover), while ruling out every constant factor required the Unique Games Conjecture. Whether a constant-factor approximation exists under P ≠ NP alone was open.

This mission asks for a machine-checked proof that approximating DFVS within any fixed factor A≥1A\ge1 is NP-hard on unweighted digraphs, as claimed in an OpenAI preprint dated September 23, 2026 (source, Theorem 1.1, p. 2). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Timeline

  • 1995–1998 — Seymour's fractional packing bound (Combinatorica 1995) and the algorithm of Even–Naor–Schieber–Sudan (Algorithmica 1998) give O(log⁡nlog⁡log⁡n)O(\log n\log\log n) approximation.
  • 2005 — Dinur and Safra prove Vertex Cover NP-hard below 105−21≈1.3610\sqrt5-21\approx1.36 (Annals 2005); doubling each undirected edge transfers this to DFVS.
  • 2008–2011 — Guruswami, Manokaran and Raghavendra show every constant factor is Unique-Games-hard via maximum acyclic subgraph and feedback arc set (FOCS 2008); expanded with Håstad and Charikar (SICOMP 2011).
  • 2013 — Svensson's direct Unique-Games-based construction for vertex deletion problems (ToC 2013).
  • 2016 — Guruswami and Lee give a simpler UG-based proof (ToC 2016).
  • 2018–2025 — The imperfect-completeness 2-to-1 Games Theorem is completed (Dinur–Khot–Kindler–Minzer–Safra, ToC 2025; Barak–Kothari–Steurer, ITCS 2019; Khot–Minzer–Safra, ECCC TR18-006), giving Vertex Cover, hence DFVS, hardness below 2\sqrt2.
  • 2026 — Ghorbani and Mnich record the gap for general digraphs (ICALP 2026); the OpenAI preprint claims NP-hardness for every constant factor.

Setting

A digraph is finite and loopless, given by a vertex count nn and a duplicate-free list of arcs (u,v)(u,v) with u≠vu\ne v; opposite arcs (u,v),(v,u)(u,v),(v,u) are allowed. A directed cycle is a cyclic sequence of r+1≥2r+1\ge2 distinct vertices with every successive arc present, including the closing one. FF is a feedback set if it meets every directed cycle, and DFVS(G)\mathrm{DFVS}(G) is the least size of one.

A language L⊆{0,1}∗L\subseteq\{0,1\}^* is in NP if there are a polynomial pp and a deterministic polynomial-time verifier VV (a multi-stack Turing machine with finite alphabets) with x∈Lx\in L iff some certificate ww with ∣w∣≤p(∣x∣)|w|\le p(|x|) makes V(x,w)V(x,w) accept.

Formalization targets

Goal: constant-factor hardness (Theorem 1.1, p. 2)

For every real A≥1A\ge1 and every language L∈NPL\in\mathrm{NP} there is a deterministic polynomial-time map x↦(Gx,kx)x\mapsto(G_x,k_x) with kx≥1k_x\ge1 such that

x∈L ⇒ DFVS(Gx)≤kx,x∉L ⇒ DFVS(Gx)>A kx.x\in L\ \Rightarrow\ \mathrm{DFVS}(G_x)\le k_x,\qquad x\notin L\ \Rightarrow\ \mathrm{DFVS}(G_x)>A\,k_x .

In Lean this is OAI.DirectedFeedback.main : DirectedFeedback.MainStatement. The preprint states Theorem 1.1 as a reduction from an NP-hard promise problem (the 2-to-1 game gap of Theorem 2.1, p. 5) to (G,k)(G,k); composing with that promise problem's NP-hardness gives the Lean form, which quantifies over all NP languages directly. A deterministic polynomial-time AA-approximation would then decide every NP language (proof of Theorem 1.1, p. 28).

The preprint also proves Corollary 8.3 (p. 28) for directed feedback arc set; it is not formalized on the platform.

Significance

The result itself. Theorem 1.1 shows that a constant-factor approximation for DFVS exists if and only if P = NP, removing the Unique Games hypothesis from the Guruswami–Manokaran–Raghavendra and Svensson results. It does not determine the true growth of the optimal factor between constants and O(log⁡nlog⁡log⁡n)O(\log n\log\log n).

Formalizing it. No machine-checked inapproximability result of this kind is known to exist. A complete development needs the 2-to-1 Games Theorem with imperfect completeness (Theorem 2.1, p. 5, external input), Friedgut's junta theorem in a dyadic fixed-bias form (Theorem 2.2 and Corollary 2.3, p. 6), finite Ramsey theory and von Neumann's minimax theorem, and the preprint's rank-graph construction (Definition 3.1, p. 8; Proposition 3.7, p. 12), pivotality budget (Definition 6.1, p. 20) and weighted soundness (Proposition 7.4, p. 25). An NP and Karp-reduction library on TM2 machines (including Cook–Levin) would be reusable across the whole family of hardness missions.

Difficulty

The central difficulty (Introduction, pp. 3–4) is extracting a game labeling from an arbitrary acyclic remainder: a topological order exists, but it can interleave the many vertices representing one local test arbitrarily. Comparisons in that order must first be made consistent and then read as Boolean functions; Friedgut-type junta bounds must hold at many biases simultaneously for the same random function, so a separate influence bound at each scale does not suffice. The coordinate lists must also be fixed before the tested game edge is drawn, or they do not define a game labeling. Gadget reductions from Vertex Cover cannot go beyond the Vertex Cover constants.

Formalization scope

  • DirectedFeedback.Digraph: n : ℕ, a Nodup list of arcs in Fin n × Fin n, loopless; cycles are injective maps Fin (r+1) → Fin n with all successive arcs (including the wrap-around) present, so 2-cycles count and 1-cycles cannot occur. dfvs is the least cardinality of a feedback Finset.
  • NP is defined from scratch by NPVerifier: a polynomial certificate bound and a polynomial-time TM2 verifier with finite alphabets on the unary-framed pair encoding pairBits; no SAT-specific definition is used.
  • GapReduction A L is a polynomial-time TM2 machine (finite alphabets, raw-bit input) producing a GapInstance (digraph plus k > 0), encoded explicitly in unary-framed form by GapInstance.bits; completeness and soundness are as displayed, with soundness compared in ℝ.
  • The statement quantifies over all NP languages, so its proof must include (or reprove) NP-hardness of the source promise problem in this machine model — e.g. a Cook–Levin theorem for TM2 verifiers plus the 2-to-1 Games reduction.
  • k > 0 and the strict inequality rule out a trivial reading (e.g. empty graphs with k = 0).

Welcome contributions: Friedgut's junta theorem, finite Ramsey and minimax in usable forms, the 2-to-1 Games Theorem, and Cook–Levin for Turing.TM2ComputableInPolyTime.

Selected references

2 thms1 active userReviewed
Graph TheoryTheoretical Computer Science·Captain: wurtle

Constant-factor hardness of Min-UnCutResearch Paper

Motivation

Min-UnCut asks, for a finite simple graph G=(V,E)G=(V,E), for the minimum number of edges whose deletion makes GG bipartite. Equivalently, for a bipartition V=S⊔(V∖S)V=S\sqcup(V\setminus S) let UncutG(S)\mathrm{Uncut}_G(S) count the edges with both endpoints on the same side, and set OPTuncut(G)=min⁡SUncutG(S)\mathrm{OPT}_{\mathrm{uncut}}(G)=\min_S\mathrm{Uncut}_G(S). The quantity measures distance from bipartiteness. Although it equals ∣E∣|E| minus the maximum cut, a good multiplicative approximation for Max-Cut gives nothing multiplicative for Min-UnCut on nearly bipartite graphs, which is exactly the regime of interest.

The best known algorithm (Agarwal, Charikar, Makarychev, Makarychev, STOC 2005) achieves an O(log⁡∣V∣)O(\sqrt{\log|V|}) factor. Before the source preprint, NP-hardness was known only for specific constant factors below about 1.491.49, and hardness for every constant factor was known only under the Unique Games Conjecture.

This mission asks for a machine-checked proof that Min-UnCut has no polynomial-time approximation within any constant factor unless P = NP, as claimed in an OpenAI preprint dated September 23, 2026 (source, Theorem 1.1, p. 2). The preprint has not been peer reviewed and its claim has not been independently verified; on the platform the Lean goal is open.

Timeline

  • 2001 — Håstad's near-satisfiable gap for three-variable parity equations (JACM 2001); combined with parallel repetition (Raz, SICOMP 1998; Holenstein, ToC 2009) it is the preprint's starting point.
  • 2005 — Agarwal, Charikar, Makarychev and Makarychev give O(log⁡n)O(\sqrt{\log n}) approximations for Min-UnCut and Min 2CNF Deletion (STOC 2005).
  • 2007 — Under the Unique Games Conjecture, the near-satisfiable Max-Cut gap of Khot, Kindler, Mossel and O'Donnell implies arbitrarily large constant gaps for weighted Min-UnCut (SICOMP 2007).
  • 2017 — Håstad, Huang, Manokaran, O'Donnell and Wright: NP-hard below 11/811/8 for the weighted deletion formulation (ToC 2017).
  • 2018 — Wiman: factors below 1.456851.45685 (KTH master's thesis, 2018).
  • 2024 — Martinsson: factors below 73139148/49096883≈1.4896973139148/49096883\approx1.48969 for violated two-variable parity equations, transferring to weighted Min-UnCut (APPROX/RANDOM 2024).
  • 2026 — The OpenAI preprint claims NP-hardness for every constant factor on simple unweighted graphs.

Setting

A graph is finite, simple, undirected and unweighted, given by a vertex count NN and a symmetric loopless Boolean adjacency table. A cut is a map c:{0,…,N−1}→{0,1}c:\{0,\dots,N-1\}\to\{0,1\}; the parts may be empty or unbalanced. Uncut(c)\mathrm{Uncut}(c) counts unordered edges {u,v}\{u,v\} with c(u)=c(v)c(u)=c(v), and OPTuncut(G)\mathrm{OPT}_{\mathrm{uncut}}(G) is its minimum over all cuts.

3SAT formulas are conjunctions of three-slot clauses over natural-number variable names (repeated variables allowed), given to the reduction by a canonical prefix-free binary encoding.

Formalization targets

Goal: constant-factor hardness (Theorem 1.1, p. 2)

For every fixed integer K≥2K\ge2 there is a deterministic polynomial-time reduction φ↦(G,k)\varphi\mapsto(G,k) to an explicit simple graph GG and a binary integer k≥1k\ge1 with

φ satisfiable⇒OPTuncut(G)≤k,φ unsatisfiable⇒OPTuncut(G)>K k,\varphi\ \text{satisfiable}\Rightarrow \mathrm{OPT}_{\mathrm{uncut}}(G)\le k,\qquad \varphi\ \text{unsatisfiable}\Rightarrow \mathrm{OPT}_{\mathrm{uncut}}(G)>K\,k,

with graph size and running time polynomial in the bit length of φ\varphi for each fixed KK. Choosing K≥CK\ge C shows that a deterministic polynomial-time CC-approximation for any real C>1C>1 would imply P = NP. The positive threshold k≥1k\ge1 is what separates this from bipartiteness testing. In Lean this is OAI.MinUncut.main : Nonempty MinUncut.Reduction.

The preprint also derives Corollary 1.2 (p. 3): minimum 2CNF clause deletion is NP-hard to approximate within every fixed factor C>1C>1. It is not formalized on the platform.

Significance

The result itself. Theorem 1.1 settles the constant-factor approximability of Min-UnCut in the hardness direction without the Unique Games Conjecture, and by an exact cost-preserving transformation the same holds for Min 2CNF Deletion. Together with the O(log⁡n)O(\sqrt{\log n}) algorithm, it places these problems strictly between constant-factor approximable and inapproximable within logarithmic factors (the remaining gap concerns super-constant factors).

Formalizing it. No machine-checked proof of super-constant-type inapproximability for any natural graph problem is known to exist. A complete development needs Håstad's parity gap (Theorem 2.2, p. 6) and uniform parallel repetition (Theorem 2.3, p. 7), used as external inputs, plus the preprint's inner decoding theorem (Theorem 3.2, p. 9), the composition gap for bit comparisons (Proposition 6.1, p. 27) and the finite constructions (Lemmas 7.1 and 7.2, pp. 31 and 34). PCP and parallel-repetition infrastructure would be reusable across many hardness missions.

Difficulty

A natural route is to compose a long-code test with a projection game, as in Håstad's work. The obstacle is extracting a label from an arbitrary folded bit proof with a probability and coefficient size independent of the label alphabet: the alphabet grows as the outer soundness is driven down, and every inner constant must be fixed before it (Introduction, pp. 3–4). In addition, the decoder's choices depend on shared background affine functions, so the outer game's soundness must survive such shared hints. Gadget-based approaches yield only isolated constants (up to about 1.491.49); unbounded constants previously required the Unique Games hypothesis.

Formalization scope

  • MinUncut.Output packages the graph (vertex count, symmetric loopless Bool adjacency) with a threshold threshold ≥ 1; uncut counts pairs u < v that are adjacent and on the same side, and opt is the minimum over all Fin N → Bool cuts (nonempty, so always defined).
  • MinUncut.Reduction is a single TM2 machine taking the pair (K,φ)(K,\varphi) (encoded by inputBits) with finite tape alphabets, a polynomial time K bounding the running time in the formula's bit length, and a polynomial size K bounding vertices plus output length; yes/no hold for every K ≥ 2.
  • The reduction acts on decoded formulas, so malformed inputs do not arise; runtime is measured in formulaBits φ, the canonical encoding including variable names.
  • The hypotheses are satisfiable and the conclusion demands an actual strict multiplicative gap with a positive integer threshold, so outputting a trivially bipartite graph cannot satisfy it.

Welcome contributions: Fourier and Gaussian analysis on F2\mathbb F_2-affine spaces, the long code with folding, parallel repetition for projection games, and Turing-machine complexity infrastructure.

Selected references

2 thms1 active userReviewed
Graph TheoryTheoretical Computer Science·Captain: wurtle

The Factor-Two Hardness Threshold for Vertex CoverResearch Paper

Motivation

A vertex cover of a graph is a set of vertices meeting every edge; τ(G)\tau(G) denotes the minimum size of one. Computing τ(G)\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τ(G)2\tau(G). Whether any polynomial-time algorithm achieves a fixed factor 2−ε2-\varepsilon is one of the best-known questions in approximation algorithms. Unconditional NP-hardness was known below 105−21≈1.3610\sqrt5-21\approx1.36 and, after the 2-to-2 Games Theorem, below 2\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 22.
  • 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/67/6 (JACM 2001).
  • 2005 — Dinur–Safra: NP-hard below 105−21≈1.3606810\sqrt5-21\approx1.36068 (Annals 2005).
  • 2002–2008 — Khot's Unique Games Conjecture (STOC 2002); Khot–Regev prove factor-(2−ε)(2-\varepsilon) hardness assuming it (JCSS 2008).
  • 2009 — Karakostas's algorithm achieves 2−Θ(1/log⁡n)2-\Theta(1/\sqrt{\log n}) (TALG 2009), a saving that vanishes with nn.
  • 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 2\sqrt2.
  • 2026 — The OpenAI preprint claims NP-hardness for every fixed factor below 22.

Setting

A graph is finite, simple, undirected and unweighted, given explicitly by its vertex count nn and a duplicate-free list of edges {u,v}\{u,v\} with u<vu<v. A set SS of vertices is a cover if every edge has an endpoint in SS, and τ(G)\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 α τ(G)\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≥4m\ge4 there is a deterministic polynomial-time reduction φ↦Gφ\varphi\mapsto G_\varphi from 3SAT to explicit simple graphs with

φ satisfiable⇒τ(Gφ)<(12+1m)∣V(Gφ)∣,φ unsatisfiable⇒τ(Gφ)>(1−1m)∣V(Gφ)∣.\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)→22-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≤α<21\le\alpha<2, an α\alpha-approximation algorithm for Vertex Cover yields a polynomial-time 3SAT decider:

∀ α∈[1,2):Approximation(α)  ⟹  ThreeSATDecision.\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 mm from α\alpha and comparing the returned cover with an exact rational threshold. Together with the matching algorithm, it identifies 22 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-22 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/21/2, NO graphs have none of density above 1/m1/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/21-1/\sqrt2 (the 2-to-2 route), which gives factor 2\sqrt2 rather than 22. 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≤α<21\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

3 thms1 active userReviewed
Operations ResearchTheoretical Computer Science·Captain: wurtle

A Direct Proof of Optimal Max-Cut HardnessResearch Paper

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

αGW=min⁡−1≤ρ<12arccos⁡ρπ(1−ρ)=0.878567…\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/1716/17, and optimality of αGW\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 α∈(αGW,1]\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 αGW\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/1716/17.
  • 2002 — Feige and Schechtman show the SDP integrality gap approaches αGW\alpha_{\mathrm{GW}} (RSA 2002); Khot formulates the Unique Games Conjecture (STOC 2002).
  • 2007–2010 — Khot, Kindler, Mossel and O'Donnell prove that αGW\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 αGW\alpha_{\mathrm{GW}}.

Setting

A simple unweighted graph on NN vertices is given by a symmetric, loopless Boolean adjacency table. A cut is a map cc from the vertices to {0,1}\{0,1\}; its size is the number of unordered edges {u,v}\{u,v\} with c(u)≠c(v)c(u)\ne c(v), and MaxCut(G)\mathrm{MaxCut}(G) is the largest cut size. An algorithm is an α\alpha-approximation if it always returns a cut of size at least α⋅MaxCut(G)\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>0Y>0 and N≥0N\ge0 with N<αYN<\alpha Y, and a deterministic polynomial-time map φ↦(Gφ,Qφ)\varphi\mapsto(G_\varphi,Q_\varphi) outputting a graph together with a positive integer scale QφQ_\varphi such that

φ∈3SAT⇒MaxCut(Gφ)Qφ≥Y,φ∉3SAT⇒MaxCut(Gφ)Qφ≤N.\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 NQφN Q_\varphi.

Formalization targets

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

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

∀ α∈(αGW,1]:GapReduction(α)≠∅.\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∈(0,1)t\in(0,1), B(t)=2πarcsin⁡tB(t)=\tfrac{2}{\pi}\arcsin t and 0<ε<(t−B(t))/40<\varepsilon<(t-B(t))/4, it is NP-hard to distinguish Val≥1+t2−ε\mathrm{Val}\ge\frac{1+t}{2}-\varepsilon from Val≤1+B(t)2+ε\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 2arccos⁡ρ/(π(1−ρ))2\arccos\rho/(\pi(1-\rho)) over ρ∈[−1,1)\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 αGW<α≤1\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

2 thms1 active userReviewed
Theoretical Computer Science·Captain: wurtle

The Unique Games TheoremResearch Paper

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 22 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(ϵlog⁡q)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/21/2 and arbitrarily small soundness.
  • 2026 — The OpenAI preprint claims completeness arbitrarily close to 11, i.e. the full conjecture (Theorem 1.1, p. 2).

Setting

Fix a finite alphabet KK. An instance GG has a finite vertex set and a nonempty list of oriented constraints e=(ue,ve,πe)e=(u_e,v_e,\pi_e) with πe\pi_e a permutation of KK; repeated list entries count with multiplicity, and no weights are allowed. A labeling aa assigns a label to every vertex and satisfies ee when a(ve)=πe(a(ue))a(v_e)=\pi_e(a(u_e)). The value of aa is the fraction of satisfied constraints and val(G)\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=F2sK=\mathbb F_2^s if every constraint has the form a(ve)=a(ue)+cea(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 ε,δ∈(0,1/2)\varepsilon,\delta\in(0,1/2) there exist s≥1s\ge1 and a deterministic polynomial-time map φ↦Gφ\varphi\mapsto G_\varphi to simple bipartite translation instances over F2s\mathbb F_2^s such that

φ∈3SAT  ⟹  val(Gφ)≥1−ε,φ∉3SAT  ⟹  val(Gφ)≤δ.\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↦MzM\mapsto Mz is preserved by a random rank-one update only with probability about 1/21/2. The 2-to-2 theorem gives soundness but only near-1/21/2 completeness, and pushing completeness to 1−ε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 F2s\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<ε,δ<1/20<\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 F2n\mathbb F_2^n, parallel repetition for projection games, and the Grassmann expansion theorem.

Selected references

2 thms1 active userReviewed
Machine LearningProbabilityTheoretical Computer Science·Captain: mikedeng1

What Can We Learn Privately? V: Masked Parity Is Learnable by Adaptive but Not by Nonadaptive Statistical Queries Under the Uniform DistributionResearch Paper

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+1d+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 dd, a power of two. The domain is D={0,1}d×{0,1}log⁡d×{0,1}D=\{0,1\}^d\times\{0,1\}^{\log d}\times\{0,1\}, with points u=(x,i,b)u=(x,i,b), and examples are drawn from the uniform distribution D\mathcal D on DD. For r∈{0,1}dr\in\{0,1\}^d and a∈{0,1}a\in\{0,1\}, the concept cr,a:D→{+1,−1}c_{r,a}:D\to\{+1,-1\} is

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

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

A statistical query is a function g(u,y)g(u,y) of an example and a label together with a tolerance τ\tau. The SQ oracle for the target cc answers with any real vv such that ∣v−Eu∼D[g(u,c(u))]∣≤τ|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 ⟨f,h⟩=Eu∼D[f(u)h(u)]\langle f,h\rangle=\mathbb E_{u\sim\mathcal D}[f(u)h(u)] and err(f,h)=Pr⁡u∼D[f(u)≠h(u)]\mathrm{err}(f,h)=\Pr_{u\sim\mathcal D}[f(u)\ne h(u)].

The lower bound uses the decomposition of a query into fg(u)=g(u,1)−g(u,−1)2f_g(u)=\frac{g(u,1)-g(u,-1)}2 and Cg=12E[g(u,1)+g(u,−1)]C_g=\frac12\mathbb E[g(u,1)+g(u,-1)], the restrictions cr,asc^s_{r,a}, fgsf^s_g of cr,ac_{r,a} and fgf_g to the half b=sb=s (equation (6)), and the oracle

Ocr,a,D(g,τ)={Cg+⟨fg1,cr,a1⟩if ∣⟨fg0,cr,a0⟩∣<τ,E[g(u,cr,a(u))]otherwise.\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 (dd queries, then one), with {0,1}\{0,1\}-valued queries of tolerance at least 14d+1\frac1{4d+1}, that outputs cr,ac_{r,a} for every target and every valid answers.
  2. O\mathcal O is a valid SQ oracle, and every nonadaptive learner making tt queries with values ±1\pm1 and tolerance at least 2−d/32^{-d/3}, run against O\mathcal O on a uniformly random target, satisfies
Pr⁡crˉ,aˉ[err(crˉ,aˉ,h)≥14]≥12−t2d/3+2.\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 AMP\mathcal A_{\mathrm{MP}} recovers r^=r\hat r=r and a^=a\hat a=a from every valid answers.
  • Equation (7) (p. 29): E[g(u,cr,a(u))]=Cg+⟨fg0,cr,a0⟩+⟨fg1,cr,a1⟩\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): O\mathcal O is valid and answers identically on cr,0c_{r,0} and cr,1c_{r,1} when ∣⟨fg0,cr,00⟩∣<τ|\langle f^0_g,c^0_{r,0}\rangle|<\tau.
  • Orthogonality (p. 30): ⟨cr,a0,cr′,a0⟩\langle c^0_{r,a},c^0_{r',a}\rangle is 1/21/2 if r=r′r=r' and 00 otherwise.
  • Bessel bound (p. 30): ∑(r,a)2⟨fg0,cr,a0⟩2≤1\sum_{(r,a)}2\langle f^0_g,c^0_{r,a}\rangle^2\le1 for ±1\pm1-valued gg.
  • Counting (p. 30): at most 22d/3−12^{2d/3-1} pairs (r,a)(r,a) have ∣⟨fg0,cr,a0⟩∣≥2−d/3|\langle f^0_g,c^0_{r,a}\rangle|\ge2^{-d/3}.
  • Pr⁡[Good]≥1−t/2d/3+2\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\{0,1\}^d (orthogonality and a Bessel inequality for ±1\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 aa" fails, because the true answer to a query does depend on aa; the argument needs an oracle that is valid (within tolerance of the truth) and yet independent of aa on most targets, and a quantitative bound on how many targets any single ±1\pm1-valued query can correlate with on the half b=0b=0. That bound is an L2L^2 statement over all 2d+12^{d+1} concepts, not a pointwise one.

Formalization scope

  • Domain and distribution. The index i∈{0,1}log⁡di\in\{0,1\}^{\log d} is encoded as Fin d, and every theorem assumes d=2md=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)(r,a) divided by 2d+12^{d+1}.
  • Values. Concepts, hypotheses and queries are real-valued; labels ±1\pm1 are reals. Queries in part (1) take values in {0,1}\{0,1\}, as AMP\mathcal A_{\mathrm{MP}}'s do; queries in part (2) take values ±1\pm1 on labels ±1\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][-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 O\mathcal O and asserts its validity for every τ>0\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. 2d/32^{d/3}, 22d/3−12^{2d/3-1} and 2d/3+22^{d/3+2} are real powers; no natural-number division is used.
  • Corrections of the proof (not of the theorem). The event Good\mathit{Good} on p. 30 is printed with crˉ,aˉc_{\bar r,\bar a} and ≤\le; the milestone uses crˉ,aˉ0c^0_{\bar r,\bar a} and the strict <<, which is what the counting display and the oracle's test require. The quotient 22d/3−1/2d+12^{2d/3-1}/2^{d+1} is printed as 2−d/32^{-d/3} and equals 2−d/3−22^{-d/3-2}; "cr,00=−cr,00c^0_{r,0}=-c^0_{r,0}" should read cr,10=−cr,00c^0_{r,1}=-c^0_{r,0}. The final display of the proof gives 12(1−t/2d/3+2)\frac12(1-t/2^{d/3+2}), which is at least the theorem's bound.

Contributions welcome: the Fourier facts for {0,1}d\{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.
11 thms1 active userReviewed
CombinatoricsGraph TheoryOperations Research·Captain: mikedeng1

On Metric Generators of Graphs 2: The Gadget Graph of a 3-Dimensional Matching Instance Has a Minimum T-Join With at Most q Components Exactly When a Matching ExistsResearch Paper

Motivation

Let GG be a connected graph and TT a set of vertices of even cardinality. A TT-join is a set of edges FF in which exactly the vertices of TT have odd degree. A TT-cut is a cut δ(X)\delta(X) with ∣X∩T∣|X\cap T| odd. Write τ(G,T)\tau(G,T) for the minimum size of a TT-join and ν(G,T)\nu(G,T) for the maximum number of pairwise disjoint TT-cuts. Every TT-cut meets every TT-join, so ν(G,T)≤τ(G,T)\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 TT in bipartite graphs. Middendorf and Pfeiffer (1998) showed that deciding equality is NP-complete.

Korach and Penn (1992) proved that a minimum TT-join FF with kk connected components satisfies

τ(G,T)−k+1 ≤ ν(G,T) ≤ ∣F∣.\tau(G,T)-k+1\ \le\ \nu(G,T)\ \le\ |F|.

So a minimum TT-join with few components certifies a large packing of TT-cuts, and a connected one certifies ν=τ\nu=\tau. Sebő and Tannier (Math. Oper. Res. 2004) therefore study the problem MTSC: given GG, TT and an integer kk, is there a minimum TT-join with at most kk connected components? They show it can be solved in polynomial time for k=1k=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 WW, XX, YY, each of cardinality qq, and a set of triples H⊆W×X×YH\subseteq W\times X\times Y. A matching is a subset M⊆HM\subseteq H in which every element of W∪X∪YW\cup X\cup Y occurs in exactly one triple.

The graph GG. Take a further set ZZ of qq points and put T:=W∪X∪Y∪ZT:=W\cup X\cup Y\cup Z, so ∣T∣=4q|T|=4q. The graph GG has as vertices the points of TT, the triples of HH, and one new vertex pabp_{ab} for every unordered pair {a,b}\{a,b\} of distinct points of TT. Its edges are:

  1. a paba\,p_{ab} and pab bp_{ab}\,b for every such pair, so any two points of TT are joined by a path of length 2;
  2. hwhw, hxhx, hyhy and hzhz for every h=(w,x,y)∈Hh=(w,x,y)\in H and every z∈Zz\in Z.

There are no other edges. In Lean, GG is gadget q H and TT is gadgetT q H.

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

Formalization targets

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

∃ F minimum T-join of G with at most q components  ⟺  ∃ M⊆H a matching.\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 qq and every HH, and it is the full mathematical content of the reduction.

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

  1. Every TT-join FF of GG has ∣F∣≥4q|F|\ge 4q, with equality iff each t∈Tt\in T lies in exactly one edge of FF.
  2. If MM is a matching, ZZ can be indexed as {zm:m∈M}\{z_m: m\in M\}, and for every such indexing ⋃m=(w,x,y)∈M{mw,mx,my,mzm}\bigcup_{m=(w,x,y)\in M}\{mw,mx,my,mz_m\} is a minimum TT-join with exactly qq components.
  3. Every minimum TT-join FF has ∣F∣=4q|F|=4q, and each t∈Tt\in T lies in exactly one edge of FF.
  4. Every minimum TT-join has at least qq components. It has exactly qq iff each component contains a vertex of HH and exactly one vertex of each of WW, XX and YY.

Significance

The result. The Claim shows that minimizing the number of components of a minimum TT-join is NP-hard. A Korach–Penn certificate for a large packing of TT-cuts therefore cannot in general be found by optimizing the component count. This sets the k=1k=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 TT-join library. The mission produces a reusable vocabulary for TT-joins, minimum TT-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 TT-join is a direct verification. The converse has to control an arbitrary minimum TT-join: its size, the shape of each of its components, and how the components meet WW, XX and YY. A first reading of the printed proof suggests that every vertex outside TT that carries edges of FF is adjacent to at most one vertex of each of WW, XX, YY. 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 TT, including pairs inside WW. Such components really occur in minimum TT-joins, so the count of components has to cover them as well. The stated conclusion (at least qq 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. WW, XX, YY are three copies of {0,…,q−1}\{0,\dots,q-1\} (Fin q), so their disjointness holds by construction. HH and MM 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 MM, and M⊆HM\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: TT-vertices (i,j)(i,j) with class i∈{0,1,2,3}i\in\{0,1,2,3\} (W,X,Y,ZW,X,Y,Z), one midpoint per non-diagonal unordered pair of TT-vertices, and one vertex per element of HH. The adjacency is exactly the two bullets of p. 390. The graph is fixed by the definition, not described by properties.
  • TT-joins. Edges are unordered pairs (Sym2) and FF is a Finset of edges of GG. Parity uses deg⁡F\deg_F. Minimality is "∣F∣≤∣F′∣|F|\le|F'| for all TT-joins F′F'", never an infimum on N\mathbb N.
  • Components. A component of FF is a component of the graph with edge set FF that contains an endpoint of an edge of FF. Isolated vertices are never counted, and the empty edge set has 00 components.
  • The degenerate case q=0q=0 is included: the graph is empty, F=∅F=\emptyset is a minimum TT-join with 00 components, and M=∅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 qq components" or to minimality among TT-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 TT-joins (a TT-join in a graph where TT is independent has at least ∣T∣|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 HH with "exactly one".
8 thms1 active userReviewed
CombinatoricsProbabilityTheoretical Computer Science·Captain: mikedeng1

Software Protection and Simulation on Oblivious RAMs: Every Oblivious Simulation of t Steps Makes max{|y|, Ω(t log t)} AccessesResearch Paper

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 tt steps requires at least the initial memory size and, asymptotically, a multiple of tlog⁡tt\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 mm numbered balls and mm numbered cells. Cell ii initially contains ball ii, and a player's hand is empty. Each cell can hold at most one ball and the hand can hold at most bb 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 qq accesses is written a=((v1,h1),…,(vq,hq))a=((v_1,h_1),\ldots,(v_q,h_q)), and its visible sequence is V(a)=(v1,…,vq)V(a)=(v_1,\ldots,v_q).

A request sequence r=(r1,…,rt)r=(r_1,\ldots,r_t) names a ball for each of tt rounds. A run satisfies rr if it is legal and there are indices 1≤j1≤⋯≤jt=q1\le j_1\le\cdots\le j_t=q such that ball rir_i is in the player's hand after the first jij_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)V(a) is identical for every pair of request sequences of length tt. 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≥m(t≥1),q≥cbtlog⁡t(m=t, t≥Tb),q\ge m\quad(t\ge1),\qquad q\ge c_b t\log t\quad(m=t,\ t\ge T_b),

where cb>0c_b>0 and TbT_b depend only on the fixed hand size bb. This is the paper's max⁡{m,Ω(tlog⁡t)}\max\{m,\Omega(t\log t)\} form, with mm representing the number ∣y∣|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 mm bound, the at-most-(b+2)q(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⊨r}∣≤multichoose⁡(q,t)bt,mt≤(b+2)qmultichoose⁡(q,t)bt.|\{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 mm 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 qq-access run serves at most bqb^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>qt>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][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 qq.

The two printed estimates bqb^q and bq(b+2)q>mtb^q(b+2)^q>m^t are false: with m=b=q=2m=b=q=2 and t=7t=7, taking both balls in two accesses satisfies all 27=1282^7=128 request sequences, while the printed product is 6464. Footnote 29's (qt)bt\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=0q=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 TbT_b handles small tt.

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.
7 thms1 active userReviewed
Algorithmic Game TheoryLinear OptimizationOperations Research·Captain: mikedeng1

The Polynomial Hierarchy and a Simple Model for Competitive Analysis: Every Optimum of the (p+1)-Level Linear Game J'(F) Is Binary, with x(F) = 1 iff the Σ_p Sentence (3.3) HoldsResearch Paper

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)(p+1)-level linear program with fixed criteria can encode the truth of a Σp\Sigma_p quantified Boolean sentence. The result places multi-level linear programming in the polynomial hierarchy and is widely cited for the Σp\Sigma_p-hardness of such programs; NP-hardness of bilevel linear programs (Corollary 4.6) is its special case p=1p=1.

Setting

A multi-level program has real variables x=(x1,…,xp)x=(x^1,\dots,x^p), a feasible set S0S_0 (a polyhedron {x:∑iAixi≥b}\{x: \sum_i A^ix^i\ge b\} in the linear case), and players p,p−1,…,1p,p-1,\dots,1 who move in that order; player ii controls xix^i and minimises a fixed linear criterion cixc^ix. The solution sets are defined from the last mover upwards: S1S_1 is the set of x∈S0x\in S_0 at which player 1's criterion is minimal given the choices of all earlier movers, and in general SjS_{j} keeps the points of Sj−1S_{j-1} minimising cjxc^jx among the points of Sj−1S_{j-1} that agree with xx on xj+1,…,xpx^{j+1},\dots,x^p. The value is cpxc^px on SpS_p, when Sp≠∅S_p\neq\emptyset. The sets SjS_j can be empty even when S0S_0 is a nonempty polytope: the paper's four-level Example has S4=∅S_4=\emptyset because S3S_3 is not closed.

A propositional formula FF over blocks of atoms X1,…,XpX_1,\dots,X_p (block XkX_k has nkn_k atoms) is encoded by the linear system LFL_F: one variable x(G)∈[0,1]x(G)\in[0,1] per non-atomic subformula, with the inequalities (3.1a)–(3.1c) for ∨\vee, ∧\wedge, ¬\neg. The quantifier of block XkX_k is Qk=∃Q_k=\exists when p−kp-k is even, so

(∃Xp)(∀Xp−1)⋯(Q1X1) [F(X1,…,Xp)=1](3.3)(\exists X_p)(\forall X_{p-1})\cdots(Q_1X_1)\,[F(X_1,\dots,X_p)=1] \qquad (3.3)

is a Σp\Sigma_p sentence.

The game J′(F)J'(F) adds a bookkeeper, player 00, who moves last. Player k≥1k\ge1 controls the atoms of XkX_k, and player 11 also controls auxiliary variables yy; the bookkeeper controls the x(G)x(G), a variable uu fixed to 11, and auxiliary variables zz. Two gadgets, (4.1) and (4.6), let the bookkeeper and player 1 turn the linear criteria into the piecewise-linear functions Zk=1−x(F)+2∑jP(xkj)Z_k=1-x(F)+2\sum_jP(x_{kj}) (or x(F)+…x(F)+\dots for universal QkQ_k) and Z1=(1−x(F))+fr(1−x(F))+10L∑jfr(x1j)+…Z_1=(1-x(F))+fr(1-x(F))+10L\sum_j fr(x_{1j})+\dots, where LL is the length of FF, fr(x)=min⁡{x,1−x}fr(x)=\min\{x,1-x\}, and P(x)=1P(x)=1 at x∈{0,1}x\in\{0,1\}, 22 otherwise.

Formalization targets

Goal: Theorem 4.5 (p≥2p\ge2)

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

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

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

Milestones

In attack order: Lemma 3.1 (correctness of LFL_F on binary inputs); Lemma 4.1 (robustness of LFL_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∣z=|2y-x| and z=fr(x)z=fr(x) in S1S_1; (4.2) and (4.3) (player 1's and player kk's responses on the gadgets); Lemma 4.4 (the induction on kk with the higher blocks fixed). Companion theorems: Corollary 4.6 (the bilevel case: value 00 iff (∃X1)F(\exists X_1)F), the §2 Example, and Proposition 3.2 (the pure binary game J(F)J(F)).

Significance

The theorem shows that deciding the value of a (p+1)(p+1)-level linear program with fixed criteria is at least as hard as deciding Σp\Sigma_p sentences, so known exact algorithms for multi-level linear programs cannot be expected to run in polynomial time once p≥2p\ge2, and even recognising an optimal move is Πp−1\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 zz 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)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 10L10L, 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 00; player ii optimises at level i+1i+1. In J′(F)J'(F) the players are 0,…,p0,\dots,p as in the paper; in the §2 Example and in J(F)J(F) the paper's player ii is index i−1i-1. Blocks are 0-based: block k : Fin p is the paper's Xk+1X_{k+1}, owned by player k+1k+1 in J′(F)J'(F).
  • solSet encodes the conditional minimisation of (3.7), p. 152. HasValue N w requires SN≠∅S_N\neq\emptyset; the value +∞+\infty is not modelled.
  • Formulas use ¬,∧,∨\neg,\wedge,\vee (the paper rewrites →\to as ¬G1∨G2\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)x(G) and has criterion "+z+z on (4.1) gadgets, −z-z on (4.6) gadgets, and +x(G)+x(G) for each non-atomic subformula," as stated on p. 155. The (4.1) variable zz has no upper bound. The constant 11 of (4.4)/(4.7) is the variable uu with u=1u=1.
  • "Binary value, zero iff F∈BpF\in B_p" is stated exactly: the value is 2np+1−x(F)2n_p+1-x(F), and x(F)=1x(F)=1 iff (3.3). "All optimal solutions are binary" covers the atom variables and the x(G)x(G), not the gadget variable zz, which equals 22 at y=1y=1, ξ=0\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

13 thms1 active userReviewed
Dynamic ProgrammingMathematical LogicOperations Research·Captain: mikedeng1

The Complexity of Markov Decision Processes V: A Quantified Boolean Formula Is True Iff Its Partially Observed Markov Decision Process Has a Zero-Cost PolicyResearch Paper

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 SS, a partition Π\Pi of SS, and an initial state s0s_0. For a state ss write z(s)∈Πz(s) \in \Pi for the set containing it. Each set zz carries a nonempty finite set DzD_z of decisions; decision i∈Dzi \in D_z costs c(z,i)c(z, i) and moves a current state s∈zs \in z to the next state s′s' with probability p(s,s′,i)p(s, s', i). The controller sees only the sequence of sets visited, so a policy π\pi maps each observation sequence z0,…,ztz_0, \dots, z_t to a decision in DztD_{z_t}. For a horizon TT, the expected cost of π\pi is

Jπ(T)=Eπ[∑t=0Tc(z(st),π(z(s0),…,z(st)))],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⁡πJπ(T)\inf_\pi J_\pi(T).

A quantified Boolean formula is Q1x1⋯Qnxn F(x1,…,xn)Q_1 x_1 \cdots Q_n x_n\, F(x_1, \dots, x_n) with each Qj∈{∃,∀}Q_j \in \{\exists, \forall\} and FF a conjunction of mm clauses C1,…,CmC_1, \dots, C_m, each a set of literals xjx_j or ¬xj\neg x_j. It is true if there is a value of x1x_1 such that for all values of x2x_2, and so on, FF comes out true. Deciding truth (QSAT) is PSPACE-complete (Stockmeyer and Meyer 1973).

From a formula with m≥1m \ge 1 clauses the paper builds a process MφM_\varphi: an initial state, six states Aij,Aij′,Tij,Tij′,Fij,Fij′A_{ij}, A'_{ij}, T_{ij}, T'_{ij}, F_{ij}, F'_{ij} per clause ii and variable jj, end states Ai,n+1,Ai,n+1′A_{i,n+1}, A'_{i,n+1}, and one absorbing state, so ∣S∣=6mn+2m+2|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, 11, is paid at Ai,n+1′A'_{i,n+1}. The horizon is T=2n+2T = 2n + 2.

Formalization targets

Goal: the reduction is correct

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

T<∣S∣,(∃π: Jπ(T)=0)  ⟺  φ is true,inf⁡πJπ(T)≤0  ⟺  φ is true.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/m1/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 Ai,n+1′A'_{i,n+1}, the expected cost is at least 2−n/m2^{-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 TjT_j and Tj′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 x0,…,xTx_0, \dots, x_T of their probability times ∑t=0Tc\sum_{t=0}^{T} c, and the optimum is the infimum over all policies. Paper clause CiC_i and variable xjx_j are Lean indices i−1i - 1 and j−1j - 1.

Choices made explicit:

  • Horizon. The paper prints T=2m+2T = 2m + 2 but says it is "just enough time for the process to reach one of Ai,n+1A_{i,n+1} or Ai,n+1′A'_{i,n+1}", which happens at time 2n+12n+1. With the printed value and m<nm < n the cost is never paid and every formula would map to a zero-cost process. We use T=2n+2T = 2n+2.
  • The set AjA_j. The partition sentence puts all AijA_{ij} and Aij′A'_{ij} in one set AjA_j; the decision sentence mentions "the set Aj′A'_j". We follow the partition sentence.
  • The new state reached from Ai,n+1A_{i,n+1} and Ai,n+1′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 ∃x1∀x2⋯∀xn\exists x_1 \forall x_2 \cdots \forall x_n with n>0n>0 even and three literals per clause. Clauses are sets of literals; three witnesses allow repetitions. m≥1m \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 Σ2p\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.
8 thms1 active userReviewed
Completed
Combinatorics·Captain: yousofy

Block Sensitivity vs. Sensitivity: Reach 2.1308255793978239…2.1308255793978239\ldotsOpen Problem

Comparing single-coordinate and block changes

A Boolean function can react differently to changing one input coordinate and changing several coordinates together. Measuring this difference is a question about the local complexity of total Boolean functions. The Block Sensitivity vs. Sensitivity campaign records exponents that quantify how large this difference can become along families of functions with increasing sensitivity.

This mission records the exact exponent

α=log⁡(140558)log⁡(3738277295413674)=2.130825579397823947629976285043….\alpha=\frac{\log(14055^8)}{\log(3738277295413674)} =2.130825579397823947629976285043\ldots.

Its construction is already accepted and public. The mission expresses that result using the campaign's shared definition, so that its value can enter the same record as earlier entries. The logarithmic expression is the target; the displayed decimal is an approximation. No optimality claim is part of this mission.

Boolean functions and sensitive blocks

A total Boolean function on nn coordinates is a map f:{0,1}n→{0,1}f:\{0,1\}^n\to\{0,1\}, defined on every binary input. For an input xx and a set BB of coordinates, write x⊕Bx\oplus B for the input obtained by flipping exactly the bits indexed by BB.

A coordinate ii is sensitive at xx if f(x⊕{i})≠f(x)f(x\oplus\{i\})\ne f(x). The sensitivity s(f,x)s(f,x) counts those coordinates, and s(f)s(f) is the maximum of s(f,x)s(f,x) over all inputs. A nonempty coordinate set BB is a sensitive block at xx if f(x⊕B)≠f(x)f(x\oplus B)\ne f(x). The block sensitivity bs⁡(f,x)\operatorname{bs}(f,x) is the largest number of pairwise disjoint sensitive blocks at that input. The quantity bs⁡(f)\operatorname{bs}(f) is its maximum over all inputs.

Every block in one block-sensitivity witness is tested at the same input. The blocks are disjoint as coordinate sets; their sizes need not be equal. These conventions are those of the shared foundation mission, rather than complexity measures defined only on selected inputs or on a promise domain.

Formalization target

The goal is the campaign proposition AchievesExponent⁡(α)\operatorname{AchievesExponent}(\alpha). Explicitly, for every real ε>0\varepsilon>0 and every natural number S≥2S\ge2, there must exist a natural number nn and a total Boolean function f:{0,1}n→{0,1}f:\{0,1\}^n\to\{0,1\} satisfying

s(f)≥S,bs⁡(f)≥s(f)α−ε.s(f)\ge S,\qquad \operatorname{bs}(f)\ge s(f)^{\alpha-\varepsilon}.

Both the dimension and the function may depend on ε\varepsilon and SS. The sensitivity threshold is essential: a favorable ratio for one bounded example does not establish this statement. For example, choosing successively smaller positive losses and increasing thresholds produces a sequence of finite total Boolean functions with unbounded sensitivity and exponents approaching α\alpha.

The exact numerator is the natural number

140558=1522813785050025472152230187890625.14055^8=1522813785050025472152230187890625.

The denominator inside the logarithm is 37382772954136743738277295413674. Both logarithm arguments exceed one. There is no division by a zero logarithm, and the result uses ordinary real powers. The goal does not assume a finite construction certificate or the existence of a suitable labeling as a hypothesis.

Improvement and verification status

The accepted construction theorem also proves the strict comparison

log⁡(140558)log⁡(3738289747988852)<α.\frac{\log(14055^8)}{\log(3738289747988852)}<\alpha.

It improves the earlier public exponent, approximately 2.1303203332203662.130320333220366, by approximately 0.0005052460.000505246. The full proof constructs actual Boolean functions and establishes the asymptotic quantifiers; the numerical approximation alone is not the evidence for the separation.

The complete construction has passed local Lean kernel verification and Prove2Me verification. Its accepted submission is a9d25c46-43bd-4fb1-826b-0ed075b8cf0a. The source uses ordinary checked proofs with the standard axioms propext, Classical.choice, and Quot.sound. Its final statement spells out sensitivity and block sensitivity directly through finite sets. The campaign goal uses the existing shared definitions for those same quantities, and its proof explicitly establishes the equivalence needed to transfer the accepted result.

Why the full statement matters

A lower bound on block sensitivity at one input must be combined with an upper bound on sensitivity over every input. Local calculations that ignore the latter maximum can overstate the separation. Likewise, overlapping sensitive blocks cannot be counted as a disjoint family. These requirements persist through the construction and the passage to arbitrarily large sensitivity.

The exponent also depends on exact integer growth rates. Rounded numerical scores can identify candidates, but they do not establish the final real-power inequality. A complete proof must account for finite construction constraints, the complexity measures of the resulting functions, and the exponent loss allowed in the asymptotic statement. The accepted result includes these steps. This mission records that established result rather than a proposed stronger threshold awaiting construction.

Formalization scope

The development targets Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Inputs are functions Fin n → Bool, and outputs are Bool. Sensitivity and block sensitivity are natural numbers obtained by finite maxima. The campaign proposition quantifies over positive real losses and natural sensitivity thresholds.

Dimension zero is permitted by the representation, but its sensitivity is zero and it cannot witness any required threshold S≥2S\ge2. Empty block families contribute zero; every counted block is nonempty. There are no hypotheses that can make the target vacuous. The shared definition and finite-certificate references are retained from the campaign template. The only new result recorded here is the improved separation exponent and its exact campaign formulation. Attribution to the original OpenAI development and Robin Kothari/Codex is retained in the accepted construction source; the new construction is credited to yousofy with Codex.

Selected references

6 thms0 active usersReviewed