All missions

Motivation: how many nested stars does a regular language need?

A regular expression describes a set of words using letters, union, concatenation and the Kleene star $P^*$ (any finite repetition of words from $P$). The star height of an expression is the depth of nesting of its stars, and it measures how many layers of unbounded repetition a regular language genuinely needs. For ordinary expressions this hierarchy is infinite. Allowing complement as an additional operation changes the picture: Boolean conditions can replace some layers of repetition, and the generalized star-height problem asks how far this goes. Whether every regular language has generalized star height at most some fixed number — and in particular whether one star always suffices — has been one of the longest-standing questions in the algebraic theory of automata.

Timeline

• 1963 — Eggan connects ordinary star height with the cycle structure of transition graphs and raises the question of its unboundedness (Michigan Math. J. 1963).
• 1965 — Schützenberger characterizes the star-free languages (generalized height $0$) as those recognized by finite aperiodic monoids (Inform. Control 1965).
• 1966 — Dejean and Schützenberger show that ordinary star height is unbounded already over a two-letter alphabet (Inform. Control 1966).
• 1992 — Pin, Straubing and Thérien prove generalized height at most one for languages recognized by finite nilpotent groups of class two and for further monoid classes (Inform. Comput. 1992, Theorems 7.3 and 7.8).
• 2002 — Straubing distinguishes the questions "is generalized star height bounded?" and "is it at most one?" in his account of the problem (LATIN 2002, p. 537).
• 2016–2017 — Bourne and Ruškuc prove height-one bounds for subword-counting languages with factors of length at most three (Theor. Comput. Sci. 2016); Bourne extends this to arbitrary fixed factors in his thesis (St Andrews, 2017, hdl:10023/12024).
• 2026 — Companion OpenAI preprints prove uniform bounds of thirteen (Finite Monoid Computations and a Uniform Generalized Star-Height Bound) and four (Generalized Star Height at Most Four).
• 2026 — The OpenAI preprint Generalized Star Height at Most Three (OpenAI Math Release, September 25, 2026) claims the bound three. It has not been peer reviewed and its theorem is not formally verified. Whether height one always suffices remains open; no language of generalized height greater than one is known.

Setting

Fix a finite alphabet $\Sigma$ and let $\Sigma^*$ be the set of finite words. A generalized regular expression over $\Sigma$ is built from the constants $0$ (denoting $\emptyset$) and $1$ (denoting $\{\varepsilon\}$), single letters $a\in\Sigma$, union $P\cup Q$, concatenation $PQ$, complement $\neg P$ (taken in $\Sigma^*$), and star $P^*$. Its height is defined by

$$h(0)=h(1)=h(a)=0,\quad h(P\cup Q)=h(PQ)=\max\{h(P),h(Q)\},\quad h(\neg P)=h(P),\quad h(P^*)=1+h(P).$$

For a regular language $L\subseteq\Sigma^*$, the generalized star height $h_\Sigma(L)$ is the least height of an expression over $\Sigma$ denoting $L$.

In Lean (namespace OAI.GeneralizedStarHeight), expressions are an inductive type Expression Alphabet with exactly these seven constructors, Expression.language interprets them in Mathlib's Language Alphabet (complement is Language complement, i.e. relative to all words), Expression.height is the recursion above, and HasHeightAtMost L n means some expression has language $L$ and height at most $n$.

Formalization targets

Goal: generalized star height at most three (Theorem 1.1)

For every finite alphabet $\Sigma$ and every regular language $L\subseteq\Sigma^*$,

$$h_\Sigma(L)\le 3 .$$

The goal is published on the platform with status Open.

Significance

The result itself. Before 2026 it was not known whether generalized star height is bounded at all; all positive results covered restricted families of monoids or languages. Theorem 1.1 gives a uniform bound independent of the alphabet and of the recognizing automaton, settling the boundedness question. It leaves open the sharper question of whether height one always suffices: no language is known to require height two. A uniform bound also implies that the hierarchy of generalized heights has at most four nonempty levels, which narrows where any separating example must be sought.

Formalizing it. The statement is short and fully elementary, but the proof composes many constructions (finite-monoid recognition, prefix codes of episodes, split identities, marker scales) whose height accounting is error-prone. A formal proof would certify the boundedness theorem itself. Mathlib already has regular languages (Language.IsRegular) and ordinary regular expressions; this mission adds generalized expressions with complement and their height.

Difficulty

The classical lower bounds for ordinary star height do not transfer once complement is allowed, and complement can simulate many but not obviously all counting arguments. The natural approach — write each fiber of a morphism from $\Sigma^*$ to a finite monoid by an expression that simulates the monoid computation letter by letter — needs one star per level of the computation's dependence on earlier history, and the depth of this dependence grows with the monoid. Group components are the difficulty: aperiodic monoids give height zero, but counting modulo $n$ and nonabelian group computations require stars, and a uniform bound must handle arbitrary finite groups nested inside arbitrary monoids without the number of stars growing with their size.

Formalization scope

• The alphabet is any Type u with [Finite Alphabet]; regularity is Mathlib's Language.IsRegular (acceptance by a finite-state DFA).
• Expressions must use letters of the same alphabet, so no auxiliary letters may be introduced; complement is relative to all words over that alphabet.
• height charges $1$ only for stars; complement, union and concatenation are free, exactly as in the source. Since HasHeightAtMost asks only for existence of an expression, no bound on expression size or computability is claimed, matching the source's remark that the construction bounds nesting only.
• Needed infrastructure: recognition of regular languages by finite monoids, prefix codes and unique factorization, and closure of bounded-height expressions under Boolean operations. The generalized-expression layer is reusable for the companion bounds (four and thirteen) and for formal work on star-free languages.

Selected references

• L. C. Eggan, Transition graphs and the star-height of regular events, Michigan Math. J. 10 (1963). https://doi.org/10.1307/mmj/1028998975
• M.-P. Schützenberger, On finite monoids having only trivial subgroups, Inform. Control 8 (1965). https://doi.org/10.1016/S0019-9958(65)90108-7
• F. Dejean and M.-P. Schützenberger, On a question of Eggan, Inform. Control 9 (1966). https://doi.org/10.1016/S0019-9958(66)90083-0
• J.-É. Pin, H. Straubing and D. Thérien, Some results on the generalized star-height problem, Inform. Comput. 101 (1992). https://doi.org/10.1016/0890-5401(92)90063-L
• H. Straubing, On logical descriptions of regular languages, LATIN 2002, LNCS 2286. https://doi.org/10.1007/3-540-45995-2_46
• T. Bourne and N. Ruškuc, On the star-height of subword counting languages and their relationship to Rees zero-matrix semigroups, Theor. Comput. Sci. 653 (2016). https://doi.org/10.1016/j.tcs.2016.09.024
• T. Bourne, Counting subwords and other results related to the generalised star-height problem for regular languages, PhD thesis, University of St Andrews, 2017. https://hdl.handle.net/10023/12024
• OpenAI, Generalized Star Height at Most Three, OpenAI Math Release preprint, September 25, 2026 (Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Generalized-Star-Height-at-Most-Three-September-25-2026/article.pdf

Motivation

Weisfeiler–Leman (WL) refinement compares two graphs by repeatedly refining colors of ordered vertex $k$-tuples. For every fixed dimension $k$ this is a polynomial-time procedure, with running time $n^{O(k)}$. When $k$ is part of the input, that computation is no longer polynomial, and the complexity of deciding the outcome becomes a question in its own right. Seppelt (2024) proved coNP-hardness and recorded Berkholz's question whether the problem is EXPTIME-complete.

This preprint answers that question for the joint-update convention: deciding $k$-WL equivalence of two explicit graphs with $k$ in binary is EXPTIME-complete, even on connected graphs of maximum degree three.

Background

• 1968. Weisfeiler and Leman introduce the refinement method.
• 1982. Luks shows isomorphism of graphs of bounded degree is decidable in polynomial time.
• 1992. Cai, Fürer and Immerman construct degree-three graphs with small color classes that remain indistinguishable with linearly many counting variables.
• 2019. Kiefer and Neuen record the joint-update convention and its bijective $(k+1)$-pebble game characterization.
• 2024–2025. Seppelt, and independently Lichter, Raßmann and Schweitzer, prove coNP-hardness of WL equivalence with the dimension as input. Grohe, Lichter, Neuen and Schweitzer compress CFI graphs to obtain long refinement sequences.
• 2026. The OpenAI preprint Variable-dimension Weisfeiler–Leman equivalence on general and subcubic graphs (dated September 25, 2026) proves EXPTIME-completeness; companion preprints treat identification and fixed-dimension time lower bounds. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

Graphs are finite, simple, undirected and uncolored, given by adjacency matrices. In the joint-update convention a $k$-tuple's initial color records equalities and adjacencies among its entries; each round adjoins to the old color the multiset, over replacement vertices $z$, of the vector of $k$ old colors obtained by replacing each coordinate in turn by $z$. Color names are common to both graphs, and $G \equiv_k H$ means their $k$-tuple color histograms agree at every round.

The language $\mathrm{WL}$ consists of encodings $(G, H, k)$ with $k \ge 2$ in binary and $G \equiv_k H$. The language $\mathrm{SubWL}$ additionally requires $G$ and $H$ to be connected, of the same positive order, and of maximum degree at most three. Malformed encodings are excluded.

In Lean (OAI.VariableWL), Graph is a SimpleGraph on Fin order, color and histogram implement the joint update by recursion on rounds, pairCode concatenates the two graph codes (order header plus row-major matrix) and the code of $k$, and complexity classes are defined from an explicit deterministic Turing machine model with OutputsWithin, InEXPTIME, PolytimeReduces and EXPTIMEComplete.

Formalization targets

Goal: Theorem 1.1

Both $\mathrm{WL}$ and $\mathrm{SubWL}$ are EXPTIME-complete under deterministic polynomial-time many-one reductions:

$$\mathrm{WL},\ \mathrm{SubWL} \in \mathrm{EXPTIME}, \qquad L \le_p \mathrm{WL} \text{ and } L \le_p \mathrm{SubWL} \text{ for every } L \in \mathrm{EXPTIME}.$$

Significance

The result. Theorem 1.1 resolves the question recorded by Seppelt and strengthens the known coNP-hardness to EXPTIME-completeness. The subcubic case is notable because isomorphism of bounded-degree graphs is polynomial-time (Luks), yet equivalence under refinement at a supplied dimension remains EXPTIME-complete for degree three; nonisomorphic graphs can be equivalent. Corollary 8.3 shows hardness persists with $k$ in unary.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The uniform computation interface developed here is reused by the companion identification paper, so a formalization would serve both missions.

Difficulty

Membership requires showing that the dimension can be capped before allocating tuple tables (Lemma 2.2), since $k$ may exceed the graph order. Hardness requires simulating an arbitrary exponential-time computation by a graph pair whose WL equivalence at a polynomially encoded dimension reflects acceptance. Because the number of address coordinates grows with the input, fixed-dimension constructions with dimension-dependent constants do not give a uniform polynomial-time reduction, and in the subcubic case colors must be realized by uncolored degree-three gadgets that a winning strategy still recognizes.

Formalization scope

• Graphs: SimpleGraph (Fin order); Subcubic bounds every vertex degree by three; SubWL also demands positive equal orders and connectivity.
• Equivalence quantifies over all rounds $s$; colors are nested Multiset types.
• Dimension $k \ge 2$ is encoded in binary after a unary length header.
• The Turing machine model is explicit; EXPTIME bounds are $2^{c(n+1)^d}$ and reductions run in $c(n+1)^d$ steps.

The statement is not trivial: both membership and hardness are required for both languages.

Needed infrastructure: the bijective game characterization (Lemma 2.4), product-circuit compilation (Proposition 3.2), the general and subcubic realizations (Propositions 5.1 and 7.1) and the uniform compiler (Proposition 8.2). Contributions toward any of these are welcome.

Selected references

• OpenAI, Variable-dimension Weisfeiler–Leman equivalence on general and subcubic graphs, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Variable-dimension-Weisfeiler-Leman-equivalence-on-general-and-subcubic-graphs-September-25-2026/paper.pdf
• OpenAI, The complexity of identifying a graph by Weisfeiler–Leman refinement, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/main/preprints/The-complexity-of-identifying-a-graph-by-Weisfeiler-Leman-refinement-September-25-2026/paper.pdf
• B. Weisfeiler, A. Leman, The Reduction of a Graph to Canonical Form and the Algebra Which Appears Therein, 1968. https://www.iti.zcu.cz/wl2018/pdf/wl_paper_translation.pdf
• J.-Y. Cai, M. Fürer, N. Immerman, An Optimal Lower Bound on the Number of Variables for Graph Identification, Combinatorica 12 (1992). https://doi.org/10.1007/BF01305232
• E. M. Luks, Isomorphism of Graphs of Bounded Valence Can Be Tested in Polynomial Time, J. Comput. Syst. Sci. 25 (1982). https://doi.org/10.1016/0022-0000(82)90009-5
• S. Kiefer, D. Neuen, The Power of the Weisfeiler–Leman Algorithm to Decompose Graphs, MFCS 2019.
• T. Seppelt, An Algorithmic Meta Theorem for Homomorphism Indistinguishability, MFCS 2024.
• M. Lichter, S. Raßmann, P. Schweitzer, Computational Complexity of the Weisfeiler–Leman Dimension, CSL 2025. https://doi.org/10.4230/LIPIcs.CSL.2025.13
• M. Grohe, M. Lichter, D. Neuen, P. Schweitzer, Compressing CFI Graphs and Lower Bounds for the Weisfeiler–Leman Refinements, J. ACM 72 (2025). https://doi.org/10.1145/3727978

Motivation

The Weisfeiler–Leman (WL) method colors $k$-tuples of vertices by repeatedly recording their local extension patterns; two graphs are $k$-WL equivalent when the stable color histograms agree. For each fixed $k$ the direct algorithm runs in time $n^{O(k)}$: there are $n^k$ tuples and polynomially many refinement rounds. The question is whether the growing exponent is necessary for any algorithm deciding the equivalence relation, not just for implementations of refinement.

This preprint proves that it is, unconditionally: for every sufficiently large fixed $k$, every deterministic sequential decider for $k$-WL equivalence needs time $n^{ck}$ at every sufficiently large graph order, without assuming the Exponential Time Hypothesis.

Background

• 1966. Hennie and Stearns use padded machine indices and clocked self-simulation in their time-hierarchy proof.
• 1968. Weisfeiler and Leman introduce the refinement method.
• 1992. Cai, Fürer and Immerman's parity constructions establish limits of bounded-variable graph identification.
• 1996. Hella introduces the bijective pebble game characterizing counting-logic equivalence.
• 1999. Grohe proves equivalence in finite-variable logics is complete for polynomial time.
• 2013. Berkholz proves unconditional time lower bounds with exponent linear in the number of pebbles for existential pebble games.
• 2024–2025. Seppelt, and Lichter, Raßmann and Schweitzer, prove coNP-hardness of WL equivalence when the dimension is part of the input. Grohe, Lichter, Neuen and Schweitzer prove $\Omega_k(n^{k/2})$ lower bounds on the number of refinement rounds via compressed CFI graphs; such bounds do not constrain other algorithms deciding the equivalence.
• 2026. The OpenAI preprint Unconditional time lower bounds for Weisfeiler–Leman equivalence (dated September 25, 2026) proves the bound stated below. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

Graphs are finite, simple, undirected and uncolored, given as $n \times n$ adjacency matrices. For a $k$-tuple, the initial color records coordinate equalities and adjacencies. Each refinement step keeps the old color and adds, in the joint convention, the multiset over vertices $z$ of the $k$-vectors of colors obtained by replacing each coordinate by $z$; in the separate convention, one such multiset per coordinate. Two $n$-vertex graphs are $k$-WL equivalent if their color histograms agree at every round.

A decider for a convention and dimension $k$ is a deterministic machine that halts on every encoded pair of $n$-vertex graphs and accepts exactly the equivalent pairs. Its worst-case time $T_A(n)$ is the maximum running time over pairs of $n$-vertex graphs (optionally restricted to connected graphs of diameter at most two).

In Lean (OAI.WLTime), Graph n is a symmetric loopless Boolean matrix on Fin n, tupleColor and histogram define both conventions by recursion on rounds, Equivalent compares all rounds, encodePair encodes $n$ and both matrices, and machines are either multitape Turing machines (TM) or logarithmic-word RAMs (RAM) whose word operations are themselves implemented by Turing machines in time polynomial in the word length.

Formalization targets

Goal: Theorem 1.1

There are absolute constants $c > 0$ and $k_0$ such that for every fixed $k \ge k_0$, either convention, either input class (all graphs, or connected graphs of diameter at most two) and every correct deterministic decider $A$ in either machine model, there is $n_0 = n_0(A, k)$ with

$$T_A(n) \ge n^{ck} \qquad \text{for every } n \ge n_0 .$$

The exponent constant $c$ is independent of $k$ and of the program; the threshold $n_0$ may depend on both. The bound holds at every large order, not only infinitely often.

Significance

The result. Theorem 1.1 rules out any running time $f(k)\,n^{g(k)}$ with $g(k) = o(k)$, unconditionally. Earlier lower bounds either concerned the number of refinement rounds, assumed ETH, or treated the dimension as part of the input (coNP- and EXPTIME-hardness), which does not give a fixed-dimension exponent. It covers both standard update conventions and the restricted class of diameter-two graphs.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. The Lean statement fixes explicit machine models, so a proof would include a verified padded diagonalization (Theorem 5.2), a verified computation-to-graph reduction (Theorem 4.3) and a verified compressed consistency construction (Theorem 3.2).

Difficulty

Unconditional time lower bounds in concrete models are rare; the only general technique is diagonalization, which yields hard languages but not hard natural problems. The proof must therefore transfer a diagonal language to WL equivalence through a reduction that is efficient enough to preserve an exponent linear in $k$. A polynomial-time computation with exponent proportional to $k$ has too many addressed locations to list in a small reduction, and local consistency is symmetric whereas a computation must propagate information forward without forcing false predecessors to become true.

Formalization scope

• Decides A c k p requires halting and correctness on every pair in the input class at every order $n$; worstTime is a Finset.sup over pairs in the class.
• Diameter two includes $n > 0$ and every pair of vertices equal, adjacent, or with a common neighbour (hence connected).
• Turing machines have finitely many tapes, states and symbols; RAM words have $O(\log(n+2))$ bits, and RAM instructions are fixed finite programs whose word operations carry a polynomial-time implementation.
• Time is a natural number; the bound $n^{ck}$ is compared in ℝ.

The statement is not vacuous: correct deciders exist (direct refinement), so the conclusion constrains real algorithms.

Needed infrastructure: bijective pebble games and their equivalence with refinement (Lemma 2.3), Turing machine simulation and clocking, and the graph constructions of Sections 3–4. Contributions toward any of these components are welcome.

Selected references

• OpenAI, Unconditional time lower bounds for Weisfeiler–Leman equivalence, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Unconditional-time-lower-bounds-for-Weisfeiler-Leman-equivalence-September-25-2026/paper.pdf
• B. Weisfeiler, A. Leman, The Reduction of a Graph to Canonical Form and the Algebra Which Appears Therein, 1968. https://www.iti.zcu.cz/wl2018/pdf/wl_paper_translation.pdf
• J.-Y. Cai, M. Fürer, N. Immerman, An Optimal Lower Bound on the Number of Variables for Graph Identification, Combinatorica 12 (1992). https://doi.org/10.1007/BF01305232
• L. Hella, Logical Hierarchies in PTIME, Information and Computation 129 (1996). https://doi.org/10.1006/inco.1996.0070
• F. C. Hennie, R. E. Stearns, Two-Tape Simulation of Multitape Turing Machines, J. ACM 13 (1966). https://doi.org/10.1145/321356.321362
• C. Berkholz, Lower Bounds for Existential Pebble Games and k-Consistency Tests, Logical Methods in Computer Science 9 (2013).
• M. Grohe, Equivalence in Finite-Variable Logics Is Complete for Polynomial Time, Combinatorica 19 (1999). https://doi.org/10.1007/s004939970004
• M. Grohe, M. Lichter, D. Neuen, P. Schweitzer, Compressing CFI Graphs and Lower Bounds for the Weisfeiler–Leman Refinements, J. ACM 72 (2025). https://doi.org/10.1145/3727978
• M. Lichter, S. Raßmann, P. Schweitzer, Computational Complexity of the Weisfeiler–Leman Dimension, arXiv:2402.11531, 2024. https://arxiv.org/abs/2402.11531
• T. Seppelt, An Algorithmic Meta Theorem for Homomorphism Indistinguishability, MFCS 2024.

Motivation

The Weisfeiler–Leman (WL) algorithm refines colors of vertex tuples to test graph isomorphism, and its dimension $k$ controls how much tuple information is used. A graph's Weisfeiler–Leman dimension $\mathrm{WLdim}(G)$ is the least $k$ for which $k$-WL refinement identifies $G$, i.e. distinguishes it from every non-isomorphic graph. This is a standard measure of the descriptive complexity of an individual graph, tied to counting logics and pebble games. The question here is how hard it is to compute: given $G$ and $k$, decide whether $\mathrm{WLdim}(G) \le k$.

Identification differs from testing whether a given pair of graphs is equivalent: it quantifies over every possible comparison graph. The preprint shows the problem is EXPTIME-complete when $k$ is part of the input.

Background

• 1968. Weisfeiler and Leman introduce the refinement method.
• 1992. Cai, Fürer and Immerman relate WL to counting logic and pebble games and construct parity graphs needing linear dimension.
• 2017. Arvind, Köbler, Rattan and Verbitsky prove P-hardness of identification by color refinement (dimension one).
• 2019. Kiefer and Neuen give a game formulation used to analyze WL decompositions.
• 2024. Seppelt proves coNP-hardness of variable-dimension pair equivalence.
• 2025. Lichter, Raßmann and Schweitzer prove P-hardness of identification for each fixed $k \ge 2$ and NP-hardness when the dimension is part of the input, including on simple uncolored graphs; they also prove coNP-hardness of pair equivalence independently. Grohe, Lichter, Neuen and Schweitzer introduce compressed CFI graphs for round lower bounds.
• 2026. The OpenAI preprint The complexity of identifying a graph by Weisfeiler–Leman refinement (dated September 25, 2026) proves EXPTIME-completeness, building on the companion preprint on variable-dimension WL equivalence. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

All graphs are finite, simple, undirected and uncolored. For $k \ge 2$ the joint-update convention is used: a $k$-tuple starts with its equality and adjacency type, and each round adjoins the multiset over vertices $z$ of the vector of colors obtained by replacing each coordinate by $z$. For $k = 1$ ordinary color refinement is used. Colors are shared between graphs. $G \equiv_k H$ means the tuple-color histograms agree at every round. $k$-WL identifies $G$ if $G \equiv_k H$ implies $G \cong H$ for every graph $H$, and $\mathrm{WLdim}(G)$ is the least positive such $k$.

The decision problem takes a nonempty graph $G$ by its adjacency matrix and a positive integer $k$ in binary, and asks whether $\mathrm{WLdim}(G) \le k$; malformed inputs are rejected.

In Lean (OAI.WLIdentification), Graph is an order with a symmetric loopless Boolean adjacency on Fin order; Equivalent, Identifies and WLdim follow the definitions above; inputs are bit words consisting of a unary order header, the row-major matrix and the binary dimension; complexity classes are defined from an explicit deterministic single-tape Turing machine model (Machine, run, DecidesWithin, InEXPTIME, PolytimeManyOne, EXPTIMEComplete).

Formalization targets

Goal: Theorem 1.1

The language

$$\{\langle G, k\rangle : G \text{ nonempty},\ k \ge 1,\ \mathrm{WLdim}(G) \le k\}$$

is EXPTIME-complete under deterministic polynomial-time many-one reductions: it is decidable in time $2^{C(n+1)^d}$, and every EXPTIME language reduces to it in polynomial time.

Significance

The result. Theorem 1.1 settles the complexity of the input-dimension identification problem, strengthening the NP-hardness of Lichter, Raßmann and Schweitzer to EXPTIME-completeness. By Corollary 7.3 hardness persists with $k$ in unary, so it does not come from exponentially large numerical dimensions.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. A formal proof would include a verified reduction from arbitrary exponential-time Turing machine computations to graphs, and a verified upper bound for WL identification. The Turing-machine model and the WL definitions in the Lean statement are reusable for the companion missions on WL equivalence.

Difficulty

Hardness must handle the all-mates quantifier: an encoding of a computation into a graph must ensure that every graph $H$ that is $k$-WL equivalent to it is isomorphic to it exactly when the computation accepts. Local recognition of gadgets, as in earlier NP-hardness proofs, shows each incidence piece of $H$ has an allowed pattern, but the encoding here admits a whole family of shifted constraints, and one must show every shift arising from an equivalent mate lifts to a single global isomorphism on accepting instances. Membership in EXPTIME is also not immediate, since identification quantifies over infinitely many comparison graphs.

Formalization scope

• Graphs are Fin n-indexed Boolean adjacency matrices; the problem language requires a nonempty graph, a binary word with leading bit true, and a positive value.
• WLdim G is sInf of the positive identifying dimensions; this set is nonempty for finite graphs (dimension equal to the order identifies), so the infimum is not the default value.
• Time is counted in steps of the explicit Turing machine on the input length; EXPTIME uses bounds $2^{C(n+1)^d}$ and reductions use bounds $C(n+1)^d$.

The goal is not trivial: membership in EXPTIME and hardness under the explicit machine model are both required.

Needed infrastructure: WL refinement monotonicity, pebble games or an equivalent characterization, CFI-type gadget constructions, and Turing-machine simulation. Contributions toward the upper bound (Proposition 7.1) or the reconstruction results of Sections 3–5 are welcome.

Selected references

• OpenAI, The complexity of identifying a graph by Weisfeiler–Leman refinement, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-complexity-of-identifying-a-graph-by-Weisfeiler-Leman-refinement-September-25-2026/paper.pdf
• OpenAI, Variable-dimension Weisfeiler–Leman equivalence on general and subcubic graphs, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/main/preprints/Variable-dimension-Weisfeiler-Leman-equivalence-on-general-and-subcubic-graphs-September-25-2026/paper.pdf
• B. Weisfeiler, A. Leman, The Reduction of a Graph to Canonical Form and the Algebra Which Appears Therein, Nauchno-Technicheskaya Informatsiya, 1968. https://www.iti.zcu.cz/wl2018/pdf/wl_paper_translation.pdf
• J.-Y. Cai, M. Fürer, N. Immerman, An Optimal Lower Bound on the Number of Variables for Graph Identification, Combinatorica 12 (1992). https://doi.org/10.1007/BF01305232
• V. Arvind, J. Köbler, G. Rattan, O. Verbitsky, Graph Isomorphism, Color Refinement, and Compactness, Computational Complexity 26 (2017).
• M. Lichter, S. Raßmann, P. Schweitzer, Computational Complexity of the Weisfeiler–Leman Dimension, CSL 2025. https://doi.org/10.4230/LIPIcs.CSL.2025.13 (full version https://arxiv.org/abs/2402.11531)
• T. Seppelt, An Algorithmic Meta Theorem for Homomorphism Indistinguishability, MFCS 2024.
• M. Grohe, M. Lichter, D. Neuen, P. Schweitzer, Compressing CFI Graphs and Lower Bounds for the Weisfeiler–Leman Refinements, J. ACM 72 (2025). https://doi.org/10.1145/3727978
• S. Kiefer, D. Neuen, The Power of the Weisfeiler–Leman Algorithm to Decompose Graphs, MFCS 2019.

Motivation

The Weisfeiler–Leman (WL) method is the standard combinatorial heuristic for graph isomorphism: it repeatedly refines colors of $k$-tuples of vertices, and two graphs it cannot tell apart are called $k$-WL equivalent. It is equivalent to counting-logic indistinguishability and, by results of Dvořák (2010) and Dell, Grohe and Rattan (2018), to equality of homomorphism counts from graphs of treewidth below $k$ (bags of size at most $k+1$). For fixed $k$, direct refinement decides $k$-WL equivalence in $n^{O(k)}$ time; whether the growing exponent is necessary is a natural complexity question.

This preprint gives an exact reduction from a simple constraint problem (choosing compatible elements from finite domains) to $k$-WL equivalence of two explicit uncolored graphs, and uses it to derive $n^{\Omega(k)}$ conditional time lower bounds.

Background

• 1968. Weisfeiler and Leman introduce the refinement method for graph canonization.
• 1992. Cai, Fürer and Immerman construct parity (CFI) graph pairs of bounded degree that need WL dimension linear in their order.
• 1999. Grohe shows equivalence in finite-variable logics is complete for polynomial time.
• 2001. Impagliazzo and Paturi formulate the Exponential Time Hypothesis; Impagliazzo, Paturi and Zane give sparsification.
• 2010, 2018. Dvořák, and Dell–Grohe–Rattan, characterize $k$-WL equivalence by homomorphism counts from bounded-treewidth graphs.
• 2019. Atserias, Mančinska, Roberson, Šámal, Severini and Varvitsiotis encode solutions of binary linear systems as graph vertices.
• 2025. Grohe, Lichter, Neuen and Schweitzer prove $\Omega(n^{k/2})$ round lower bounds for joint refinement; Lichter, Raßmann and Schweitzer conjecture that WL equivalence and identification do not admit $n^{o(k)}$ time.
• 2026. The OpenAI preprint Parity lifts and bounded-treewidth witnesses for Weisfeiler–Leman equivalence (dated September 25, 2026) proves the parity reduction below. It has not been peer reviewed; the Lean goal is open on this platform.

Setting

Fix $k \ge 4$. The atomic type of a tuple $\mathbf{x} \in V(X)^k$ records all equalities and adjacencies among its entries. In joint refinement a round records the old color of $\mathbf x$ and the multiset over $y \in V(X)$ of the vectors $(C_r(\mathbf x[1\leftarrow y]), \dots, C_r(\mathbf x[k\leftarrow y]))$. In separate refinement it records the old color and the $k$ multisets $\{\!\{C_r(\mathbf x[i\leftarrow y]) : y\}\!\}$. Two graphs are $k$-WL equivalent ($\equiv_k$) when their tuple-color histograms agree at every round. The bag parameter is $t = k+1$ (joint) or $t = k$ (separate).

A choice system on $t$ domains consists of finite sets $D_1, \dots, D_t$ and, for each pair $i < j$, a finite label set $L_{ij}$ with maps $\lambda^i_{ij} : D_i \to L_{ij}$, $\lambda^j_{ij} : D_j \to L_{ij}$. A successful choice is $(d_1, \dots, d_t) \in \prod_i D_i$ with $\lambda^i_{ij}(d_i) = \lambda^j_{ij}(d_j)$ for all $i < j$. Empty domains are allowed.

In Lean (OAI.ParityWL), ChoiceSystem t packages the domains and labels, template t is the $t$-clique with helpers, baseGraph C replaces template types by domains and labels, and zeroLift C, starLift C are the two parity lifts. Colors are defined by recursion on rounds (jointColor, separateColor) with histograms compared as multisets.

Formalization targets

Goal: Theorem 1.2 (Parity reduction)

For $k \ge 4$, either convention and the corresponding $t$, for every choice system on $t$ domains the two explicit uncolored simple graphs $X_0, X_\star$ have equal order and

$$X_0 \equiv_k X_\star \iff \text{the choice system has no successful choice},$$

both with common color names on separate graphs and with pure-tuple comparison in the disjoint union. If every domain and label set has size at most $A \ge 1$, the common order is at most $A M_t$ with

$$M_t = t\, 2^{\,t-2+3\binom{t-1}{2}} + 12\binom{t}{3}.$$

When a successful choice exists, the histograms already differ after two joint rounds or one separate round.

Significance

The result. The reduction turns compatible-choice problems, which encode sparse satisfiability, into WL equivalence of uncolored graphs whose size grows only linearly in the domain size. Combined with sparsification it gives Theorem 1.3: under the positive-rate ETH there are $c > 0$, $K \ge 4$ such that no deterministic algorithm decides $k$-WL equivalence of $n$-vertex graphs in time $O(n^{ck})$ for fixed $k \ge K$, even when only early-round histograms are compared. This addresses the expectation stated by Lichter, Raßmann and Schweitzer.

Formalizing it. No machine-checked proof exists; the source is an unrefereed preprint. A formalization would also give Lean definitions of both WL conventions, reusable by the companion missions in this family on identification and unconditional lower bounds. The ETH consequence (Theorem 1.3) is not part of the Lean goal.

Difficulty

The forward direction (a successful choice yields a distinguishing homomorphism test detected in few rounds) is constructive. The converse is the hard part: one must show that every bounded-treewidth homomorphism test that distinguishes the lifts yields a successful choice, even when bags do not induce cliques, projected images repeat, and some weights vanish. A naive argument that counts only type-preserving homomorphisms fails because non-type-preserving maps also contribute to $\hom(F, X_0) - \hom(F, X_\star)$.

Formalization scope

• Graphs are SimpleGraph on finite types; the lifts' vertex types are sigma types of base vertices with parity tags.
• WL colors are nested Multiset-valued types defined by recursion on the round number; equivalence quantifies over all rounds $r$.
• The order bound uses orderFactor t = t * 2^(t-2+3*(t-1).choose 2) + 12 * t.choose 3 with natural-number subtraction (harmless since $t \ge 4$).
• Successful is an existential over dependent tuples; empty domains are allowed, in which case no successful choice exists and the lifts must be equivalent.

The goal is not trivial: the biconditional pins down equivalence exactly, and the detection clause fixes the round.

Needed infrastructure: tree decompositions and homomorphism counts, the Dvořák/Dell–Grohe–Rattan interface for both conventions, and $\mathbb{F}_2$ linear algebra for the parity lifts. Contributions toward either direction of the equivalence are welcome.

Selected references

• OpenAI, Parity lifts and bounded-treewidth witnesses for Weisfeiler–Leman equivalence, OpenAI Math Release preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Parity-lifts-and-bounded-treewidth-witnesses-for-Weisfeiler-Leman-equivalence-September-25-2026/paper.pdf
• B. Weisfeiler, A. Leman, The Reduction of a Graph to Canonical Form and the Algebra Which Appears Therein, 1968. https://www.iti.zcu.cz/wl2018/pdf/wl_paper_translation.pdf
• J.-Y. Cai, M. Fürer, N. Immerman, An Optimal Lower Bound on the Number of Variables for Graph Identification, Combinatorica 12 (1992). https://doi.org/10.1007/BF01305232
• Z. Dvořák, On Recognizing Graphs by Numbers of Homomorphisms, J. Graph Theory (2010). https://doi.org/10.1002/jgt.20461
• H. Dell, M. Grohe, G. Rattan, Lovász Meets Weisfeiler and Leman, ICALP 2018. https://doi.org/10.4230/LIPIcs.ICALP.2018.40
• A. Atserias et al., Quantum and Non-Signalling Graph Isomorphisms, J. Combin. Theory Ser. B (2019). https://doi.org/10.1016/j.jctb.2018.11.002
• R. Impagliazzo, R. Paturi, On the Complexity of k-SAT, J. Comput. Syst. Sci. (2001). https://doi.org/10.1006/jcss.2000.1727
• M. Grohe, M. Lichter, D. Neuen, P. Schweitzer, Compressing CFI Graphs and Lower Bounds for the Weisfeiler–Leman Refinements, J. ACM (2025). https://doi.org/10.1145/3727978
• M. Lichter, S. Raßmann, P. Schweitzer, Computational Complexity of the Weisfeiler–Leman Dimension, CSL 2025. https://doi.org/10.4230/LIPIcs.CSL.2025.13

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 discrete Fourier transform of length $n$ is computed by the fast Fourier transform with $O(n\log n)$ arithmetic operations, and this has been the benchmark since Cooley and Tukey (1965). Whether $\Omega(n\log n)$ operations are necessary is one of the basic open questions of algebraic complexity theory. Lower bounds of order $n\log n$ are known only under restrictions on the algorithm: bounded coefficients, unitary $2\times2$ gates on exactly $n$ registers, or bounded conditioning of intermediate maps. In the unrestricted model of linear circuits, where coefficients are arbitrary complex numbers and only arithmetic operations are counted, the question remained open. This mission concerns that unrestricted question.

Timeline

• 1958. Good gives the multidimensional (coprime-factor) form of the Fourier transform (doi:10.1111/j.2517-6161.1958.tb00300.x).
• 1965. Cooley and Tukey publish the fast Fourier transform (doi:10.1090/S0025-5718-1965-0178586-1).
• 1969–1970. Rabiner, Schafer and Rader (chirp $z$-transform) and Bluestein reduce arbitrary lengths to convolution (doi:10.1109/TAU.1969.1162034, doi:10.1109/TAU.1970.1162132).
• 1973. Morgenstern proves an $\Omega(n\log n)$ lower bound for linear circuits with bounded coefficients (doi:10.1145/321752.321761).
• 2013–2014. Ailon proves lower bounds for $2\times2$ unitary gate models and for well-conditioned computations (arXiv:1305.4745, arXiv:1403.1307).
• 2023. Alman and Rao improve the leading constants for power-of-two transforms via matrix non-rigidity (doi:10.1145/3564246.3585188).
• 2025. Alman and Li characterize asymptotic sizes of depth-two circuits for Kronecker powers (arXiv:2509.14489).

The source of this mission, an OpenAI preprint dated September 25, 2026, claims that the $\Omega(n\log n)$ lower bound fails in the unrestricted complex linear-circuit model.

Setting

For $n\ge2$ let $\zeta_n=e^{2\pi i/n}$ and $F_n=(\zeta_n^{jk})_{0\le j,k<n}$. A linear circuit of length $n$ has inputs $x_0,\dots,x_{n-1}$ and the constant $0$, followed by a finite sequence of gates. Each gate computes $u+v$, $u-v$ or $\lambda u$ from previously available values $u,v$, where $\lambda\in\mathbb C$ is a fixed coefficient; each gate costs one. Values may be reused arbitrarily, and the $n$ outputs are designated available values. The circuit computes $F_n$ if its outputs equal $F_nx$ for every $x\in\mathbb C^n$. Coefficients may depend on $n$ and have no bound on size or description; depth, storage and conditioning are unrestricted. Let $L(n)$ be the minimum number of gates.

Formalization targets

Goal: Theorem 1.1

$$\liminf_{n\to\infty}\frac{L(n)}{n\log_2 n}=0,$$

equivalently: for every $c>0$ and every $N_0\ge2$ there are $n\ge N_0$ and an exact circuit for $F_n$ with fewer than $c\,n\log_2 n$ gates. The Lean statement OAI.ExactFourier.main_theorem is this second form and is open on the platform.

The statement does not assert an upper bound for every length, a uniform construction, or anything about numerical stability. A companion OpenAI preprint gives a quantitative all-length bound in a model that also charges coefficient preparation; that result is not part of this mission.

Significance

The theorem refutes the assertion that $L(n)\ge c\,n\log_2n$ for some fixed $c>0$ and all large $n$ in the unrestricted linear model. It shows that the known lower bounds necessarily depend on their restrictions (bounded coefficients, conditioning, unitary gates). The mechanism, a single finite tensor saving amplified through tensor powers, is a general tool: one strict improvement over the standard axis-by-axis algorithm for one tensor power of one nonmonomial matrix yields an exponent improvement for all tensor powers.

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists. The existence part of the argument is non-constructive (it proceeds by contradiction through price functions and compactness), so a formal proof is a meaningful check.

Difficulty

Leading-constant improvements of the FFT do not change the $n\log n$ scale, and every classical structural algorithm (Cooley–Tukey, Good–Thomas, chirp) has that scale. A gain in the exponent of the logarithm needs a saving that compounds across many tensor factors; but a saving for one tensor power of a small matrix does not obviously transfer to Fourier matrices of growing length, because Fourier factorizations introduce diagonal twiddle factors and change the coordinate set. In addition, the existence of a single finite saving is itself not exhibited explicitly and must be proved.

Formalization scope

• Gate w is add i j, sub i j or scale c i with c : ℂ, referencing the $w$ values available so far.
• Program n k is a list of $k$ gates in topological order; values $0,\dots,n-1$ are the inputs and value $n$ is the constant $0$ (via Fin.snoc x 0).
• Circuit n has size, a program of that size, and outputs : Fin n → Fin (n+1+size); output selection is free.
• fourierMatrix n j k = zeta n ^ (j*k) with zeta n = exp(2πi/n); Computes is equality with mulVec for every input.
• MainStatement: for every real $c>0$ and $N_0\ge2$ there are $n\ge N_0$ and a computing circuit with size < c * n * logb 2 n.

A complete development needs tensor products of matrices and circuits, the Chinese Remainder (Good–Thomas) identification of $F_{rs}$ with $F_r\otimes F_s$ for coprime $r,s$, a Toeplitz/Vandermonde factorization of $F_r$ on its own coordinates, and the price-function existence argument (separation, compactness, feedback). Contributions formalizing Lemma 2.3 (tensor amplification) and Proposition 3.4 (transfer of a finite win to Fourier circuits) are natural first steps.

Selected references

• OpenAI, Finite tensor savings and exact Fourier circuits, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Finite-tensor-savings-and-exact-Fourier-circuits-September-25-2026/main.pdf
• J. W. Cooley, J. W. Tukey, An algorithm for the machine calculation of complex Fourier series, Math. Comp., 1965. https://doi.org/10.1090/S0025-5718-1965-0178586-1
• J. Morgenstern, Note on a lower bound on the linear complexity of the fast Fourier transform, J. ACM, 1973. https://doi.org/10.1145/321752.321761
• N. Ailon, A lower bound for Fourier transform computation in a linear model over 2×2 unitary gates, preprint, 2013. https://arxiv.org/abs/1305.4745
• N. Ailon, An $\Omega((n\log n)/R)$ lower bound for Fourier transform computation in the $R$-well conditioned model, preprint, 2014. https://arxiv.org/abs/1403.1307
• J. Alman, K. Rao, Faster Walsh–Hadamard and discrete Fourier transforms from matrix non-rigidity, STOC 2023. https://doi.org/10.1145/3564246.3585188
• I. J. Good, The interaction algorithm and practical Fourier analysis, J. R. Stat. Soc. B, 1958. https://doi.org/10.1111/j.2517-6161.1958.tb00300.x
• J. Alman, B. Li, Kronecker powers, orthogonal vectors, and the asymptotic spectrum, preprint, 2025. https://arxiv.org/abs/2509.14489

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: how many deletion traces does it take to recover a word?

In the trace reconstruction problem an unknown binary word $x\in\{0,1\}^n$ is passed repeatedly through a deletion channel: each bit is deleted independently with known probability $q\in(0,1)$ and the surviving bits are concatenated in order. Each output, called a trace, reveals its length and its bits but not which positions survived. The question is how many independent traces are needed to recover every word $x$ exactly with a fixed success probability. The problem arises in DNA storage and sequencing, in multiple sequence alignment, and as a basic test of how much information a channel with synchronization errors destroys. Its central open question has been whether a polynomial number of traces suffices at a fixed deletion probability.

Timeline

• 2001 — Levenshtein studies efficient reconstruction of sequences from corrupted copies, in combinatorial and memoryless-channel versions (IEEE Trans. Inf. Theory 2001).
• 2004 — Batu, Kannan, Khanna and McGregor introduce the independent-deletion trace problem in connection with multiple sequence alignment and outline a linear lower bound at fixed deletion probability (SODA 2004).
• 2008 — Holenstein, Mitzenmacher, Panigrahy and Wieder give the first worst-case upper bound $\exp(\widetilde O(\sqrt n))$ at constant deletion probability (SODA 2008).
• 2014 — McGregor, Price and Vorotnikova analyze lower bounds via a single displaced one among zeros (ESA 2014).
• 2017 — De, O'Donnell and Servedio (STOC 2017) and, independently, Nazarov and Peres (STOC 2017) improve the upper bound to $\exp(O(n^{1/3}))$.
• 2020 — Holden and Lyons prove the lower bound $\Omega(n^{5/4}/\sqrt{\log n})$ (Ann. Appl. Probab. 2020; erratum 2022).
• 2021 — Chase improves the lower bound to $\Omega(n^{3/2}/\log^7 n)$ (Ann. Inst. Henri Poincaré Probab. Stat. 2021) and the upper bound to $\exp(O(n^{1/5}\log^5 n))$ (STOC 2021).
• 2026 — Burudgunte, Valiant and Wang give a quasipolynomial sample upper bound $\exp(p^{-7/3}(\log_2 n)^{C_0})$ with $p=1-q$ (arXiv:2607.04073).
• 2026 — An OpenAI preprint, Quantitative lower bounds for trace reconstruction (OpenAI Math Release, September 24, 2026), claims that $n^{\Omega(\log\log n)}$ traces are necessary at every fixed $q$, answering the polynomial-sample question negatively. The preprint has not been peer reviewed and its theorems are not formally verified.

Setting

Fix $n$ and $q\in(0,1)$. A deletion mask $a\in\{0,1\}^n$ keeps bit $i$ when $a_i=1$; it has probability $\prod_i (1-q)^{a_i} q^{1-a_i}$. The trace of $x$ under $a$ is the list of the bits $x_i$ with $a_i=1$, in order. Write $\mathcal D_q(x)$ for the law of the trace of $x$ under a random mask.

An estimator with budget $m$ receives $m$ independent traces of $x$ and returns a random word; it may be randomized and its computation is unrestricted. For $s\in(0,1]$, the sample complexity $T_{q,s}(n)$ is the least $m$ such that some estimator recovers every $x\in\{0,1\}^n$ with probability at least $s$; it is $+\infty$ if no finite $m$ works. The one-trace distance is

$$\operatorname{TV}\bigl(\mathcal D_q(x),\mathcal D_q(y)\bigr)=\tfrac12\sum_{w}\bigl|\mathcal D_q(x)(w)-\mathcal D_q(y)(w)\bigr|,$$

the sum running over all finite binary words.

In Lean (namespace OAI.TraceReconstruction), words are Fin n → Bool, traceMass q x w is the probability of output w, an estimator is a function A : (Fin m → Trace) → Word n → ℝ giving a probability vector for each sample, sampleComplexity n q s : ℝ≥0∞ is the infimum of sufficient budgets, and minTraceTV n q is the minimum of traceTV q x y over $x\neq y$.

Formalization targets

Goal: quantitative sample lower bound (Theorem 1.1)

Fix $s\in(0,1]$ and $0<c<1/(4\log 2)$. For every sequence of instances $(n_k,q_k)$ with $n_k\to\infty$, $q_k\in(0,1)$ and $q_k^3\log n_k\to\infty$,

$$T_{q_k,s}(n_k)\;\ge\; n_k^{\,c\log(q_k^3\log n_k)}\qquad\text{for all sufficiently large }k.$$

At fixed $q$ this gives $T_{q,s}(n)\ge n^{\Omega(\log\log n)}$, so no polynomial number of traces suffices. The goal is published on the platform with status Open.

Milestones: superpolynomial indistinguishability (Theorem 1.2)

For every fixed $q\in(0,1)$ and every $A>0$,

$$\lim_{n\to\infty} n^{A}\min_{x\neq y\in\{0,1\}^n}\operatorname{TV}\bigl(\mathcal D_q(x),\mathcal D_q(y)\bigr)=0, \qquad \lim_{n\to\infty}\frac{T_{q,s}(n)}{n^{A}}=\infty\quad (s\in(0,1]).$$

Significance

The result itself. Theorem 1.1 is the first superpolynomial lower bound for exact worst-case trace reconstruction at a fixed deletion probability; previous lower bounds were of order $n^{3/2}$ up to logarithms. It holds against unrestricted computation and any fixed positive success probability, and it settles in the negative the question of whether polynomially many traces suffice. Combined with the 2026 quasipolynomial upper bound of Burudgunte, Valiant and Wang, the sample complexity at fixed $q$ is now known to lie between $\exp(\Theta(\log n\log\log n))$ and $\exp((\log n)^{O(1)})$. Theorem 1.2 isolates the underlying phenomenon: some pairs of distinct words have single-trace laws closer than every inverse polynomial.

Formalizing it. The definitions fix exactly what an estimator may see (only the complete traces, no positions or boundaries) and what "sample complexity" means, including the value $+\infty$. A formal proof would certify a lower bound whose argument is a long multi-scale construction with many quantitative error budgets, the kind of argument where an overlooked loss would invalidate the conclusion.

Difficulty

Earlier lower bounds compare two words that differ by a single local defect and compute their trace distance directly; such pairs are distinguishable from polynomially many traces, so no single-defect construction can give a superpolynomial bound. A superpolynomial bound needs pairs of words whose trace laws agree to every polynomial order, while the argument must remain uniform in the deletion probability (which may tend to $0$ slowly), keep all constants below scale margins that shrink as the number of construction stages grows with $n$, and transfer a bound for one trace to a bound for $m$ independent traces and for arbitrary randomized estimators.

Formalization scope

• Traces are List Bool; traceTV sums over the finite set of all lists of length at most $n$, which contains the support of every trace law, so it agrees with the source's total variation over all finite words.
• sampleComplexity is an sInf in ℝ≥0∞; the infimum of the empty set is $\top$, matching $T_{q,s}(n)=+\infty$. The lower bound is compared after ENNReal.ofReal, and the right-hand side $n^{c\log(q^3\log n)}$ uses the real power.
• Theorem 1.1 is encoded with sequences n q : ℕ → …, Tendsto n atTop atTop, and Tendsto (q k ^ 3 * log (n k)) atTop atTop; the conclusion is ∀ᶠ k in atTop. Logarithms are natural.
• Estimators are arbitrary real-valued probability kernels from samples to words; success is the exact probability of returning the true word, required to be at least $s$ for every input.
• minTraceTV n q is a real sInf, attained for $n\ge1$; at $n=0$ the set is empty and the junk value $0$ does not affect the limit.
• Needed infrastructure: the deletion channel and its trace law, total variation and Hellinger distance for finite laws and their tensorization, and the reduction from sample complexity to pairwise distinguishability. These are reusable for other deletion-channel problems.

Selected references

• V. I. Levenshtein, Efficient reconstruction of sequences, IEEE Trans. Inform. Theory, 2001. https://doi.org/10.1109/18.904499
• T. Batu, S. Kannan, S. Khanna and A. McGregor, Reconstructing strings from random traces, SODA 2004. https://people.cs.umass.edu/~mcgregor/papers/04-soda.pdf
• T. Holenstein, M. Mitzenmacher, R. Panigrahy and U. Wieder, Trace reconstruction with constant deletion probability and related results, SODA 2008. https://www.eecs.harvard.edu/~michaelm/postscripts/soda2008c.pdf
• A. McGregor, E. Price and S. Vorotnikova, Trace reconstruction revisited, ESA 2014. https://doi.org/10.1007/978-3-662-44777-2_57
• A. De, R. O'Donnell and R. A. Servedio, Optimal mean-based algorithms for trace reconstruction, STOC 2017. https://doi.org/10.1145/3055399.3055450
• F. Nazarov and Y. Peres, Trace reconstruction with $\exp(O(n^{1/3}))$ samples, STOC 2017. https://doi.org/10.1145/3055399.3055494
• N. Holden and R. Lyons, Lower bounds for trace reconstruction, Ann. Appl. Probab., 2020. https://doi.org/10.1214/19-AAP1506
• Z. Chase, New lower bounds for trace reconstruction, Ann. Inst. Henri Poincaré Probab. Stat. 57 (2021), 627–643. https://doi.org/10.1214/20-AIHP1089
• Z. Chase, Separating words and trace reconstruction, STOC 2021. https://doi.org/10.1145/3406325.3451118
• A. Burudgunte, P. Valiant and H. Wang, Quasipolynomial trace reconstruction, preprint, 2026. https://arxiv.org/abs/2607.04073
• OpenAI, Quantitative lower bounds for trace reconstruction, OpenAI Math Release preprint, September 24, 2026 (Theorem 1.1, p. 1; Theorem 1.2, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/quantitative-lower-bounds-for-trace-reconstruction-September-24-2026/paper.pdf

Motivation

Sparsest cut asks for a partition of a weighted graph whose crossing capacity is small compared with the demand it separates. It is a basic graph-partitioning primitive (used for divide-and-conquer algorithms, clustering and expansion testing), and its relaxations are the main bridge between approximation algorithms and the geometry of finite metric spaces. In the uniform version every pair of vertices has demand one. The best known polynomial-time approximation, due to Arora, Rao and Vazirani, uses the Goemans–Linial semidefinite relaxation and achieves ratio $O(\sqrt{\log n})$. How good this relaxation can be, i.e. its integrality gap on uniform instances, has been a long-standing question.

Timeline

• 1995. Linial, London and Rabinovich develop the metric approach to cuts: $\ell_1$ metrics are combinations of cut metrics, so embeddings into $\ell_1$ round to cuts (doi:10.1007/BF01200757).
• 1997 and 2002. Goemans and Linial propose the semidefinite relaxation with triangle inequalities and the conjecture that negative-type metrics embed into $\ell_1$ with constant distortion (doi:10.1007/BF02614315).
• 2003 and 2008. Rabinovich relates uniform sparsest cut to average distortion of embeddings into the line and into $L_1$ (doi:10.1145/780542.780609, doi:10.1007/s00454-007-9047-5).
• 2004/2009. Arora, Rao and Vazirani prove the $O(\sqrt{\log n})$ upper bound for uniform demands (doi:10.1145/1502793.1502794).
• 2005/2015. Khot and Vishnoi disprove the Goemans–Linial conjecture for general demands (doi:10.1145/2629614).
• 2006. Devanur, Khot, Saket and Vishnoi give an $\Omega(\log\log n)$ uniform integrality gap (doi:10.1145/1132516.1132594). Lee and Naor propose the Heisenberg-group approach for general demands (doi:10.1109/FOCS.2006.47).
• 2009–2011. Cheeger, Kleiner and Naor prove a $(\log n)^{\Omega(1)}$ general-demand gap (arXiv:0910.2024) and note that their examples cannot give a diverging uniform gap.
• 2013. Kane and Meka improve the uniform gap to $\exp(\Omega(\sqrt{\log\log n}))$ (doi:10.1145/2488608.2488610).
• 2018 and 2025. Naor and Young obtain the sharp general-demand lower bound $\Omega(\sqrt{\log n})$ (doi:10.4007/annals.2018.188.1.4); Chang, Naor and Ren prove the matching upper bound (doi:10.1145/3717823.3718285).

For uniform demands the gap between the lower bound $\exp(\Omega(\sqrt{\log\log n}))$ and the upper bound $O(\sqrt{\log n})$ remained. The source of this mission, an OpenAI preprint dated September 24, 2026, claims a lower bound matching the upper bound up to a power of $\log\log n$.

Setting

Let $C=(c_{ij})$ be symmetric nonnegative capacities on pairs of distinct vertices of $[n]$. The uniform sparsest-cut value is

$$\mathrm{OPT}(C)=\min_{\varnothing\ne B\subsetneq[n]}\frac{\sum_{i\in B,\,j\notin B}c_{ij}}{|B|\,(n-|B|)}.$$

A negative-type semimetric is $d(i,j)=\|x_i-x_j\|^2$ for vectors $x_i$ in a real Hilbert space, satisfying all triangle inequalities $d(i,k)\le d(i,j)+d(j,k)$; distinct points may have distance zero. The Goemans–Linial value is

$$\mathrm{GL}(C)=\min\Bigl\{\sum_{i<j}c_{ij}\,d(i,j)\ :\ \sum_{i<j}d(i,j)=1,\ d\ \text{negative type}\Bigr\}.$$

Normalized cut metrics are feasible, so $\mathrm{GL}(C)\le\mathrm{OPT}(C)$. The integrality gap of $C$ is $\mathrm{OPT}(C)/\mathrm{GL}(C)$.

Formalization targets

Goal: Theorem 1.1

There are an absolute $c>0$ and instances $C^{(j)}$ on $n_j\to\infty$ vertices with $\mathrm{GL}(C^{(j)})>0$ such that, for all large $j$,

$$\frac{\mathrm{OPT}(C^{(j)})}{\mathrm{GL}(C^{(j)})}\ \ge\ c\,\frac{\sqrt{\log n_j}}{(\log\log n_j)^3}.$$

The Lean statement OAI.UniformSparsestCut.mainGap is open on the platform.

Significance

The bound reaches the exponent $1/2$ in $\log n$, so the Arora–Rao–Vazirani analysis of the Goemans–Linial SDP is tight for uniform demands up to the factor $(\log\log n)^3$. It strengthens the Devanur–Khot–Saket–Vishnoi and Kane–Meka refutations of the uniform constant-gap conjecture. Geometrically, it gives a finite negative-type metric for which every $1$-Lipschitz map into $\ell_1$ preserves only a $(\log\log n)^3/\sqrt{\log n}$ fraction of the average distance. The theorem concerns the basic Goemans–Linial SDP only, not strengthened hierarchies.

The result is claimed in an OpenAI preprint; it has not been peer reviewed and no machine-checked proof exists.

Difficulty

The sharp general-demand lower bounds (Heisenberg group, Naor–Young) control worst-pair distortion, and Cheeger–Kleiner–Naor note that those examples have constant average distortion into a line, so they cannot give a diverging uniform gap. A uniform-demand example must force every $\ell_1$ contraction to lose most of the average distance over all pairs, not merely on a few pairs. At the same time the constructed distance must remain of negative type and satisfy all triangle inequalities exactly, and the passage from a probability measure on points to an exactly uniform demand with positive SDP value must be carried out without losing the bound.

Formalization scope

• Capacity n stores cap : Fin n → Fin n → ℝ, nonnegative, symmetric, zero on the diagonal.
• cutRatio C B is the crossing capacity of $B$ divided by $|B|(n-|B|)$; OPT C is the sInf over nonempty proper Finsets $B$.
• NegativeType d requires points x : Fin n → EuclideanSpace ℝ (Fin n) with $d=\|x_i-x_j\|^2$ and all triangle inequalities; Feasible d adds $\sum_{i<j}d(i,j)=1$; glValue C is the sInf of $\sum_{i<j}c_{ij}d(i,j)$ over feasible $d$.
• The goal asks for a sequence $n_j\ge2$, $n_j\to\infty$, with $\mathrm{GL}>0$ for every $j$ (ruling out a gap that is trivial because of division by zero) and the bound eventually.

A complete development needs cut-cone duality, a Hilbert-space kernel construction with rounded charts, Gaussian direction families, and contraction estimates for maps into $\ell_1$. Cut-cone duality and the reduction to exactly uniform demands are reusable. Contributions formalizing Lemma 6.1 (cut-cone duality) or the weak duality $\mathrm{GL}\le\mathrm{OPT}$ are welcome first steps.

Selected references

• OpenAI, Near-square-root logarithmic integrality gaps for uniform sparsest cut, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Near-square-root-logarithmic-integrality-gaps-for-uniform-sparsest-cut-September-24-2026/Near-square-root-logarithmic-integrality-gaps-for-uniform-sparsest-cut-September-24-2026.pdf
• S. Arora, S. Rao, U. Vazirani, Expander flows, geometric embeddings and graph partitioning, J. ACM, 2009. https://doi.org/10.1145/1502793.1502794
• N. R. Devanur, S. A. Khot, R. Saket, N. K. Vishnoi, Integrality gaps for sparsest cut and minimum linear arrangement problems, STOC 2006. https://doi.org/10.1145/1132516.1132594
• D. M. Kane, R. Meka, A PRG for Lipschitz functions of polynomials with applications to sparsest cut, STOC 2013. https://doi.org/10.1145/2488608.2488610
• S. A. Khot, N. K. Vishnoi, The Unique Games Conjecture, integrality gap for cut problems and embeddability of negative type metrics into $\ell_1$, J. ACM, 2015. https://doi.org/10.1145/2629614
• N. Linial, E. London, Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica, 1995. https://doi.org/10.1007/BF01200757
• Y. Rabinovich, On average distortion of embedding metrics into the line, Discrete Comput. Geom., 2008. https://doi.org/10.1007/s00454-007-9047-5
• J. Cheeger, B. Kleiner, A. Naor, A $(\log n)^{\Omega(1)}$ integrality gap for the Sparsest Cut SDP, FOCS 2009. https://arxiv.org/abs/0910.2024
• A. Naor, R. Young, Vertical perimeter versus horizontal perimeter, Ann. of Math., 2018. https://doi.org/10.4007/annals.2018.188.1.4

Motivation

A cell-bounded contingency table is a nonnegative integer matrix with prescribed row sums, column sums and an upper bound on each entry. Bounds of zero forbid entries (structural zeros), and bounds of one give bipartite graphs with prescribed degrees, so the model contains degree-constrained subgraph counting and perfect matchings (the permanent). Counting such tables is central to exact conditional inference in statistics and is equivalent to counting integer flows in bipartite networks. Exact counting is #P-complete even for two-row ordinary tables (Dyer, Kannan and Mount, 1997), so the target is a fully polynomial randomized approximation scheme (FPRAS): a randomized algorithm that, for any $\varepsilon,\delta\in(0,1)$, returns a $(1\pm\varepsilon)$-approximation with probability at least $1-\delta$ in time polynomial in the input length, $1/\varepsilon$ and $\log(1/\delta)$.

Timeline

• 1986. Jerrum, Valiant and Vazirani relate approximate counting and sampling through self-reducibility.
• 1995. Diaconis and Gangolli survey fixed-margin arrays (doi:10.1007/978-1-4612-0801-3_3).
• 1997. Dyer, Kannan and Mount prove #P-completeness for two-row tables and give geometric methods for large margins; Morris improves the margin requirements in 2002 (doi:10.1002/rsa.10049).
• 2000–2003. Dyer and Greenhill (two rows), Cryan and Dyer (fixed number of rows), Dyer (dynamic programming) give approximate counting for a bounded number of rows.
• 2004. Jerrum, Sinclair and Vigoda's permanent algorithm yields an FPRAS for all 0/1 caps (doi:10.1145/1008731.1008738).
• 2009–2010. Barvinok bounds weighted table counts within $N^{O(m+n)}$ (doi:10.1093/imrn/rnn133); Barvinok, Luria, Samorodnitsky and Yong give quasipolynomial randomized approximations for smooth margins (doi:10.1002/rsa.20301).
• 2010. Cryan, Dyer and Randall give an FPRAS for integral flows with large tight capacities and for cell-bounded tables with a fixed number of rows, and list unrestricted approximation as open (doi:10.1137/060650544).
• 2023. Brändén, Leake and Pak give capacity lower bounds via Lorentzian polynomials (doi:10.1007/s11856-022-2364-9); Guo and Jerrum count vertices of certain 0/1 polytopes (doi:10.1007/s00454-022-00406-8).

The source of this mission, an OpenAI preprint dated September 24, 2026, claims an FPRAS with no restriction on dimensions, margins or caps.

Setting

For positive integers $m,n$, margins $r\in\mathbb Z_{\ge0}^m$, $c\in\mathbb Z_{\ge0}^n$ with equal totals, and bounds $b\in\mathbb Z_{\ge0}^{m\times n}$,

$$\Omega(r,c,b)=\Bigl\{X\in\mathbb Z_{\ge0}^{m\times n}:\ \textstyle\sum_jX_{ij}=r_i,\ \sum_iX_{ij}=c_j,\ X_{ij}\le b_{ij}\Bigr\},\qquad Z(r,c,b)=|\Omega(r,c,b)|.$$

All numbers are written in binary, so a capacity can be exponentially larger than its description. $L$ denotes the total binary input length including the rational accuracy parameters $\varepsilon,\delta$. The algorithm uses independent unbiased random bits and is charged for every bit operation.

Formalization targets

Goal: Theorem 1.1 (FPRAS)

One randomized algorithm, given $(r,c,b)$ and rational $\varepsilon,\delta\in(0,1)$, outputs a nonnegative rational $\widehat Z$ with

$$\Pr\bigl[(1-\varepsilon)Z(r,c,b)\le\widehat Z\le(1+\varepsilon)Z(r,c,b)\bigr]\ge1-\delta,$$

outputs exactly $0$ on every execution when $\Omega(r,c,b)=\emptyset$, and performs at most $\mathrm{poly}(L,\varepsilon^{-1},\log\delta^{-1})$ bit operations on every execution. Lean: OAI.ContingencyTables.counting, open on the platform.

Significance

The theorem would answer the question left open by Cryan, Dyer and Randall in 2010: approximate counting of cell-bounded tables (equivalently, integral flows in bipartite networks with arbitrary capacities) without any fixed-dimension, large-capacity, density or balance assumption, with polynomial cost on every execution and no oracle. It contains the 0/1 case handled by Jerrum–Sinclair–Vigoda and the fixed-row results as special cases, and via self-reduction it gives approximate samplers for integer flows. A companion preprint of the same family treats exact uniform sampling of uncapped tables. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

Two regimes clash. Large capacities cannot be expanded into that many binary choices without exponential blow-up, so geometric (polytope volume) methods are needed for them; but those methods require every cell to be large. Small capacities need combinatorial Markov chains, which in turn must preserve exactly one unit of mass per table despite the multiplicities created by encoding a bounded integer by binary choices. Arbitrary mixtures of tiny and huge caps, zero caps and variable dimensions defeat each approach used alone.

Formalization scope

• Algorithms are MatchingFPRAS.RandomMachines: a single finite transition table on an 8-symbol alphabet, one random bit per tick; time is counted in ticks (polynomially equivalent to bit operations).
• Inputs are delimited binary encodings of $m,n,r,c,b$ and of $\varepsilon,\delta$ as reduced fractions (encodeCountingInput); outputs are encoded rationals.
• count r c b is Fintype.card of bounded tables.
• CountingStatement: one machine and constants $C>0$, $d$; with $t=C(|\text{input}|+\lceil1/\varepsilon\rceil+\lceil\log_2\lceil1/\delta\rceil\rceil+1)^d$, every tape of length $t$ halts with a rational $q\ge0$; if count = 0 every tape outputs $0$; and the fraction of tapes with $(1-\varepsilon)Z\le q\le(1+\varepsilon)Z$ is at least $1-\delta$.
• $m,n\ge1$ and equal margin totals are hypotheses, as in the paper.

Needed infrastructure: randomized Turing machines, Markov chain mixing and Poincaré inequalities, log-concavity (Prékopa–Leindler), and network-flow feasibility. The machine model and encodings are shared with the exact-sampling mission of this family. Contributions formalizing Proposition 2.2 (contamination bound), Lemma 3.3 (log-concave tree marginals), Proposition 6.1 (weight evaluation) or Proposition 7.2 are welcome.

Selected references

• OpenAI, An FPRAS for Cell-Bounded Contingency Tables, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/An-FPRAS-for-Cell-Bounded-Contingency-Tables-September-24-2026/main.pdf
• M. Cryan, M. Dyer, D. Randall, Approximately counting integral flows and cell-bounded contingency tables, SIAM J. Comput., 2010. https://doi.org/10.1137/060650544
• M. Jerrum, A. Sinclair, E. Vigoda, A polynomial-time approximation algorithm for the permanent of a matrix with nonnegative entries, J. ACM, 2004. https://doi.org/10.1145/1008731.1008738
• B. Morris, Improved bounds for sampling contingency tables, Random Structures Algorithms, 2002. https://doi.org/10.1002/rsa.10049
• A. Barvinok, Asymptotic estimates for the number of contingency tables, integer flows, and volumes of transportation polytopes, IMRN, 2009. https://doi.org/10.1093/imrn/rnn133
• A. Barvinok, Z. Luria, A. Samorodnitsky, A. Yong, An approximation algorithm for counting contingency tables, Random Structures Algorithms, 2010. https://doi.org/10.1002/rsa.20301
• P. Brändén, J. Leake, I. Pak, Lower bounds for contingency tables via Lorentzian polynomials, Israel J. Math., 2023. https://doi.org/10.1007/s11856-022-2364-9
• H. Guo, M. Jerrum, Counting vertices of integral polytopes defined by facets, Discrete Comput. Geom., 2023. https://doi.org/10.1007/s00454-022-00406-8

Motivation

A contingency table with margins $r=(r_1,\dots,r_m)$ and $c=(c_1,\dots,c_n)$ is a nonnegative integer matrix whose row sums are $r$ and column sums are $c$. Such tables are the basic objects of categorical data analysis: conditional tests of independence (Fisher's exact test and its generalizations) compare an observed table with the uniform distribution on all tables with the same margins, and in practice this requires sampling uniformly from that set. The set is finite but can be exponentially large in the input size when margins are written in binary. Whether one can sample it (approximately or exactly) in time polynomial in both dimensions and in the bit length of the margins has been open since the 1990s.

Timeline

• 1995. Diaconis and Gangolli survey enumeration and random generation of rectangular arrays with fixed margins (doi:10.1007/978-1-4612-0801-3_3).
• 1997–2002. Dyer, Kannan and Mount sample dense tables via the transportation polytope; Morris improves the dense bounds (doi:10.1002/rsa.10049).
• 2000. Dyer and Greenhill give polynomial-time approximate counting and sampling for two-rowed tables.
• 2003. Kijima and Matsui give exact sampling for two rows by coupling from the past; Cryan and Dyer approximately count for a fixed number of rows (doi:10.1016/S0022-0000(03)00014-X); Dyer gives an exact dynamic-programming sampler for fixed row count.
• 2006. Cryan, Dyer, Goldberg, Jerrum and Martin prove rapid mixing of the heat-bath chain for every fixed number of rows (doi:10.1137/S0097539703434243).
• 2016. DeSalvo and Zhao give an exact divide-and-conquer sampler whose polynomial runtime is conditional on a conjecture (arXiv:1507.00070).
• 2021. Arman, Gao and Wormald give linear-time exact generation for sparse margins with $5\Delta^4<N$, and report that no polynomial-time approximately uniform sampler for arbitrary margins was known (arXiv:2104.09413).
• 2024. Göbel, Liu, Manurangsi and Pappik turn sufficiently accurate samplers into perfect samplers (arXiv:2410.00882).

The source of this mission, an OpenAI preprint dated September 24, 2026, claims both an almost-uniform and an exactly uniform sampler for arbitrary margins.

Setting

For nonnegative integer vectors $r\in\mathbb Z_{\ge0}^m$, $c\in\mathbb Z_{\ge0}^n$ with common total $N=\sum_ir_i=\sum_jc_j$, let

$$\Omega(r,c)=\Bigl\{X\in\mathbb Z_{\ge0}^{m\times n}:\ \textstyle\sum_jX_{ij}=r_i,\ \sum_iX_{ij}=c_j\Bigr\}.$$

The input is $(m,n,r,c)$ with margins in binary, so its length is polynomial in $m$, $n$ and $\log(N+1)$. An algorithm uses unbiased random bits. For laws on a finite set, $\mathrm{TV}(\mu,\nu)=\tfrac12\sum_x|\mu(x)-\nu(x)|$.

Formalization targets

Milestone: Theorem 1.1(i) (almost-uniform, bounded time)

For each $k\ge1$, an algorithm halts on every execution in time $\mathrm{poly}(m,n,\log(N+1),k)$ and outputs $X\in\Omega(r,c)$ with

$$\mathrm{TV}\bigl(\mathrm{law}(X),\ \mathrm{Unif}\,\Omega(r,c)\bigr)\le2^{-k}.$$

Goal: Theorem 1.1(ii) (exact uniform sampling)

An algorithm outputs $X\in\Omega(r,c)$ with

$$\Pr[X=Y]=\frac1{|\Omega(r,c)|}\quad(Y\in\Omega(r,c)),$$

terminates almost surely, and has expected running time $\mathrm{poly}(m,n,\log(N+1))$, with polynomials uniform over all margins. Lean: OAI.ContingencyTables.exactSampling, open on the platform.

Significance

The theorem would give the first unconditional polynomial-time exact uniform sampler for contingency tables with arbitrary dimensions and binary margins, with no positivity, sparsity, balance or fixed-dimension restriction, and with all random bits and integer arithmetic counted. It removes the fixed-row restriction of the Dyer–Greenhill and Cryan–Dyer line and the sparsity condition of Arman–Gao–Wormald. The exponents are deliberately large; the contribution is the existence of a polynomial algorithm. Exact time is polynomial in expectation, not on every run. A companion preprint of the same family gives an FPRAS for counting tables with cell bounds. The result is claimed in an OpenAI preprint that has not been peer reviewed; no machine-checked proof exists.

Difficulty

Markov-chain approaches mix rapidly for a fixed number of rows, but the bounds degrade with the row count. Geometric (polytope) methods need all margins to be large, and fail when some margins are tiny while others are huge, which is exactly the mixed regime that arbitrary binary margins allow. Making the sampler exact rather than approximate adds a separate difficulty: the residual-mixture correction requires that the actual output law of the approximate sampler can be computed, with cost polynomial in the accuracy bits.

Formalization scope

• Algorithms are MatchingFPRAS.RandomMachines: a single finite transition table over an 8-symbol tape alphabet; each tick reads one random bit and either moves, writes or halts. Time is counted in ticks, polynomially equivalent to bit operations.
• Inputs are binary encodings with delimiters (encodeNat, encodeMargins); outputs are row-major matrix encodings left on the tape (OutputsTable).
• tableMass A input t X and haltMass A input t are the fractions of the $2^t$ random tapes of length $t$ that halt with output $X$, respectively halt at all, within $t$ ticks.
• ExactSamplingStatement: one machine and constants $C>0$, $d$ such that for all $m,n,r,c$ with equal totals: every halted output is in $\Omega(r,c)$; tableMass → 1/|Ω| for each table; haltMass → 1; and $\sum_t(1-\text{haltMass}_t)$, the expected running time, is at most $C(m+n+\lceil\log_2(N+1)\rceil+1)^d$.
• BoundedSamplingStatement: every tape of length $t=C(m+n+\lceil\log_2(N+1)\rceil+k+1)^d$ halts with a feasible table, and the TV distance to uniform is at most $2^{-k}$.
• Dimensions $m,n$ vary freely (zero allowed); the machine is uniform, not one per size.

Needed infrastructure: randomized Turing machines and their output laws, Markov chain mixing (conductance, Poincaré inequalities), and log-concave sampling. Contributions formalizing Theorem 4.3 (graph Poincaré inequality), Theorem 5.1 (dense completion draw), Proposition 6.3 (law tabulation) or the Göbel–Liu–Manurangsi–Pappik correction are welcome.

Selected references

• OpenAI, Exact Uniform Sampling of Contingency Tables with Arbitrary Margins, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Exact-Uniform-Sampling-of-Contingency-Tables-with-Arbitrary-Margins-September-24-2026/main.pdf
• P. Diaconis, A. Gangolli, Rectangular arrays with fixed margins, Discrete Probability and Algorithms, 1995. https://doi.org/10.1007/978-1-4612-0801-3_3
• B. Morris, Improved bounds for sampling contingency tables, Random Structures Algorithms, 2002. https://doi.org/10.1002/rsa.10049
• M. Cryan, M. Dyer, A polynomial-time algorithm to approximately count contingency tables when the number of rows is constant, J. Comput. System Sci., 2003. https://doi.org/10.1016/S0022-0000(03)00014-X
• M. Cryan, M. Dyer, L. A. Goldberg, M. Jerrum, R. Martin, Rapidly mixing Markov chains for sampling contingency tables with a constant number of rows, SIAM J. Comput., 2006. https://doi.org/10.1137/S0097539703434243
• S. DeSalvo, J. Y. Zhao, Random sampling of contingency tables via probabilistic divide-and-conquer, preprint, 2016. https://arxiv.org/abs/1507.00070
• A. Arman, P. Gao, N. Wormald, Linear-time uniform generation of random sparse contingency tables with specified marginals, preprint, 2021. https://arxiv.org/abs/2104.09413
• A. Göbel, J. Liu, P. Manurangsi, M. Pappik, Perfect sampling from rapidly mixing Markov chains, preprint, 2024. https://arxiv.org/abs/2410.00882