Complexity Theory

Motivation

Sensitivity and block sensitivity are two of the basic complexity measures of a Boolean function $f:\{0,1\}^n\to\{0,1\}$. Sensitivity counts how many single-bit flips change the value; block sensitivity allows disjoint groups of bits to be flipped together. Block sensitivity is polynomially related to decision-tree complexity, certificate complexity, degree and quantum query complexity, so the question of how it compares with sensitivity (the Sensitivity Conjecture, from Nisan's 1989 work on CREW PRAMs) decides whether sensitivity belongs to that same family. Huang's 2019 theorem settled the polynomial question: $\mathrm{bs}(f)\le s(f)^4$. Nisan and Szegedy had suggested the stronger bound $\mathrm{bs}(f)\le s(f)^2$, and the best known separations were quadratic.

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

Background

• 1989 — Nisan introduces block sensitivity and records Rubinstein's quadratic separation (STOC 1989).
• 1994 — Nisan and Szegedy suggest $\mathrm{bs}(f)\le s(f)^2$ (Comput. Complexity 1994).
• 1995 — Rubinstein's function: $\mathrm{bs}(f)=\tfrac12 s(f)^2$ (Combinatorica 1995).
• 2011 — Virza improves to $\tfrac12s^2+\tfrac12s$ (IPL 2011); Ambainis and Sun reach $\tfrac23s^2-\tfrac13s$ (arXiv:1108.3494).
• 2013–2014 — Tal studies composition as an amplification tool (ITCS 2013); Ambainis and Prūsis note that a seed with $\mathrm{bs}>s^2$ would give a superquadratic power separation by iteration (ECCC TR14-027).
• 2019 — Huang proves $\mathrm{bs}(f)\le s(f)^4$ (Annals 2019); Wellens later sharpens the constant (Discrete Analysis 2022).
• 2026 — Meiburg shows block sensitivity can exceed spectral sensitivity squared (arXiv:2608.00851).
• September 2026 — The OpenAI preprint claims $\mathrm{bs}(f)/s(f)^2$ is unbounded, and $\mathrm{bs}\ge s^\alpha$ for a fixed $\alpha>2$.

Setting

For $x\in\{0,1\}^n$ and $B\subseteq[n]$, let $x^B$ be $x$ with the coordinates in $B$ flipped. For a total Boolean function $f$,

$$s(f,x)=\#\{a\in[n]: f(x^{\{a\}})\ne f(x)\},\qquad s(f)=\max_x s(f,x),$$

and $\mathrm{bs}(f,x)$ is the largest number of pairwise disjoint nonempty sets $B_1,\dots,B_m$ with $f(x^{B_j})\ne f(x)$ for every $j$; $\mathrm{bs}(f)=\max_x\mathrm{bs}(f,x)$. Always $s(f)\le\mathrm{bs}(f)$, and a nonconstant $f$ has $s(f)\ge1$.

Formalization targets

Goal: the quantitative form of Theorem 1.1 (p. 2)

For every integer $d\ge1$ there are $n\ge1$ and a nonconstant $f:\{0,1\}^n\to\{0,1\}$ with $f(0,\dots,0)=0$ and

$$\frac{\mathrm{bs}(f)}{s(f)^2}\ \ge\ \frac{2^d}{4(d+2)^2}.$$

Since the right side tends to infinity, for every $C>0$ some nonconstant $f$ has $\mathrm{bs}(f)>C\,s(f)^2$, which is the first sentence of Theorem 1.1. The goal does not include the fixed-exponent statement of Corollary 4.3 (p. 10).

Significance

The result itself. It refutes the quadratic strengthening of the Sensitivity Conjecture suggested by Nisan and Szegedy and leaves the true exponent between $2$ and $4$: Huang's theorem gives $\mathrm{bs}\le s^4$, while Corollary 4.3 of the preprint gives functions with $\mathrm{bs}(f,0)\ge s(f)^\alpha$ for some $\alpha>2$ and unbounded block sensitivity. Because spectral sensitivity is at most sensitivity, the separation also strengthens Meiburg's spectral result.

Formalizing it. The objects are finite and elementary, so a formal proof is a complete certificate of an explicit combinatorial construction. Huang's theorem has been formalized in Lean; a formal proof here would place the lower side of the gap on the same footing.

Difficulty

Known separations compose small gadgets, and composition multiplies both measures in a way that keeps the exponent at $2$. To break it, a recursion must grow the number of disjoint sensitive blocks by a factor $\approx 2M^2$ per level while ordinary sensitivity grows by only $\approx M$. The preprint's nested predicates on a labelled tournament (Section 2) achieve this, but a single bit flip can repair a failed gate condition only by changing two child predicates at once. Controlling sensitivity therefore requires tracking these joint sensitivities alongside ordinary ones at every input, not only at the input where the blocks are found (Proposition 3.1, p. 5), and the random edge labelling must exclude dense local configurations (Lemma 2.1, p. 3).

Formalization scope

• Inputs are Fin n → Bool; flip x B flips the coordinates in a Finset. sensitivity and blockSensitivity are Finset.sup over all inputs of the local counts; block families are finsets of pairwise disjoint nonempty finsets, each of which changes the value.
• The ratio is computed in ℝ. Nonconstancy (∃ x y, f x ≠ f y) forces $s(f)\ge1$, so the division is genuine.
• The extra clause $f(0)=0$ is not in the printed Theorem 1.1, but the constructed function satisfies it (the predicates vanish at zero, Lemma 2.3, p. 5, and the proof of Corollary 4.3 uses $f(0)=0$), so it is a faithful strengthening rather than an added assumption.
• Nothing is vacuous: $d\ge1$ is satisfiable and the conclusion asks for an explicit function.

Welcome contributions: a reusable library of Boolean-function complexity measures (sensitivity, block sensitivity, certificate complexity) and composition lemmas such as Lemma 4.2 (p. 9).

Selected references

• OpenAI, A superquadratic separation between sensitivity and block sensitivity, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-superquadratic-separation-between-sensitivity-and-block-sensitivity-September-25-2026/paper.pdf
• N. Nisan, CREW PRAMs and decision trees, STOC 1989. https://doi.org/10.1145/73007.73038
• N. Nisan, M. Szegedy, On the degree of Boolean functions as real polynomials, Comput. Complexity (1994). https://doi.org/10.1007/BF01263419
• D. Rubinstein, Sensitivity vs. block sensitivity of Boolean functions, Combinatorica (1995). https://doi.org/10.1007/BF01200762
• M. Virza, Sensitivity versus block sensitivity of Boolean functions, Inform. Process. Lett. (2011). https://doi.org/10.1016/j.ipl.2011.02.001
• A. Ambainis, X. Sun, New separation between s(f) and bs(f), arXiv:1108.3494 (2011). https://arxiv.org/abs/1108.3494v1
• A. Tal, Properties and applications of Boolean function composition, ITCS 2013. https://doi.org/10.1145/2422436.2422485
• A. Ambainis, K. Prūsis, A tight lower bound on certificate complexity in terms of block sensitivity and sensitivity, ECCC TR14-027 (2014). https://eccc.weizmann.ac.il/report/2014/027/revision/1/download
• H. Huang, Induced subgraphs of hypercubes and a proof of the Sensitivity Conjecture, Ann. of Math. 190 (2019). https://doi.org/10.4007/annals.2019.190.3.6
• J. Wellens, Relationships between the number of inputs and other complexity measures of Boolean functions, Discrete Analysis (2022). https://doi.org/10.19086/da.57741
• S. Aaronson, S. Ben-David, R. Kothari, et al., Degree vs. approximate degree and quantum implications of Huang's sensitivity theorem, STOC 2021. https://doi.org/10.1145/3406325.3451047
• A. Meiburg, Block sensitivity can exceed spectral sensitivity squared, arXiv:2608.00851 (2026). https://arxiv.org/html/2608.00851v1

Motivation: the state cost of removing nondeterminism with two-way motion

Two-way deterministic finite automata (2DFAs) recognize exactly the regular languages (Rabin and Scott; Shepherdson, 1959), but letting the head revisit the input can change how much finite control is needed. In 1978 Sakoda and Sipser asked for the state cost of converting one-way and two-way nondeterministic automata into 2DFAs: is a polynomial number of states always enough? They identified a complete witness family $B_h$, now called one-way liveness, whose letters are binary relations on an $h$-element set; a word is live when the product of its letters is nonempty. Lower bounds against unrestricted 2DFAs — whose head may reverse anywhere and arbitrarily often — have been the difficult part of this question.

Background and timeline

• 1959 — Rabin–Scott and Shepherdson: two-way deterministic automata recognize only regular languages.
• 1978 — Sakoda and Sipser pose the state-cost question and prove completeness of the liveness family $B_h$ (STOC 1978, Theorem 2.3).
• 1980 — Sipser: exponential lower bounds for sweeping 2DFAs, which reverse only at endmarkers (J. Comput. System Sci. 21, 1980).
• 1986 — Chrobak: quadratic lower bounds against unrestricted 2DFAs for unary languages (TCS 1986).
• 2013 — Kapoutsis extends exponential bounds to 2DFAs with sublinearly many reversals (Inf. Comput. 222, 2013).
• 2018 — Kapoutsis: optimal $\Theta(h^2/\log h)$ for liveness restricted to words of three letters (LNCS 11011, 2018).
• 2026 — Adeogun and Kapoutsis: a quadratic lower bound for unrestricted 2DFAs against one-way liveness (arXiv:2602.24279). An OpenAI preprint, An exponential two-way deterministic state lower bound for one-way liveness (OpenAI Math Release, September 25, 2026), claims an exponential bound for unrestricted 2DFAs over the growing relation alphabets. The preprint has not been peer reviewed, and its main theorem is not formally verified.

Setting

An automaton has a finite set of states and a read-only head on a word over an alphabet $\Sigma$, bracketed by two distinct endmarkers. The head starts on the left endmarker in the initial state; each transition depends on the current state and scanned symbol, changes the state, and moves the head left, right or not at all, never across an endmarker. A deterministic rule gives at most one successor (rules may be partial); a nondeterministic rule allows several. Acceptance means some finite computation reaches an accepting state; infinite nonaccepting computations reject. Two conventions are considered: under the first, an accepting initial configuration counts; under the second (positive convention) at least one transition is required. All states are counted.

For $H=\{1,\dots,h\}$ let $\mathcal R_H$ be the monoid of binary relations on $H$ with path-order product, $(x,z)\in AB$ iff $(x,y)\in A$ and $(y,z)\in B$ for some $y$, and identity $I_H$. The one-way liveness language is

$$\mathrm{OWL}_h=\{R_1\cdots R_\ell\in\mathcal R_H^*:\ R_1R_2\cdots R_\ell\neq\varnothing\},$$

where the empty product is $I_H$, so the empty word is live.

Formalization targets

Goal: Theorem 1.1

For every $h\ge2$:

1. $\mathrm{OWL}_h$ is recognized, under both acceptance conventions, by a nondeterministic automaton with $h+3$ states that never moves left;
2. every 2DFA with $s$ states recognizing $\mathrm{OWL}_h$ satisfies

$$2^{\lfloor (h-2)/31\rfloor}\;\le\;4\,(s+2)^2\quad\text{(positive convention)},\qquad 2^{\lfloor (h-2)/31\rfloor}\;\le\;4\,(s+1)^2\quad\text{(initial acceptance counts)}.$$

The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The theorem gives an exponential separation between one-way nondeterministic automata and unrestricted two-way deterministic automata, improving the quadratic bound of Adeogun and Kapoutsis to an exponential one. Corollary 1.2 of the source deduces that no polynomial $Cn^c$ bounds the deterministic two-way state cost of $n$-state 2NFAs uniformly over all finite alphabets. The alphabet $\mathcal R_H$ has $2^{h^2}$ letters, so the result does not address a fixed alphabet or logarithmic-space complexity classes. A companion OpenAI preprint uses the same language to prove an exponential lower bound for complementing 2NFAs.

Formalizing it. The statement is a finite combinatorial claim about two explicit machine models. A formal proof would certify the passage from deterministic computations to products in the Brauer diagram monoid and the rank-loss induction with explicit constants ($32$ conjugates, $256$ additions, step $31$).

Difficulty

Earlier exponential bounds rely on restricting how often the deterministic head reverses; an unrestricted 2DFA may revisit a cell arbitrarily often as input length grows, and crossing-sequence arguments then lose control. The central obstacle is to represent repeated visits to a cell by an object that depends only on that cell's symbol, not on its neighbors, so that the machine induces a monoid map onto the relation monoid. Once such a representation exists, one still needs a lower bound on its size that grows exponentially in $h$ rather than polynomially.

Formalization scope

• Letters are BRel (Fin h), a structure wrapping Fin h → Fin h → Prop, with the monoid structure given by path-order composition and identity Eq; OWL h is the set of words whose List.prod relates some pair.
• Symbol Alpha adds left and right endmarkers; moves are left | stay | right; head positions are Fin (w.length + 2) and Move.Rel fixes the position change.
• NMachine Alpha n and DMachine Alpha s have state types Fin n, Fin s, a set of accepting states, set-valued or Option-valued transitions, and boundary axioms forbidding left moves on the left endmarker and right moves on the right endmarker.
• FiniteRun positive uses TransGen (at least one step) when positive = true and ReflTransGen otherwise; Recognizes positive L means acceptance exactly on L.
• NoLeft forbids left moves in the source automaton. The recognizer clause quantifies over both conventions with the same machine.
• The bound is in natural numbers with floor division (h - 2) / 31, and s ranges over all natural numbers (an s = 0 machine has no states and cannot recognize the language).
• Infrastructure needed: Brauer (matching) diagram monoids with rank and idempotents, relation monoids, and the tour construction turning deterministic computations into diagrams. The diagram-monoid layer is reusable for other two-way automata lower bounds.

Selected references

• M. O. Rabin, D. Scott, Finite automata and their decision problems, IBM J. Res. Develop. 3 (1959), 114–125.
• J. C. Shepherdson, The reduction of two-way automata to one-way automata, IBM J. Res. Develop. 3 (1959), 198–200.
• W. J. Sakoda, M. Sipser, Nondeterminism and the size of two way finite automata, STOC 1978, 275–286. https://doi.org/10.1145/800133.804357
• M. Sipser, Lower bounds on the size of sweeping automata, J. Comput. System Sci. 21 (1980), 195–202.
• M. Chrobak, Finite automata and unary languages, Theoret. Comput. Sci. 47 (1986), 149–158. https://doi.org/10.1016/0304-3975(86)90142-8
• C. Kapoutsis, Nondeterminism is essential in small two-way finite automata with few reversals, Inform. and Comput. 222 (2013), 208–227.
• C. A. Kapoutsis, Optimal 2DFA algorithms for one-way liveness on two and three symbols, LNCS 11011 (2018), 33–48.
• K. Adeogun, C. Kapoutsis, A quadratic lower bound for 2DFAs against one-way liveness, preprint (2026). https://doi.org/10.48550/arXiv.2602.24279
• R. Brauer, On algebras which are connected with the semisimple continuous groups, Ann. of Math. 38 (1937), 857–872.
• OpenAI, An exponential state lower bound for two-way nondeterministic complementation, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-exponential-state-lower-bound-for-two-way-nondeterministic-complementation-September-25-2026/paper.pdf
• OpenAI, An exponential two-way deterministic state lower bound for one-way liveness, OpenAI Math Release preprint, September 25, 2026 (source of the goal; Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-exponential-two-way-deterministic-state-lower-bound-for-one-way-liveness-September-25-2026/main.pdf

Motivation: approximating the shortest common superstring

Given a finite collection $\mathcal S$ of strings, the shortest common superstring (SCS) problem asks for a shortest string $T$ that contains every member of $\mathcal S$ as a contiguous substring. It is a basic model of sequence assembly (reconstructing a long DNA sequence from overlapping fragments) and of data compression, and it is a standard test problem for approximation algorithms. Computing the optimum exactly is hard — Blum, Jiang, Li, Tromp and Yannakakis showed the problem is MAX SNP-hard, so it has no polynomial-time approximation scheme unless P = NP (Blum et al., J. ACM 1994) — so the natural question is the best constant factor achievable in polynomial time. For decades the target has been factor $2$: the classical Greedy conjecture asserts that repeatedly merging the pair with maximum overlap achieves it.

Timeline

• 1988 — Tarhio and Ukkonen propose the factor-$2$ conjecture for the maximum-overlap Greedy procedure (Theor. Comput. Sci. 1988).
• 1994 — Blum, Jiang, Li, Tromp and Yannakakis give the first constant-factor algorithm a polynomial-time $3$-approximation (J. ACM 1994).
• 1997 — Breslauer, Jiang and Jiang use rotations of periodic strings to control overlaps (J. Algorithms 1997).
• 1999 — Sweedyk obtains factor $5/2$ (SIAM J. Comput. 1999).
• 2013 — Mucha obtains $2+11/23$ via Lyndon words (SODA 2013).
• 2019/2020 — Golovnev, Kulikov, Logunov, Mihajlin and Nikolaev introduce the all-substrings hierarchical graph and the Collapsing conjecture (APPROX/RANDOM 2019; arXiv:1809.08669).
• 2023 — Englert, Matsakis and Veselý obtain $(14+\sqrt{67})/9<2.466$ (ISAAC 2023).
• 2026 — Chukhin, Kulikov, Mihajlin and Smal report a $7/3$-approximation (ECCC TR26-157); Shibata reports a counterexample to the Greedy conjecture with ratio at least $9/4$ (arXiv:2609.01365).
• 2026 — An OpenAI preprint, A Polynomial-Time 2-Approximation for Shortest Common Superstring (OpenAI Math Release, September 24, 2026), claims a deterministic polynomial-time algorithm with ratio $2$. The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

A string is a finite list of symbols; a string $s$ is a substring of $T$ if $T=usv$ for some strings $u,v$ (the empty string is a substring of everything). For a finite list $\mathcal S$ of strings, a common superstring is a string $T$ having every $s\in\mathcal S$ as a substring, and

$$\mathrm{OPT}(\mathcal S)=\min\{|T| : T \text{ is a common superstring of }\mathcal S\},$$

where $|T|$ counts symbols. The alphabet is unbounded: each symbol is given by an explicit binary label, and the input is measured by its total encoded bit length $N$. An algorithm runs in polynomial time if its running time on a bit-level machine is bounded by a polynomial in $N$.

In Lean (namespace OAI.Superstring), a symbol is List Bool, a word is a list of symbols, and an instance is a list of words. Substring containment is Mathlib's infix relation <:+:, opt S is the infimum of lengths of common superstrings, and HasPolynomialImplementation f asks for a Mathlib Turing.TM2ComputableInPolyTime certificate for f with respect to an explicit self-delimiting binary encoding of instances and outputs, with every stack alphabet finite.

Formalization targets

Goal: a polynomial-time 2-approximation (Theorem 1.1)

There is a function $f$ from instances to words, computable in polynomial time in the encoded input length, such that for every instance $\mathcal S$

$$f(\mathcal S)\ \text{is a common superstring of } \mathcal S\qquad\text{and}\qquad |f(\mathcal S)|\le 2\,\mathrm{OPT}(\mathcal S).$$

The goal is published on the platform with status Open.

Significance

The result itself. Factor $2$ has been the conjectured benchmark for SCS since 1988, and the best proved polynomial-time ratio before this preprint was $7/3$ (reported in 2026). Theorem 1.1 reaches factor $2$ with a new algorithm rather than with Greedy, which a 2026 preprint reports does not achieve factor $2$.

Formalizing it. The statement mixes three components that are each easy to get subtly wrong on paper: the correctness of the output (contiguous coverage of every input), the ratio against the unrestricted optimum, and a running-time bound measured in bits, with symbols of arbitrary label length. The formal statement pins down all three with an explicit machine model. A complete formalization requires both the combinatorial ratio proof and a verified polynomial-time implementation on Mathlib's stack-machine model, which is substantial reusable infrastructure for complexity statements in Lean.

Difficulty

The classical approach builds the overlap (distance) graph, takes a minimum-weight cycle cover as a lower bound, and then opens and concatenates the cycles; the cost of joining cycles is what has kept ratios above $2$. Greedy, the natural candidate for factor $2$, is reported to fail. Any factor-$2$ algorithm needs a lower bound on $\mathrm{OPT}$ that is tight enough that the cost of connecting all the pieces can be charged to the lower bound a second time without double-counting, uniformly over periodic and highly repetitive inputs. The polynomial running time must also be established at the bit level, with symbols of unbounded encoded length.

Formalization scope

• Instances are List (List (List Bool)): duplicates and empty strings are allowed, and symbols are arbitrary bit lists, so the alphabet is unbounded.
• Coverage is contiguous substring containment (List.IsInfix), not subsequence containment.
• opt is a natural-number sInf; the set is nonempty because the concatenation of all inputs is a common superstring, so the junk value is never used. The ratio is measured in symbols.
• Polynomial time uses Mathlib's Turing.TM2ComputableInPolyTime for the encodings encodeInstance and encodeWord (prefix markers for list structure), together with finiteness of every stack alphabet, so the time bound is in input bits on a finite-alphabet machine. A function that is merely computable, or polynomial only in the number of symbols, does not satisfy the goal.
• Needed infrastructure: the all-substrings graph and Euler tours, periodicity lemmas (Fine–Wilf), and a verified implementation on Mathlib's TM2 model. Contributions of reusable TM2 programming libraries are welcome.

Selected references

• J. Tarhio and E. Ukkonen, A greedy approximation algorithm for constructing shortest common superstrings, Theor. Comput. Sci. 57 (1988), 131–145. https://doi.org/10.1016/0304-3975(88)90167-3
• A. Blum, T. Jiang, M. Li, J. Tromp and M. Yannakakis, Linear approximation of shortest superstrings, J. ACM 41 (1994), 630–647. https://doi.org/10.1145/179812.179818
• D. Breslauer, T. Jiang and Z. Jiang, Rotations of periodic strings and short superstrings, J. Algorithms 24 (1997), 340–353. https://doi.org/10.1006/jagm.1997.0861
• Z. Sweedyk, A 2.5-approximation algorithm for shortest superstring, SIAM J. Comput. 29 (1999), 954–986. https://doi.org/10.1137/S0097539796324661
• M. Mucha, Lyndon words and short superstrings, SODA 2013, 958–972. https://doi.org/10.1137/1.9781611973105.69
• A. Golovnev, A. S. Kulikov, A. Logunov, I. Mihajlin and M. Nikolaev, Collapsing superstring conjecture, APPROX/RANDOM 2019. https://doi.org/10.4230/LIPIcs.APPROX-RANDOM.2019.26
• M. Englert, N. Matsakis and P. Veselý, Approximation guarantees for shortest superstrings: simpler and better, ISAAC 2023. https://doi.org/10.4230/LIPIcs.ISAAC.2023.29
• N. Chukhin, A. S. Kulikov, I. Mihajlin and A. Smal, A tight cycle-cover inequality for shortest common superstring, ECCC TR26-157, 2026. https://eccc.weizmann.ac.il/report/2026/157/
• H. Shibata, Disproving the greedy superstring conjecture, arXiv:2609.01365, 2026. https://arxiv.org/abs/2609.01365v1
• OpenAI, A Polynomial-Time 2-Approximation for Shortest Common Superstring, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Polynomial-Time-2-Approximation-for-Shortest-Common-Superstring-September-24-2026/paper.pdf

Motivation

A disjunctive normal form (DNF) is a disjunction of terms, each term a conjunction of Boolean literals. An unambiguous DNF has pairwise disjoint terms: no Boolean assignment satisfies two different terms. This restriction makes several tasks easy. In particular, the cited open-problem entry records polynomial-time algorithms for weighted satisfiability on unambiguous DNFs and for unweighted falsifiability. The unresolved boundary is weighted falsifiability: can one find a high-weight assignment outside the union of the terms, without enumerating all assignments?

This question is relevant to the complexity of negating compact representations of Boolean functions. Amarilli's entry observes that, since unambiguous DNFs are d-DNNFs, a polynomial-time negation procedure for d-DNNFs would yield a polynomial-time solution to weighted falsifiability on unambiguous DNFs by applying weighted satisfiability to the negated representation. Conversely, if weighted falsifiability for unambiguous DNFs—or even for d-DNNFs—is NP-hard, then, unless $\mathrm{P}=\mathrm{NP}$, d-DNNFs cannot be negated in polynomial time. These are implications stated by the source, not results established by this mission.

Historical note

The question appears on Albertine Amarilli's open-problem list. The entry cites a Theoretical Computer Science Stack Exchange question by Mikaël Monet and credits him with helping prepare the entry. It records two partial tractability results: weighted satisfiability with binary weights, and weighted falsifiability when the variable weights are unary. The entry gives no date for when the problem was posed or last seen open, so this description does not assign one. The linked discussion is useful context, not a novelty or resolution certificate.

Setting

Let $X=\{x_0,\ldots,x_{n-1}\}$ be exactly the variables occurring in the DNF. The formal input declares this finite universe by its size $n$; validity requires every declared variable to occur in at least one literal. An input DNF is a finite list of terms, and each term is a finite list of signed variable indices. An assignment is a function $\nu:X\to\{0,1\}$. A positive literal $x_i$ is true when $\nu(x_i)=1$; a negative literal $\neg x_i$ is true when $\nu(x_i)=0$. A term is true when all its literals are true, and the DNF is true when at least one term is true. Thus the empty DNF is false and an empty term is true.

The input also contains one positive integer weight $c_i$ for each variable and a positive threshold $t$. The weight of an assignment is

$$w(\nu)=\sum_{i=0}^{n-1} c_i\nu(x_i).$$

The DNF is valid for this problem when every literal index is below $n$ and every pair of distinct terms is mutually unsatisfiable. The decision question is whether there exists an assignment that falsifies the DNF and has weight at least $t$.

Formalization targets

Partial result — weighted satisfiability

For valid unambiguous DNF inputs with positive binary-encoded weights and threshold, the decision problem asking whether a satisfying assignment has weight at least $t$ has a deterministic polynomial-time algorithm. This is the weighted-satisfiability baseline recorded in the source entry. It is a separate result from the goal below.

Partial result — unary-weight falsifiability

For the same valid DNF model, when each variable weight is encoded in unary, weighted falsifiability has a deterministic polynomial-time algorithm. The threshold remains binary-encoded in this formalization. The source entry records this unary-weight restriction as tractable.

Goal — binary-weight falsifiability

For arbitrary positive binary-encoded variable weights and a positive binary-encoded threshold, determine whether one fixed deterministic Turing machine and one polynomial time bound decide weighted falsifiability for every valid input. The machine must be correct on all valid instances; its running-time bound is uniform and measured in the length of the explicit input code. No witness output is required.

The two partial results are reference points, not assumptions from which the goal is claimed to follow. The goal is the open binary-weight case; it must not be replaced by the satisfiability problem or by the unary-weight restriction.

Dependency graph

Input, semantics, validity, and serialization definitions
├── binary-weight weighted satisfiability (source baseline)
├── unary-weight weighted falsifiability (source baseline)
└── binary-weight weighted falsifiability (open goal)

Each branch shares the same finite DNF model and correctness predicates. The arrows indicate required definitions and scope, not a claim that either partial theorem implies the open goal.

Significance

A positive result would give a uniform algorithm for finding whether a disjoint union of Boolean subcubes omits any sufficiently heavy point, even when weights are represented compactly in binary. A negative complexity result would identify a sharp obstruction to efficient complement-related operations on these representations. The exact-weight version (asking for weight exactly $t$) is a different problem and is outside this mission's scope; the goal here is specifically weight at least $t$.

Formalizing the question fixes the universe of variables, signed-literal semantics, unambiguity condition, threshold direction, input encoding, and computational model. It also makes the unary and satisfiability baselines comparable to the binary-weight goal without treating a finite search or a candidate implementation as a complexity proof. No solution is supplied or presumed here.

Difficulty

The direct search over all $2^n$ assignments is exponential in $n$. Counting satisfying assignments is enough to settle ordinary falsifiability, but a weighted threshold partitions assignments by exponentially many possible total weights when the weights are binary. The unary dynamic program therefore does not by itself give a polynomial bound in the binary input length. Conversely, solving weighted satisfiability on the DNF does not answer whether a heavy assignment lies outside it. The task is to settle that gap without silently replacing binary magnitude by unary size.

Formalization scope

The Lean model uses Input, an explicit variable count, a list of signed-index terms, a weight list, and a threshold. validInput requires exactly one positive weight per variable, positive weights and threshold, in-range literal indices, that every declared variable occurs in the formula, and pairwise unsatisfiable distinct terms. The finite assignment type is Fin n → Bool; unused variables remain part of the input. The decision predicate is existential and exact.

The binary code includes the variable count, every list count and delimiter, all signed indices, all weights, and the threshold. Natural-number payloads use canonical binary digits with an explicit unary length prefix. The unary-weight code changes only the variable-weight payloads to unary; formula data and threshold remain binary. The complexity statements use Mathlib's bundled deterministic Turing.TM2ComputableInPolyTime model, with a single machine and polynomial bound in the chosen code length. This formalization does not claim refinement to JSON, CPython, or any runtime implementation. Human review should check the encoding/decoder round-trip and the source correspondence before launch.

The reusable definitions are the finite DNF semantics, weighted assignment score, validity predicate, binary/unary encoders, and exact decision predicates. Formalizing the two cited partial results is part of the mission's milestone path; neither is evidence that the binary-weight goal is solved.

Selected references

• Albertine Amarilli, “Weighted falsifiability for unambiguous DNFs,” List of open questions in theoretical computer science, https://a3nm.net/work/research/questions/#weighted-falsifiability-for-unambiguous-dnfs.
• Mikaël Monet, “Is this problem on unambiguous DNFs hard?”, Theoretical Computer Science Stack Exchange, https://cstheory.stackexchange.com/questions/53733/is-this-problem-on-unambiguous-dnfs-hard.

Motivation

Market equilibrium is the central solution concept of general equilibrium theory: prices at which every agent buys a utility-maximizing bundle and supply meets demand. Arrow and Debreu (1954) proved that equilibria exist under mild conditions on endowments and utilities, and a line of work in algorithmic game theory asks how hard it is to compute them. For linear utilities an equilibrium can be computed in polynomial time, and there is an efficiently checkable condition for its existence. The next natural class, additively separable piecewise-linear concave utilities, models diminishing marginal utility and is the class most used in applications.

Vazirani and Yannakakis (J. ACM 58(3), 2011) settle the complexity of this class. They show that equilibria are rational whenever they exist (Theorems 4.1 and 5.1), that computing an equilibrium under the standard sufficient conditions is PPAD-complete (Theorems 6.1 and 7.1, building on Chen, Dai, Du and Teng 2009), and — the subject of this mission — that deciding whether an equilibrium exists at all is NP-complete (Theorem 8.1). The hardness half rests on an explicit construction: from an instance of Exact Cover by 3-Sets, a market whose equilibria encode exact covers.

Setting

An Arrow–Debreu market has a finite set $B$ of agents and a finite set $G$ of divisible goods. Agent $i$ owns an endowment $w_{ij}\ge 0$ of each good $j$ and has utility $u_i(y)=\sum_{j} f^i_j(y_j)$, where each $f^i_j$ is a piecewise-linear concave utility function: slopes $c_1\ge c_2\ge\dots\ge c_m>0$ on consecutive pieces of lengths $a_1,\dots,a_m$, followed by a last piece of slope $t\in[0,c_m]$ until infinity ($t=0$ means the function goes flat).

At prices $p$, agent $i$'s income is $\sum_j p_j w_{ij}$. An optimal bundle is an affordable $y\ge 0$ maximizing $u_i$ among affordable bundles, bought only along the pieces of $f^i_j$ that carry utility. A price equilibrium is a price vector $p$ in the unit simplex ($p\ge 0$, $\sum_j p_j=1$) together with an allocation of optimal bundles such that $\sum_i x_{ij}=\sum_i w_{ij}$ for every good $j$. It is an $\epsilon$-approximate equilibrium if instead $|\sum_i x_{ij}-\sum_i w_{ij}|\le\epsilon\sum_i w_{ij}$ for every $j$.

An X3C instance is a family $\mathcal C=(C_1,\dots,C_n)$ of $3$-element subsets of $X=\{x_1,\dots,x_n\}$; an exact cover is a subfamily in which every element of $X$ lies in exactly one set. Following the paper, $n$ is a multiple of $3$, $n>35$, and $\bigcup_i C_i=X$.

The market $D(\mathcal C)$ has $2n+1$ goods (good $0$, goods $C_i$, goods $x_j$) and $2n+2$ agents, with $e_0=n^3$:

1. agent $0$ owns $e_0$ units of every good; his utility for every good has slope $2$ up to $e_0$ units and slope $1$ beyond;
2. agent $C_i$ owns one unit of good $C_i$; segments of slope $1$, length $1/2$ for good $0$, slope $1/3$, length $1/6$ for each good $x_j\in C_i$, slope $1/9$, length $1/4$ for good $C_i$;
3. agent $x_j$ owns $1/6$ unit of good $x_j$; one segment of slope $1$, length $1/12$ for good $0$;
4. the extra agent owns $n/2$ units of good $0$; one segment of slope $1$, length $3/4$ for each good $C_i$.

All other utility functions are flat.

Formalization targets

Goal: the reduction statement

$$\mathcal C\ \text{has an exact cover}\iff D(\mathcal C)\ \text{has an equilibrium}\iff D(\mathcal C)\ \text{has an } n^{-5}\text{-approximate equilibrium}.$$

This is the mathematical content of the NP-hardness half of Theorem 8.1, assembled by the paper from Lemmas 8.2 and 8.3.

Milestones

1. Lemma 8.2: an exact cover yields an equilibrium of $D(\mathcal C)$.
2. Lemma 7.2, as applied in Lemma 8.3: in an $n^{-5}$-approximate equilibrium of $D(\mathcal C)$ all prices are positive and within a factor $2$ of each other.
3. Claims 8.4–8.7: in such an equilibrium, with $p_m$ the minimum price, $p(0)=2p_m$; $p(x_j)<2p_m$; with $S=\{i: p(C_i)\ge p_m+\tfrac16\sum_{x_j\in C_i}p(x_j)\}$, every $i\notin S$ has $p(C_i)=p_m$; and the sets indexed by $S$ are pairwise disjoint.
4. Lemma 8.3: an equilibrium, or an $n^{-5}$-approximate equilibrium, of $D(\mathcal C)$ yields an exact cover.

Significance

Theorem 8.1 shows that there is no efficiently checkable necessary and sufficient condition for the existence of an equilibrium in piecewise-linear concave markets unless P = NP, in contrast with the linear case. Together with the PPAD results of the same paper it separates two questions: under the classical sufficient conditions an equilibrium exists and finding one is PPAD-complete; without them, even deciding existence is NP-hard, and remains so for $n^{-5}$-approximate equilibria. The construction illustrates the technique the paper uses for both of its negative results: well-chosen piecewise-linear pieces make an agent buy a segment wholly or not at all, depending on how prices compare, which gives the equilibrium problem a discrete character.

The result is proved in the paper. To our knowledge no part of it has been machine-checked. This mission formalizes the reduction's correctness at full strength, including the approximate version, which requires quantitative control of clearing errors that the exact version does not.

Difficulty

The direction "exact cover ⇒ equilibrium" is an explicit verification: prescribed prices and an allocation, and a check that every bundle is optimal, which for separable piecewise-linear utilities is a bang-per-buck comparison. The converse is the substantial part. An arbitrary approximate equilibrium must be shown to have the rigid price structure — every price in $[p_m,2p_m]$, good $0$ at $2p_m$, unused sets at $p_m$ — before a counting argument on agent $0$'s savings forces $|S|=n/3$. Each step is an excess-demand argument in which the error $\epsilon$ times the supply must be compared with quantities of order $1/n$; this is where $n>35$ and the exponent $5$ enter, and why the approximate statement does not follow from the exact one. Optimality of bundles is a statement about all affordable bundles, so each claim needs the structure of optimal bundles under piecewise-linear concave utility, which is not in Mathlib.

Formalization scope

Lean namespace PLCMarkets.ExactCover. Market data (endowments, slopes, lengths) are rationals; prices and allocations are reals. Goods and agents of $D(\mathcal C)$ are small inductive types named as in the paper; indices are 0-based. Supplies are not normalized to $1$, so clearing is $\sum_i x_{ij}=\sum_i w_{ij}$; prices are normalized to the simplex in both equilibrium notions, as in the proof of Lemma 8.3. The family $\mathcal C$ is indexed and may repeat a set; exact cover and the disjointness of $S$ count indices.

Standing hypotheses of every theorem: each $C_i$ has three elements, $3\mid n$, $n>35$, $\bigcup_i C_i=X$ — the paper's own "without loss of generality" assumptions (p. 10:19). Two conventions depart from the printed page, both necessary and both disclosed on the items:

• Optimal bundles buy only utility-bearing pieces. If a utility function is flat beyond its segments, the agent does not buy beyond them. The paper uses this throughout (an agent "can only spend $p_m/6$ on the single segment", Claim 8.5). Without it, agents can spend leftover income on goods worth nothing to them; then setting $p(0)=2p_m$ and every other price to $p_m$ gives an exact equilibrium of every $D(\mathcal C)$, and the goal is false.
• The extra agent's segments have length $3/4$. The page prints $3n/4$; every computation in the paper (Lemma 8.2, Claim 8.6, the end of Lemma 8.3) uses $3/4$ per good, and with $3n/4$ the prices of Lemma 8.2 are not an equilibrium.

Trivializing encodings are excluded: optimality of bundles is part of both equilibrium notions (without it the endowment itself clears every market), clearing is relative and per good, and the goal quantifies only over $n$ and $\mathcal C$, with $D(\mathcal C)$ an explicit function of $\mathcal C$.

Out of scope: the complexity-class statement "NP-complete" and NP membership (which comes from the rationality theorems of the companion mission); polynomial-time computability of the construction and string encodings of markets; and the Fisher market $F$ of §8, whose half of Lemmas 8.2 and 8.3 is a natural follow-up. Reusable infrastructure: piecewise-linear concave utilities, Arrow–Debreu markets with exact and approximate equilibria, and bang-per-buck characterizations of optimal bundles. Contributions proving that characterization as a standalone lemma are welcome.

Selected references

• V. V. Vazirani and M. Yannakakis, Market Equilibrium under Separable, Piecewise-Linear, Concave Utilities, Journal of the ACM 58(3), Article 10, 2011. https://doi.org/10.1145/1970392.1970394
• X. Chen, D. Dai, Y. Du and S.-H. Teng, Settling the Complexity of Arrow–Debreu Equilibria in Markets with Additively Separable Utilities, Proceedings of the IEEE Symposium on Foundations of Computer Science (FOCS), 2009 (reference [Chen et al. 2009a] of the paper).
• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.
• K. J. Arrow and G. Debreu, Existence of an Equilibrium for a Competitive Economy, Econometrica 22(3), 1954. https://doi.org/10.2307/1907353

Motivation

The permanent versus determinant problem asks how large an $n$ must be for the permanent of an $m \times m$ matrix to be written as the determinant of an $n \times n$ matrix whose entries are affine linear functions of the $m^2$ input variables. Valiant showed that some finite $n$ always works and conjectured in 1979 that the least such $n$, the determinantal complexity $\mathrm{dc}(\mathrm{per}_m)$, grows faster than every polynomial in $m$; this is the algebraic counterpart of $\mathbf{P} \ne \mathbf{NP}$.

Geometric complexity theory (GCT), proposed by Mulmuley and Sohoni in 2001, attacks the conjecture by replacing the two polynomials with the closures of their $\mathrm{GL}$-orbits and comparing the $\mathrm{GL}$-representations carried by the coordinate rings of those closures. If some irreducible representation occurs in the coordinate ring of the orbit closure of the padded permanent but not in that of the determinant, then one orbit closure cannot contain the other, and a lower bound on $\mathrm{dc}(\mathrm{per}_m)$ follows. Such a representation is an occurrence obstruction, and Mulmuley and Sohoni conjectured that occurrence obstructions exist for every polynomial padding.

Timeline of what is actually proved.

• 1979: Valiant introduces $\mathrm{dc}$ and conjectures superpolynomial growth (Valiant 1979).
• 2001: Mulmuley and Sohoni restate the conjecture in terms of orbit closures and propose proving it by exhibiting occurrence obstructions (arXiv:cs/9908014).
• 2014: Kadish and Landsberg show that any partition occurring for the padded permanent has at most $m^2$ rows and a first row of length at least $(n-m)d$ (arXiv:1204.4772).
• 2016: Ikenmeyer and Panova show that vanishing rectangular Kronecker coefficients cannot supply occurrence obstructions (arXiv:1512.03798).
• 2016: Mulmuley, in GCT V, makes the "infinitesimally close approximation" form of the permanent hardness hypothesis the engine of derandomized Noether normalization (JAMS).
• 2017: Ikenmeyer, Mulmuley and Walter prove that deciding positivity of Kronecker coefficients is $\mathbf{NP}$-hard and construct superpolynomially many vanishing triples in the Kronecker cone (comput. complex. 26).
• 2019: Bürgisser, Ikenmeyer and Panova prove that no occurrence obstructions exist at all once $n \ge m^{25}$, refuting the Mulmuley–Sohoni conjecture on obstructions (JAMS 32).

Setting

Fix $n$ and write $V = \mathbb{C}^{n \times n}$. A form of degree $n$ is a homogeneous polynomial of degree $n$ in the $n^2$ variables $X_{ij}$, $0 \le i, j < n$; the space of such forms is $\mathrm{Sym}^n V^*$. The group $\mathrm{GL}_{n^2}$ acts on it by linear substitution of the variables, and for a form $p$ we write $\overline{\mathrm{GL}_{n^2}\cdot p}$ for the closure of its orbit in the Euclidean topology, which for these orbits agrees with the Zariski closure.

Two orbit closures matter:

$$\Omega_n \;=\; \overline{\mathrm{GL}_{n^2}\cdot \det\nolimits_n}, \qquad Z_{n,m} \;=\; \overline{\mathrm{GL}_{n^2}\cdot X_{00}^{\,n-m}\mathrm{per}_m},$$

where $\det_n = \sum_{\sigma \in S_n}\mathrm{sgn}(\sigma)\prod_i X_{i\sigma(i)}$ and $\mathrm{per}_m = \sum_{\sigma \in S_m}\prod_i X_{i\sigma(i)}$, and the second polynomial is padded by a power of the single variable $X_{00}$ so that it, too, has degree $n$.

The coordinate ring of a $\mathrm{GL}_{n^2}$-stable subset $S$ of $\mathrm{Sym}^n V^*$ decomposes into irreducible polynomial representations, which are labelled by partitions $\lambda$ with at most $n^2$ parts. A partition $\lambda \vdash nd$ occurs in the degree $d$ part of the coordinate ring of $S$ when some polynomial function $F$ of degree $d$ on $\mathrm{Sym}^n V^*$ is an eigenvector of the Borel subgroup of upper triangular matrices,

$$F(g \cdot p) \;=\; \Big(\prod_{v} g_{vv}^{\lambda_{v}}\Big) F(p) \quad\text{for all upper triangular invertible } g \text{ and all forms } p,$$

and $F$ does not vanish identically on $S$. If $\lambda$ occurs for $Z_{n,m}$ but not for $\Omega_n$, then $Z_{n,m} \not\subseteq \Omega_n$, hence $\mathrm{dc}(\mathrm{per}_m) > n$: this is an occurrence obstruction.

Formalization targets

Goal — no occurrence obstructions (Theorem 1.4)

$$n \ge m^{25},\quad \lambda \vdash nd, \quad \lambda \text{ occurs for } Z_{n,m} \;\Longrightarrow\; \lambda \text{ occurs for } \Omega_n .$$

No partition can separate the two orbit closures once the padding is at least polynomial of degree $25$; the occurrence-obstruction route to Valiant's conjecture is therefore closed.

Supporting targets

The milestone list follows the structure of the proof: the shape restriction for the padded permanent (Theorem 2.1), the semigroup property of occurring partitions (Lemma 2.2), the occurrence of row extended even rectangles (Proposition 2.3), the non-vanishing of highest weight vectors of long first row on $\Omega_n$ (Proposition 2.4), and the fact that padded power sums lie in $\Omega_n$ (Theorem 2.5), together with two elementary anchors ($\Omega_2$ is everything; a symbolic determinant of size $n$ puts the padded permanent into $\Omega_n$) and the GCT V hardness hypothesis, which is exactly the statement that the padded permanent stays outside $\Omega_s$ for subexponential $s$.

Significance

Theorem 1.4 removes an entire proof strategy: after fifteen years in which occurrence obstructions were the main object of study in GCT, the theorem shows that they do not exist in the regime where they would be useful, so lower bounds must come from comparing multiplicities rather than mere occurrence. The supporting statements are of independent use: Theorem 2.5 and Proposition 2.3 give explicit families of points and partitions for $\Omega_n$, and the shape restriction of Theorem 2.1 constrains every future obstruction argument.

None of this is formalized anywhere. What this mission produces is a machine-checked model of orbit closures of forms, of the Borel-eigenvector description of occurrence, and of the known statements about $\Omega_n$ and $Z_{n,m}$ — infrastructure that any later multiplicity-based argument would reuse. The goal theorem is proved in the literature; the work here is formalizing that proof. The hardness hypothesis and the Mulmuley–Sohoni conjecture itself remain open, and are labelled as such.

Difficulty

The naive approach to "λ occurs in $\mathbb{C}[\Omega_n]$" is to decompose the plethysm $\mathrm{Sym}^d \mathrm{Sym}^n V$ and read off multiplicities; this fails because the coordinate ring of $\Omega_n$ is a quotient of that plethysm by the unknown vanishing ideal of the orbit closure, and almost nothing is known about which highest weight vectors survive restriction. The proof of Theorem 1.4 works instead with explicit highest weight vectors evaluated at explicit points of $\Omega_n$ (padded power sums), using the fundamental invariant of $\mathrm{Sym}^n \mathbb{C}^N$ and a lifting map for highest weight vectors in plethysms; the combinatorics of tableaux and the case distinction on the degree $d$ are where the work lies. A formalization additionally has to build the representation-theoretic vocabulary from scratch, since Mathlib has neither plethysms, nor Weyl modules, nor highest weight theory for $\mathrm{GL}_N$.

Formalization scope

Conventions fixed by the Lean development, all in the namespace GCTOcc:

1. Polynomials live in one ring, with variables indexed by pairs of natural numbers; the $n \times n$ matrix of variables occupies the indices $i, j < n$, so forms of different sizes need no renaming maps.
2. The padding variable is $X_{00}$, an entry of the matrix itself, as in the source; the choice of padding linear form is known to be immaterial.
3. Orbit closure is defined sequentially: $p$ lies in the closure when the coefficients of a sequence of orbit points converge to those of $p$. On this finite-dimensional space sequential closure is the Euclidean closure.
4. Occurrence of $\lambda$ is defined by the existence of a Borel eigenvector of weight $\lambda$ and degree $d$ that does not vanish identically on the set. Weights are indexed by the order $(i,j) \mapsto in+j$ on the variables, and triangularity refers to the same order. A partition is a nonincreasing function $\mathbb{N} \to \mathbb{N}$ supported on the first $n^2$ indices whose parts sum to $nd$.
5. The statements are not vacuous: all hypotheses used in the milestones are satisfiable, and the elementary anchors ($\Omega_2$, the symbolic determinant bridge) exhibit points of the orbit closures explicitly.

Infrastructure a complete development needs, and which is reusable beyond this mission: plethysms $\mathrm{Sym}^d\mathrm{Sym}^n V$ and their highest weight vectors, the fundamental invariant of a form space, semistandard tableaux of rectangular content, and basic facts about orbit closures of forms. Contributions of any of these pieces are welcome, as are counterexample-hunting reports on the elementary anchors.

Not covered here: the Kronecker-coefficient strand of the program (Ikenmeyer–Mulmuley–Walter 2017 on $\mathbf{NP}$-hardness of Kronecker positivity, and the construction of vanishing triples in the Kronecker cone). Stating those results requires irreducible characters of the symmetric group indexed by partitions, or equivalently symmetric-function machinery, which Mathlib does not yet have; they are natural targets for a companion mission once Specht modules exist.

Selected references

• P. Bürgisser, C. Ikenmeyer, G. Panova, No occurrence obstructions in geometric complexity theory, J. Amer. Math. Soc. 32 (2019), 163–193, doi:10.1090/jams/908.
• K. D. Mulmuley, Geometric Complexity Theory V: Efficient algorithms for Noether normalization, J. Amer. Math. Soc., electronically published 2016, doi:10.1090/jams/864.
• C. Ikenmeyer, K. D. Mulmuley, M. Walter, On vanishing of Kronecker coefficients, comput. complex. 26 (2017), doi:10.1007/s00037-017-0158-y.
• L. G. Valiant, Completeness classes in algebra, STOC 1979, doi:10.1145/800135.804419.
• H. Kadish, J. M. Landsberg, Padded polynomials, their cousins, and geometric complexity theory, Comm. Algebra 42 (2014), arXiv:1204.4772.

Motivation

A quantum circuit of depth $d$ built from gates of fan-in at most two cannot let an output wire depend on more than $2^d$ input wires. The argument is folklore and takes a paragraph on paper: the causal cone of the measured wire grows by at most a factor of two per layer. Formalizing it exposes a subtlety that the paper argument hides, and that is what this mission is about.

The subtlety

Define the backward cone step of a wire set $S$ through a layer $l$ by adjoining the support of every gate of $l$ that meets $S$. There is a choice here: test each gate against the incoming set $S$, or against the partially accumulated cone. Testing against the accumulator over-approximates, and the doubling bound fails. Testing against the incoming set gives the bound — but is only correct when the gates within a layer act on pairwise disjoint wires.

Without that hypothesis (LayerOk) the semantic statement is false, and the counterexample is small: on three wires, the single layer [cnot 2 1, cnot 1 0] has cone $\{0,1\}$ around wire $0$, yet wire $0$ ends up holding $x_0 \oplus x_1 \oplus x_2$. So the cone under-approximates the true dependence. This mission's development carries LayerOk throughout, and the counterexample is recorded in the source.

What is formalized

Layered circuits over $\{H, S, T, \mathrm{CNOT}\}$ on $n$ wires, with states as amplitude functions on bit-strings and no tensor products anywhere. On top of that:

• the combinatorial half — one layer at most doubles the cone, hence $|\mathrm{cone}| \le 2^{d}\,|S|$;
• norm preservation, so that acceptProb is a genuine probability in $[0,1]$;
• the semantic half — inputs agreeing on the causal cone of the output wire are accepted with equal probability.

The semantic half is proved in the Heisenberg picture. The measurement observable is conjugated backwards through the circuit and its support tracked: a gate meeting the support enlarges it by that gate's own wires, and a gate missing it commutes with the observable and cancels against its own adjoint. That cancellation is the reason the non-cascading cone step is correct, and it is why unitarity of the gate set is needed at the $2^n$-dimensional level rather than gate by gate. Supporting this is a small reusable algebra of local operators: locality is monotone, closed under adjoint and product, and disjointly supported operators commute.

The frontier

The published depth bound assumes each input wire lies in the syntactic cone of the output. That is weaker than saying the wire matters. Milestone 1 asks for the semantically honest version, stated in terms of genuine functional dependence; the bridge is the semantic cone theorem already in the development.

Beyond that, the natural continuations are the same argument for fan-in-$k$ gates ($|\mathrm{cone}| \le k^{d}$), for geometrically local circuits where cone growth is linear rather than exponential, and ultimately the Bravyi–Gosset–König separation $\mathrm{QNC}^{0} \not\subset \mathrm{NC}^{0}$ — which needs machinery (non-local games, magic squares) that this development deliberately does not build.

Hardness of the closest vector problem, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.

For every Boolean language $A$ of finite bit strings for which there exist a polynomial $P\in\mathbb N[X]$ and a deterministic polynomial-time Boolean verifier $V$ satisfying $A(x)=\mathrm{true}$ if and only if there is a bit-string certificate $c$ with $|c|\le P(|x|)$ and $V(x,c)=\mathrm{true}$, there exists a total deterministic polynomial-time map $f$ on bit strings sending every $x$ with $A(x)=\mathrm{true}$ into the following YES set and every $x$ with $A(x)=\mathrm{false}$ into the following NO set. An instance consists of a natural dimension $n>0$, an integer matrix $B\in\mathbb Z^{n\times n}$ with $\det B\ne0$, a target $t\in\mathbb Q^n$ all of whose coordinates are integers, and a rational radius $r>0$. It is in YES exactly when some $z\in\mathbb Z^n$ satisfies $\sum_{i=0}^{n-1}((Bz)_i-t_i)^2\le r^2$, and in NO exactly when every $z\in\mathbb Z^n$ satisfies $(n^{1/400}r)^2<\sum_{i=0}^{n-1}((Bz)_i-t_i)^2$. The sets consist of the exact encoded instance strings, formed by concatenating the encodings of $n$, $r$, the target coordinates in order, and the matrix entries in row-major order. Each scalar is encoded by taking its library natural-number code, applying the library's natural-number-to-bit-string encoding to get a word $w$, and prefixing $w$ with $|w|$ true bits followed by one false bit. Strings without such a valid encoded instance, and instances satisfying neither distance condition, are outside both sets; dimension one is included. Polynomial time is witnessed in the library's TM2 machine model, using its product encoding of Boolean lists for verifier input, its Boolean output encoding for the verifier, and identity encodings for the reduction's input and output.

Additional targets:

• NP-hardness of binary nearest codeword with gap n^(1/200).
• NP-hardness of feasible binary syndrome decoding with gap n^(1/200).
• NP-hardness of rational finite-p lattice distance with gap n^(1/(200p)).

The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.

Sources: Lean formalization, H_GapCVP.json.

Planned collection: OAI Ten Proofs (oai-ten-proofs).

Arithmetic formula lower bounds for the permanent, from the OpenAI Ten Proofs formalization. The source already contains machine-checked proofs; this mission organizes its headline result and additional Comparator targets for reuse.

For every natural number $n\ge32$ and every finite arithmetic formula $f$ whose leaves are variables $x_{ij}$, $0\le i,j<n$, or arbitrary complex constants and whose binary operations are addition, subtraction, multiplication, and division, assume that every divisor subformula evaluates to a nonzero element of the fraction field of $\mathbb C[x_{ij}]$ and that the value of $f$ in this fraction field equals the polynomial $\operatorname{per}_n=\sum_{\sigma\in S_n}\prod_{i=0}^{n-1}x_{i,\sigma(i)}$ under the canonical inclusion. Then the number $V(f)$ of variable-leaf occurrences satisfies $n^4/(192\log_2 n)\le V(f)$, with both sides viewed as real numbers. Repeated occurrences are counted separately, constants contribute zero, and the leaves of both operands of each operation, including division, are counted. Nonzero divisors are required as rational functions, not at every numerical substitution.

Additional targets:

• Variable-leaf lower bound for division-free formulas computing the permanent.

The formalization uses Lean 4.33.1 with Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Its goal and milestone statements retain the validated source statements and their conventions.

Sources: Lean formalization, C_PermanentFormulaLowerBound.json.

Planned collection: OAI Ten Proofs (oai-ten-proofs).

Why the value of a nonlocal game matters

In a two-player one-round nonlocal game, a verifier samples a pair of questions, sends one to each of two players who cannot communicate, and accepts or rejects the pair of answers. The players may share an arbitrary quantum state and measure it; the entangled value of the game is the supremum of their acceptance probability over all such strategies. Nonlocal games are the operational form of Bell's theorem, the model behind device-independent cryptography and self-testing, and the engine of the complexity class $\mathrm{MIP}^*$ of languages decidable by a polynomial-time verifier interacting with entangled provers (Cleve, Høyer, Toner, Watrous, 2004, arXiv:quant-ph/0404076).

With classical provers, multiprover interactive proofs decide exactly $\mathrm{NEXP}$ (Babai, Fortnow, Lund, 1991, doi:10.1007/BF01200056). For entangled provers the lower bounds grew in steps: $\mathrm{NEXP} \subseteq \mathrm{MIP}^*$ (Ito, Vidick, 2012, arXiv:1207.0550), $\mathrm{NEEXP} \subseteq \mathrm{MIP}^*$ (Natarajan, Wright, 2019, arXiv:1904.05870), and finally $\mathrm{MIP}^* = \mathrm{RE}$ (Ji, Natarajan, Vidick, Wright, Yuen, 2020, arXiv:2001.04383): every recursively enumerable language, the halting problem included, has a two-prover one-round interactive proof with entangled provers, and the entangled value of a game cannot be approximated by any algorithm. Through the equivalences of Fritz (2012, arXiv:1008.1168), Junge, Navascués, Palazuelos, Pérez-García, Scholz, Werner (2011, arXiv:1008.1142) and Ozawa (2013, arXiv:1212.1700), the theorem gives a negative answer to Tsirelson's problem and to Connes' embedding problem for von Neumann algebras.

Synchronous games, their value, and game descriptions

Everything below is defined from scratch; the formal development uses exactly these objects.

A synchronous game $G = (X, A, \mu, D)$ has a finite question alphabet $X$ and a finite answer alphabet $A$, shared by both players, a probability distribution $\mu$ on $X \times X$, and a decision predicate $D(x, y, a, b) \in \{0, 1\}$ which, on equal questions $x = y$, rejects every pair of unequal answers $a \ne b$.

A synchronous strategy of dimension $d \ge 1$ assigns to each question $x$ a projective measurement $(M^x_a)_{a \in A}$ on $\mathbb{C}^d$: positive semidefinite matrices summing to the identity, each idempotent. Both players use the same measurements, and probabilities are taken in the normalized trace $\tau(M) = \operatorname{Tr}(M)/d$. The value of the strategy is

$$\omega(G, M) \;=\; \sum_{x, y \in X} \sum_{a, b \in A} \mu(x, y)\, D(x, y, a, b)\, \frac{\operatorname{Tr}\bigl(M^x_a M^y_b\bigr)}{d},$$

the acceptance probability when the players measure a maximally entangled state of dimension $d$. The synchronous value $\omega_{\mathrm{s}}(G)$ is the supremum of $\omega(G, M)$ over all synchronous strategies of all dimensions. A synchronous strategy is a tensor-product strategy, so $\omega_{\mathrm{s}}(G) \le \omega^*(G)$, the entangled value.

A game description $g$ is a finite object from which a synchronous game is read off: natural numbers $n_X, n_A$ fixing $X = \{0, \dots, n_X\}$ and $A = \{0, \dots, n_A\}$, a finite list of weighted question pairs $(x, y, w)$ and a finite list of accepted tuples $(x, y, a, b)$. The game $G_g$ has $\mu(x, y)$ proportional to the total weight listed for $(x, y)$ (the point mass at $(0, 0)$ if the total weight is zero), and $D$ accepts exactly the listed tuples, except that unequal answers to equal questions are rejected. Descriptions are coded as natural numbers, so a map from machines to descriptions can be computable.

Turing machines are Gödel numbers $c \in \mathcal{C}$ of partial recursive functions, an equivalent model of computation; "$c$ halts on the empty input" means that $c$ applied to $0$ is defined.

Formalization targets

Goal: halting reduces to the synchronous game value

There is a computable map $g$ from machines to game descriptions such that for every machine $c$,

$$c \text{ halts on the empty input} \;\Longrightarrow\; \omega_{\mathrm{s}}\bigl(G_{g(c)}\bigr) = 1, \qquad c \text{ does not halt} \;\Longrightarrow\; \omega_{\mathrm{s}}\bigl(G_{g(c)}\bigr) \le \tfrac12 .$$

This is Theorem 12.2 of arXiv:2001.04383 in synchronous form, with the running time of $g$ relaxed from polynomial to computable. It leaves the running time and the choice of value unfixed, and it is the weakest statement that already makes the game value uncomputable: no algorithm decides whether a game has synchronous value $1$ or at most $\tfrac12$.

Stronger: polynomial time, and the entangled value

The paper's statement has $g$ computable in polynomial time, and both the synchronous and the entangled value satisfy the two clauses. With polynomial time the goal gives $\mathrm{RE} \subseteq \mathrm{MIP}^*$ for the class $\mathrm{MIP}^*_{1, 1/2}(2, 1)$ of two-prover one-round proofs with completeness $1$ and soundness $\tfrac12$, and with the elementary inclusion $\mathrm{MIP}^* \subseteq \mathrm{RE}$ this is $\mathrm{MIP}^* = \mathrm{RE}$. These statements need a model of polynomial time and a definition of tensor-product strategies, and will be added as milestones once those definitions are published here.

Significance

The result. Approximating $\omega^*(G)$ to within a constant is as hard as the halting problem. A hierarchy of semidefinite programs converges from above to the commuting-operator value $\omega^{\mathrm{co}}(G)$, so the two values cannot coincide for every game: a negative answer to Tsirelson's problem and, by the equivalences cited above, to Connes' embedding problem, open since 1976. On the complexity side, $\mathrm{MIP}^* = \mathrm{RE}$ is the exact characterization of the power of entangled provers.

Formalizing it. The theorem is proved and its proof is machine-checked: HaltingGameValue.halting_reduces_to_gameValue in the Lean 4 development vidick/MIPRE-formalization proves exactly the goal above over Mathlib, with propext, Classical.choice and Quot.sound as its only axioms. The development is about 1,200 modules and 410,000 lines, including vendored components and a separate library for the low individual degree test; its blueprint records every statement, the dependency graph and the correspondence with the paper. This mission makes the result a fixed, auditable target: the definitional layer above is written over Mathlib alone, so the goal can be checked from first principles, and the components of the proof whose developments are self-contained are published as milestones with their proofs, to be imported, reused and re-proved. The first milestone, the recursive compression lemma of Marks, Nezhadi and Yuen (Lemma 5.1 of their manuscript; blueprint node lem:recursive-compression), comes with a complete proof over a dependency tree of 22 definition bundles and 60 theorems: a cost model of computation, an efficient universal machine, the s-m-n and Kleene recursion theorems, succinct descriptions.

Difficulty

The obvious approach fails at once: a verifier runs in time polynomial in its input, while a machine may run for arbitrarily long before halting, so no fixed game can check halting by simulation. What makes $\mathrm{RE}$ reachable is gap-preserving compression: a polynomial-time transformation of verifiers such that the compressed verifier, at index $n$, has value $1$ when the original verifier at index $2^n$ does, and value at most $\tfrac12$ when the original does. The compressed game is exponentially cheaper than the game it certifies, and a fixed-point argument through Kleene's recursion theorem, in the abstract form of the recursive compression lemma, turns compression into the halting reduction. Compression rests on three components, each with a central ingredient that is a theorem in its own right: question reduction by introspection, in which the players sample their own questions and a Pauli basis self-test built on the quantum low individual degree test certifies that they did; answer reduction, in which the players prove through a probabilistically checkable proof that their answers would have been accepted; and gap amplification by parallel repetition. In each component soundness must hold against strategies of unbounded dimension, where no finite enumeration or compactness argument is available, and the quantitative losses must compose so that the threshold $\tfrac12$ is preserved exactly.

Formalization scope

The goal is stated with the synchronous value, projective measurements on $\mathbb{C}^d$ with $d \ge 1$, and the normalized trace in place of a state vector; the real part of the trace is taken in the strategy value, and the synchronous value is the supremum, in $\mathbb{R}$, over all strategies of all dimensions (the values lie in $[0, 1]$). Game descriptions are interpreted with the fallback distribution above, so that the interpretation is total. Machines are Mathlib's Nat.Partrec.Code and computability is Mathlib's Computable; polynomial time is not fixed by the goal.

No trivializing formalization is available: the game depends on $c$ only through $g$, and the two clauses demand values $1$ and at most $\tfrac12$ on complementary sets of machines, so no map that ignores its argument, or produces only descriptions of zero total weight, satisfies the statement.

A complete development needs four layers: (i) a model of computation with costs, with polynomial-time maps, an efficient universal machine, the s-m-n and Kleene recursion theorems and succinct descriptions, which is the recursive compression milestone's dependency tree and is reusable in any undecidability argument by compression; (ii) normal form verifiers, conditionally linear samplers, the Pauli basis test and the quantum low individual degree test; (iii) the three transformations, with answer reduction over a PCP decider built from a succinct Cook–Levin theorem and direct parallel repetition in value form, and their soundness; (iv) the halting reduction from compression and the passage from the tensor-product to the synchronous value. Statements and proofs of these components over the shared definitional layer are welcome, as are alternative proofs of the goal from the same definitions, the polynomial-time and entangled-value strengthenings, and the inclusion $\mathrm{MIP}^* \subseteq \mathrm{RE}$.

Selected references

• Z. Ji, A. Natarajan, T. Vidick, J. Wright, H. Yuen, MIP* = RE, 2020 (revised 2022). arXiv:2001.04383
• Z. Ji, A. Natarajan, T. Vidick, J. Wright, H. Yuen, Quantum soundness of the classical low individual degree test, 2020. arXiv:2009.12982
• A. Marks, S. S. Nezhadi, H. Yuen, The recursive compression method for proving undecidability results, manuscript.
• J. Lin, Tracially embeddable strategies: lifting MIP* tricks to MIP^co, 2023. arXiv:2304.01940
• A. Natarajan, J. Wright, NEEXP ⊆ MIP*, FOCS 2019. arXiv:1904.05870
• T. Ito, T. Vidick, A multi-prover interactive proof for NEXP sound against entangled provers, FOCS 2012. arXiv:1207.0550
• R. Cleve, P. Høyer, B. Toner, J. Watrous, Consequences and limits of nonlocal strategies, CCC 2004. arXiv:quant-ph/0404076
• L. Babai, L. Fortnow, C. Lund, Non-deterministic exponential time has two-prover interactive protocols, Computational Complexity 1 (1991). doi:10.1007/BF01200056
• T. Fritz, Tsirelson's problem and Kirchberg's conjecture, Reviews in Mathematical Physics 24 (2012). arXiv:1008.1168
• M. Junge, M. Navascués, C. Palazuelos, D. Pérez-García, V. B. Scholz, R. F. Werner, Connes' embedding problem and Tsirelson's problem, Journal of Mathematical Physics 52 (2011). arXiv:1008.1142
• N. Ozawa, About the Connes embedding conjecture: algebraic approaches, Japanese Journal of Mathematics 8 (2013). arXiv:1212.1700
• The Lean development: vidick/MIPRE-formalization (statement MIPRE/HaltingGameValue.lean, proof MIPRE/MainTheorem.lean) and its blueprint.