Theoretical Computer Science

Motivation

A random $k$-SAT formula on $n$ Boolean variables is a conjunction of $m$ independent random clauses, each an OR of $k$ literals on distinct variables. As the clause density $m/n$ grows, the formula changes from almost surely satisfiable to almost surely unsatisfiable. Random $k$-SAT is a central model in probabilistic combinatorics, the theory of algorithms and statistical physics: its threshold is where hard instances are expected to concentrate, and it is a proving ground for methods from spin-glass theory. The satisfiability conjecture, formulated explicitly by Chvátal and Reed, asserts that for each fixed $k$ the transition happens at a limiting density $\alpha_k$ that does not drift with $n$.

Timeline

• 1992. Chvátal and Reed settle $k=2$ and formulate the conjecture for every fixed clause size (doi:10.1109/SFCS.1992.267789); Goerdt gives an independent proof for $k=2$ (doi:10.1006/jcss.1996.0081).
• 1999. Friedgut, with an appendix by Bourgain, proves a sharp transition around a sequence of densities, leaving open whether the sequence converges (doi:10.1090/S0894-0347-99-00305-7).
• 2002, 2006. Mézard, Parisi and Zecchina, and Mertens, Mézard and Zecchina, predict threshold values via the cavity method (doi:10.1126/science.1073287, doi:10.1002/rsa.20090).
• 2004. Achlioptas and Peres prove bounds $2^k\log2-O(k)$ (doi:10.1090/S0894-0347-04-00464-3).
• 2013, 2014. Bayati, Gamarnik and Tetali develop combinatorial interpolation for sparse random structures (doi:10.1214/12-AOP816); Abbe and Montanari study concentration of solution counts (doi:10.1002/rsa.20501).
• 2016. Coja-Oghlan and Panagiotou locate the threshold sequence within $o_k(1)$ of $2^k\log2-(1+\log2)/2$ (doi:10.1016/j.aim.2015.11.007).
• 2022. Ding, Sly and Sun prove the conjecture for all sufficiently large $k$, with the 1RSB value (doi:10.4007/annals.2022.196.1.1).
• 2026. Carenini proves a polynomial scaling window and resolves the conjecture for every fixed $k\ge3$ (ECCC TR26-229, made public October 5, 2026; https://eccc.weizmann.ac.il/report/2026/229/). Priority for the resolution belongs to Carenini.

The source of this mission is an OpenAI preprint dated September 25, 2026, which gives an alternative proof of the existence of the limiting threshold.

Setting

Fix $k\ge3$. For $n\ge k$, a proper $k$-clause chooses $k$ distinct variables among $x_1,\dots,x_n$ uniformly and gives each an independent fair sign, so each of the $2^k\binom nk$ clauses is equally likely. Let $C_1,C_2,\dots$ be independent such clauses (sampled with replacement: two positions may hold the same clause) and

The ratio $c=m/n$ is the clause density.

Formalization targets

Goal: Theorem 1.1

For every fixed integer $k\ge3$ there is $\alpha_k\in(0,\infty)$ such that

No assertion is made at $c=\alpha_k$, and the value of $\alpha_k$ is not identified. Lean: OAI.FixedClauseThreshold.main, open on the platform.

Significance

The theorem settles, for every fixed $k\ge3$, the existence half of the threshold question: Friedgut's sharp transition happens at a location that converges. Previously this was known only for large $k$ (Ding–Sly–Sun) and for $k=2$. Existence is a prerequisite for questions about the value of $\alpha_k$, its computability, and the fluctuations of the satisfiability hitting time, which companion OpenAI preprints address. The proof here proceeds through concentration of a capped last satisfiable index and a comparison between system sizes; it does not rely on Carenini's window.

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

Difficulty

A sharp-threshold theorem gives a narrow window at each $n$ but no control of how the window's center moves with $n$. Convergence needs a comparison between different system sizes, and interpolation methods from spin-glass theory deliver free-energy bounds, not hard satisfiability statements, and often only for even arity. The center must also be shown to concentrate polynomially, which requires bounding how many variables are forced along the clause process.

Formalization scope

• ProperClause n k is a function Fin n → Option Bool with exactly $k$ defined entries; some b at $i$ is the literal satisfied when $\sigma_i=b$.
• Formula n k m := Fin m → ProperClause n k (ordered, with replacement); properSATProbability n k m is the exact ratio of satisfiable formulas to all formulas, which equals $P_n(m)$ under the uniform product law.
• Degenerate sizes: $m=0$ gives probability $1$; for $n<k$ and $m>0$ the ensemble is empty and the ratio is $0$ by convention, affecting only finitely many $n$.
• HasLimitingThreshold k asserts $\exists\,\alpha>0$ with limits $1$ for $0\le c<\alpha$ and $0$ for $c>\alpha$ at $m=\lfloor cn\rfloor$.

Infrastructure: finite counting of formulas, Efron–Stein-type variance bounds, a deterministic concentration-to-convergence lemma (Theorem 5.1), and the Poisson/interpolation comparison with the transfer back to proper clauses. Formalizations of Proposition 2.2 (integrated forcing), Proposition 3.3 (polynomial concentration) and Theorem 5.1 are welcome.

Selected references

• OpenAI, A Limiting Satisfiability Threshold for Every Fixed Clause Size, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Limiting-Satisfiability-Threshold-for-Every-Fixed-Clause-Size-September-25-2026/article.pdf
• G. Carenini, A polynomial scaling window for random k-SAT and a proof of the satisfiability conjecture, ECCC TR26-229, 2026. https://eccc.weizmann.ac.il/report/2026/229/
• V. Chvátal, B. Reed, Mick gets some (the odds are on his side), FOCS 1992. https://doi.org/10.1109/SFCS.1992.267789
• E. Friedgut (appendix by J. Bourgain), Sharp thresholds of graph properties, and the k-SAT problem, J. Amer. Math. Soc., 1999. https://doi.org/10.1090/S0894-0347-99-00305-7
• D. Achlioptas, Y. Peres, The threshold for random k-SAT is $2^k\log2-O(k)$, J. Amer. Math. Soc., 2004. https://doi.org/10.1090/S0894-0347-04-00464-3
• A. Coja-Oghlan, K. Panagiotou, The asymptotic k-SAT threshold, Adv. Math., 2016. https://doi.org/10.1016/j.aim.2015.11.007
• J. Ding, A. Sly, N. Sun, Proof of the satisfiability conjecture for large k, Ann. of Math., 2022. https://doi.org/10.4007/annals.2022.196.1.1
• M. Bayati, D. Gamarnik, P. Tetali, Combinatorial approach to the interpolation method and scaling limits in sparse random graphs, Ann. Probab., 2013. https://doi.org/10.1214/12-AOP816
• E. Abbe, A. Montanari, On the concentration of the number of solutions of random satisfiability formulas, Random Structures Algorithms, 2014. https://doi.org/10.1002/rsa.20501

Motivation

In a Maker–Breaker achievement game, two players alternately claim cells of a board; Maker wins by owning every cell of some copy of a fixed shape, and Breaker only tries to prevent this. Polyomino achievement games on the infinite square grid, introduced by Frank Harary, ask which small polyominoes are winners (Maker can force a copy) and which are losers (Breaker can prevent it forever). The six-cell shape Snaky is the long-standing hard case: Maker was known to win with a one-stone handicap or in higher dimensions, but the ordinary planar game without handicap remained undecided.

Timeline

• 2004. Sieben shows that Snaky is a winner in 41 dimensions and records earlier handicap-two strategies of Harary, Harborth and Seemann, as well as the non-existence of a pairing strategy for Breaker (Integers 4, 2004).
• 2007. Halupczok and Schlage-Puchta prove that Snaky wins in three dimensions, loses on an $8\times8$ board, and has planar handicap number at most one (Integers 7, 2007). Ito and Miyagawa give another handicap-one construction.
• 2008. Sieben develops proof trees for weak achievement games and gives a finite proof sequence for the handicap-one win, describing the ordinary planar problem as undecided (Integers 8, 2008).
• 2011. Csernenszky, Martin and Pluhár give a computer-free proof that Breaker has no pairing defense for Snaky (Integers 11, 2011).
• 2023, 2025. Shaik, Mayer-Eichberger, van de Pol and Saffidine study QBF encodings of finite Maker–Breaker games, including Snaky on a $5\times5$ board (arXiv:2301.07345); Boucher and Villemaire treat strong achievement games (doi:10.21428/594757db.6ae0c84a).

The source of this mission, an OpenAI preprint dated September 25, 2026, settles the ordinary planar game: Snaky is a winner, within 21 Maker moves.

Setting

The board is $\mathbb Z^2$, initially empty. Snaky is

An allowed copy is $t+R(S)$ with $t\in\mathbb Z^2$ and $R$ one of the eight $2\times2$ signed permutation matrices (rotations by quarter turns and reflections; no scaling). Maker moves first; then Breaker and Maker alternate, each claiming one previously unclaimed cell. Maker wins when it owns all cells of an allowed copy.

A Maker policy is a rule that, given the current position, returns an unclaimed cell. In the fixed-endpoint formulation, the policy keeps claiming fresh cells even after a win, and one asks that after Maker's $N$-th claim its set of cells contain an allowed copy whenever Breaker's first $N-1$ replies were legal.

Formalization targets

Milestone: Proposition 10 (finite identities of the 35-move certificate)

A pure computation on a printed certificate of 616 cards: card counts, 1,837 placement terms, required-set/envelope/height data of four interface cards, and uniform bounds for all cards.

Milestone: Theorem 11

Goal: Theorem 1

The Lean statement OAI.SnakyPrototype.snaky_winning_strategy_21_with_legal_states is open on the platform.

Significance

Theorem 1 decides the ordinary planar Snaky game, recorded as undecided by Sieben (2008), and gives an explicit bound of 21 Maker moves (a win by the 41st individual turn). It also gives a win on the finite $17\times17$ board (Corollary 6), and removes the handicap from the earlier handicap-one strategies. The paper does not claim the bound 21 is optimal or address the strong game in which both players seek a copy.

The result is proved in an OpenAI preprint that has not been peer reviewed. Its correctness rests on a soundness lemma for a composition rule together with large finite certificates checked by standalone programs. A machine-checked proof would replace this combination of informal soundness argument and external computation by a single certified statement.

Difficulty

The board is infinite and Breaker may play anywhere, so no finite game-tree search applies directly: a proof must cover all Breaker replies, including those far from the action. Pairing strategies, the usual tool for proving shapes are losers, are known to fail for Snaky, but that does not give Maker a strategy. The certificate approach needs a composition rule whose soundness accounts for arbitrary previous ownership on both sides; the move count must be the number of actual Maker claims, including any replacement moves.

Formalization scope

• Cells are ℤ × ℤ; snaky is the six-cell set above and HasSnaky M asks for r : Fin 8, t : Cell with snaky.image (placement r t) ⊆ M, where orient lists all eight signed permutations.
• A Policy is a function of a move counter, the Maker set and the Breaker set; it must never return an owned cell. playState σ N β ∅ ∅ k is the position after $k$ Maker claims and $k$ Breaker replies.
• LegalRepliesBeforeFinal σ N β ∅ ∅ constrains only the first $N-1$ Breaker replies; the theorems conclude a copy of $S$, exactly $N$ Maker cells, and disjointness of the two players' sets throughout.
• The certificate milestone stores the cards as an Array Entry and computes rowAt i (required set, envelope, height) by the composition recursion; it is a decidable statement about explicit finite data.

A trivializing reading is ruled out: the policy is required to be legal on all inputs, and Breaker's replies are arbitrary legal cells of the infinite board. A complete development needs a soundness proof for the composition rule (Lemma 3) and verified evaluation of the certificates; the policy, game and certificate infrastructure is shared between the 21- and 35-move statements. Contributions formalizing Lemma 3, Proposition 5 (the 21-move certificate identities) and Corollary 6 are welcome.

Selected references

• OpenAI, Snaky in 21 Maker moves, preprint, September 25, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Snaky-in-21-Maker-moves-September-25-2026/article.pdf
• N. Sieben, Snaky is a 41-dimensional winner, Integers 4, 2004. https://math.colgate.edu/~integers/eg5/eg5.pdf
• I. Halupczok, J.-C. Schlage-Puchta, Achieving Snaky, Integers 7, 2007. https://math.colgate.edu/~integers/hg2/hg2.pdf
• N. Sieben, Proof trees for weak achievement games, Integers 8, 2008. https://math.colgate.edu/~integers/ig7/ig7.pdf
• H. Ito, H. Miyagawa, Snaky is a winner with one handicap, 8th Hellenic European Conference on Computer Mathematics and its Applications, 2007.
• A. Csernenszky, R. R. Martin, A. Pluhár, On the complexity of Chooser–Picker positional games, Integers 11, 2011. https://math.colgate.edu/~integers/lg2/lg2.pdf
• I. Shaik, V. Mayer-Eichberger, J. van de Pol, A. Saffidine, Implicit state and goals in QBF encodings for positional games, preprint, 2023. https://arxiv.org/abs/2301.07345
• S. Boucher, R. Villemaire, The QBF Cover encoding for Harary's Tic-Tac-Toe, Canadian Conference on AI, 2025. https://doi.org/10.21428/594757db.6ae0c84a

Motivation

A single exact linear equation $y = \langle x, s\rangle$ about an unknown unit vector $s \in \mathbb{R}^d$ carries arbitrarily fine information: $d$ independent Gaussian equations determine $s$ almost surely, provided all of them can be kept. A learner that reads the equations once, in order, and keeps only a bounded number of bits between them faces a different problem. The question asked here is how many noiseless measurements such a learner needs in order to reach a prescribed angular precision $\epsilon$, as a function of its memory.

This is a question about memory–sample trade-offs: how much a bound on persistent memory forces a learning procedure to read more data. With unbounded real registers, the randomized Kaczmarz update $z_t = z_{t-1} + \frac{y_t - \langle x_t, z_{t-1}\rangle}{\|x_t\|^2} x_t$ satisfies $\mathbb{E}\|z_t - s\|^2 = (1 - 1/d)^t$ on isotropic Gaussian rows, so order $d\log(1/\epsilon)$ samples suffice. That update stores real numbers and gives no finite-bit upper bound; the question is whether a learner with roughly $d^2$ bits can do better than this scale.

Background

• 1937. Kaczmarz introduces the projection method for linear systems; Strohmer and Vershynin (2009) give the randomized version with exponential convergence.
• 2014. Shamir's finite-message framework for online and distributed learning includes bounded-memory online processing as a special case.
• 2015. Steinhardt and Duchi prove memory-dependent minimax rates for sparse linear regression with noise.
• 2016. Steinhardt, Valiant and Wager relate memory, communication and statistical queries and pose a quadratic-memory versus exponential-sample conjecture for parity learning; Raz proves a time–space lower bound for parity learning, and in 2017 extends the method to a large class of learning problems.
• 2019. Sharan, Sidford and Valiant prove that for Gaussian regression with tiny uniform additive noise, a learner with at most $d^2/4$ bits needs $\Omega(d\log r)$ samples to reach Euclidean accuracy $d^{-r}$, in a stated range of $r$, and ask (Section 1.1) whether the first-order sample dependence on precision is optimal under bounded memory. In the same year Dagan, Kur and Shamir prove quadratic-space lower bounds for two different linear-prediction tasks in the streaming model.
• 2026. The OpenAI preprint Memory and precision in noiseless Gaussian regression (dated September 27, 2026) states an $\Omega_A(d\log(1/\epsilon))$ lower bound for exact observations and memory $Ad^2$. It has not been peer reviewed, and the Lean statement of its main theorem is open on this platform.

Setting

Fix integers $d \ge 2$, $M \ge 0$, $T \ge 0$. A signal $s$ lies on the unit sphere $S^{d-1} \subset \mathbb{R}^d$. At step $t \in \{1,\dots,T\}$ the learner receives the pair $(x_t, y_t)$ with $x_t \sim N(0, I_d)$ independent and $y_t = \langle x_t, s\rangle$ exactly (no noise).

A finite-state learner with $M$ bits keeps a state in a set of at most $2^M$ elements. A data-independent shared seed $\omega$ (drawn from a probability space $(\Omega,\rho)$) may select its rules. Given the seed, the current state, the step index and the current pair, a transition chooses the next state and whether to stop; it may perform unrestricted computation but retains only the next state. The learner must stop by the deterministic horizon $T$. Its output $\hat s \in S^{d-1}$ is a function of the terminal state, the stopping index and the seed only; a discarded observation cannot be read again. Success at precision $\epsilon$ means angular error $\arccos\langle \hat s, s\rangle \le \epsilon$.

Write $\sigma_d$ for the uniform probability measure on $S^{d-1}$. Uniform success is the probability of success when $S \sim \sigma_d$ is drawn independently of the rows and the seed.

In Lean (OAI.NoiselessRegression), the state space is Fin (2 ^ M), a learner is a structure Learner d M T Ω with fields initialChoice, transition, output, the sample law is the product of stdGaussian on EuclideanSpace ℝ (Fin d), and uniformSuccess and success are the probabilities defined above. Randomness during the run is represented through the arbitrary seed space $\Omega$.

Formalization targets

Goal: OAI.NoiselessRegression.main

The goal is the conjunction of two statements.

Fixed quadratic memory (Theorem 1.2): for every $A > 0$ there are $c_A > 0$ and $d_A$ such that, for $d \ge d_A$, $M \le A d^2$, $0 < \epsilon \le 1/10$, and every admissible learner,

Subquadratic memory (Corollaries 1.3 and 1.4): there is an absolute $c > 0$ such that for every memory sequence $M(d) = o(d^2)$ there is $d_0$ with the same conclusion $T \ge c\, d\log(1/\epsilon)$ for $d \ge d_0$, under either uniform success at least $2/3$ or success at least $2/3$ for every fixed signal $s$.

No relation between $\epsilon$ and $M$ is assumed; the constant is absolute in the subquadratic case.

Milestone: supporting estimates (OAI.MemoryPrecision.main)

A single bundled statement collecting the paper's projection-density and backward-block estimates (Theorem 3.1, Propositions A.1, A.4, A.5, B.6, B.7, Corollary 8.2), the cube-prior precision bound (Proposition 8.3), and the explicit success bound after a bounded number of samples (Proposition 5.3):

Significance

The result. Theorem 1.2 answers, for exact observations and isotropic Gaussian rows, the precision question raised in Section 1.1 of Sharan–Sidford–Valiant: with $O(d^2)$ bits, the $d\log(1/\epsilon)$ scale achieved by real-valued Kaczmarz cannot be improved, uniformly over all $0<\epsilon\le 1/10$. Because an exact-observation learner can simulate added noise, the preprint derives from it an $\Omega_A(d r \log d)$ lower bound in the noisy experiment of Sharan–Sidford–Valiant at accuracy $d^{-r}$, which strengthens their $\Omega(d\log r)$ bound in that range.

Formalizing it. The result is proved only in an unrefereed preprint; no machine-checked proof exists. A formal proof would certify a lower bound whose model (randomized measurable rules, early stopping, shared seeds, measurability conventions) is delicate, and the conventions are already fixed in the Lean definitions. Remaining work: the full formal proof, and as a variant the every-signal version of Theorem 1.2 for fixed $A$ (Corollary 1.4), which the Lean goal states only in the subquadratic case.

Difficulty

Conditioning the uniform prior on one exact observation confines the signal to a hyperplane section of the sphere, a law singular with respect to the original spherical measure; information-theoretic arguments that track a posterior density therefore break down after a single step. Arguments for noisy observations, such as Sharan–Sidford–Valiant's, rely on the noise to keep posteriors spread out and do not transfer to the more informative exact experiment. The bound must also hold uniformly in $\epsilon$ with no relation between $\epsilon$ and $M$, so a learner with $\Theta(d^2)$ bits must be prevented from storing $\log(1/\epsilon)$ bits per coordinate for very small $\epsilon$.

Formalization scope

• Vectors live in EuclideanSpace ℝ (Fin d); signals and outputs in Metric.sphere 0 1. The uniform sphere law is the normalized toSphere measure; rows are i.i.d. stdGaussian.
• States are Fin (2 ^ M); the first component of each action is the stop flag. Runs that never stop are forced to terminate at index $T$.
• Learner.Admissible requires a.e.-measurability of the initial choice, transitions (against Gaussian × Lebesgue on pairs), outputs, and of the full experiment under each fixed signal and under the uniform prior.
• Probabilities are ℝ≥0∞-valued; the threshold is $2/3$; angular error is Real.arccos ⟪ŝ, s⟫; $\log$ is natural.
• The seed space $\Omega$ is an arbitrary probability space in universe u, so randomized learners are covered by placing their randomness in the seed.

The goal cannot be satisfied trivially: the hypotheses range over all admissible learners, and the success threshold $2/3$ is achievable (with large $T$), so the implication has content.

A complete development needs Gaussian measures on Euclidean space, spherical measure and cap estimates, Gram determinants and affine distances, $L^q$ densities of Gaussian projections, and measurable selection of Borel versions of kernels. The projection-density estimates are reusable beyond this mission. Contributions toward the bundled milestone, or toward any of its component estimates, are welcome.

Selected references

• OpenAI, Memory and precision in noiseless Gaussian regression, OpenAI Math Release preprint, September 27, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Memory-and-precision-in-noiseless-Gaussian-regression-September-27-2026/paper.pdf
• V. Sharan, A. Sidford, G. Valiant, Memory-Sample Tradeoffs for Linear Regression with Small Error, STOC 2019. https://doi.org/10.1145/3313276.3316403 (full version https://arxiv.org/abs/1904.08544)
• R. Raz, Fast Learning Requires Good Memory: A Time-Space Lower Bound for Parity Learning, 2016. https://arxiv.org/abs/1602.05161
• R. Raz, A Time-Space Lower Bound for a Large Class of Learning Problems, FOCS 2017. https://doi.org/10.1109/FOCS.2017.73
• J. Steinhardt, G. Valiant, S. Wager, Memory, Communication, and Statistical Queries, COLT 2016. https://proceedings.mlr.press/v49/steinhardt16.html
• J. Steinhardt, J. Duchi, Minimax Rates for Memory-Bounded Sparse Linear Regression, COLT 2015. https://proceedings.mlr.press/v40/Steinhardt15.html
• O. Shamir, Fundamental Limits of Online and Distributed Algorithms for Statistical Learning and Estimation, NeurIPS 2014. https://proceedings.neurips.cc/paper_files/paper/2014/hash/cc427d934a7f6c0663e5923f49eba531-Abstract.html
• Y. Dagan, G. Kur, O. Shamir, Space Lower Bounds for Linear Prediction in the Streaming Model, COLT 2019. https://proceedings.mlr.press/v99/dagan19b.html
• T. Strohmer, R. Vershynin, A Randomized Kaczmarz Algorithm with Exponential Convergence, J. Fourier Anal. Appl. 15 (2009). https://doi.org/10.1007/s00041-008-9030-4

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

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

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: 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

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

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

This mission asks for a formal proof that the matrix multiplication exponent is at most $2.25=9/4$ over every field. It is proposed for the Matrix multiplication exponent campaign, using the campaign's existing tensor-rank definition. The target is deliberately non-strict: equality with $9/4$ is allowed.

The starting point is OpenAI's October 2026 matrix-multiplication material, whose original arithmetic-exponent theorem is stated over the complex numbers. An all-fields adaptation has been checked separately in Lean. This mission asks for the corresponding result in the campaign's precise mathematical model; that connection still requires proof.

Setting

Let $K$ be any field, finite or infinite and in any characteristic. For a positive integer $n$, the square matrix multiplication tensor is the sum of $e_{ij}\otimes e_{jk}\otimes e_{ki}$ over all indices $i,j,k<n$. Each factor is the vector space of functions from pairs of indices to $K$. Its tensor rank is the least number of pure tensors in an exact decomposition over $K$.

The imported definition MME.matMulExp takes the infimum of the ratios $\log R_K(MM_n)/\log n$ for integer $n\ge2$, together with the value $3$ at sizes zero and one. The goal refers to this existing definition without modifying it. An upper bound on the infimum need not be attained at any one matrix size.

Target

For every field $K$, prove

The Lean theorem is mme_omega_le_225, with the sole typeclass hypothesis [Field K]. The decimal is interpreted exactly as a real rational, not as a floating-point approximation. There is no restriction to characteristic zero, infinite fields, algebraically closed fields, or the complex numbers.

The campaign template currently uses a strict inequality. This proposal intentionally requests the non-strict bound $\le2.25$ and should be reviewed on that basis. It does not assert $\omega<2.25$. The proposed numeric campaign value is $2.25$.

Significance

A proof of this goal would place the nine-fourths bound in the same formal tensor-rank model used by other entries in this campaign. Reusing the foundation makes its assumptions and numeric value directly inspectable. Establishing the comparison between the arithmetic and tensor formulations would also produce reusable results for future matrix multiplication missions.

The all-fields quantifier matters: constructions that use interpolation or roots of unity must justify their applicability and any descent back to the original field. A result over the complex numbers alone does not establish this goal.

Difficulty

The available checked adaptation proves the nine-fourths bound for the OAI arithmetic exponent and its exact-rank exponent. A remaining task is to connect that exact-rank representation to the campaign's tensor product and rank definition. This requires checking the coordinate conventions, converting rank decompositions, and transporting the bound through the infimum and logarithms.

The proof must also compile in the campaign's pinned Lean environment. Success in a different Lean or Mathlib version is useful evidence for the source proof, but it does not verify this mission's theorem.

Formalization scope

This draft imports the campaign's published mme_omega definition and contains one open goal. It preserves the campaign environment, Mathlib 777aaa6 with Lean 4.29.0-rc3. The separate all-fields OAI adaptation was checked using Lean 4.33.1 and Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; its proof is not yet an accepted Prove2me solution to this goal.

In particular, the bridge to MME.matMulExp and the environment port remain unproved here. The mission should remain open until Prove2me accepts a proof of this exact statement. An independent auditor read the Lean goal and imported definition without seeing the intended wording; that read-back is included verbatim in the goal's natural-language statement for review.

Selected references

• OpenAI matrix multiplication preprint, October 2, 2026.
• OpenAI ComparatorChallenges Lean source.
• Matrix multiplication exponent campaign.

The all-fields adaptation and the proposed connection to the campaign definition are additional formalization work; they are not attributed to the original complex-field statement.

Motivation

All-pairs shortest paths (APSP) asks for the exact distance between every ordered pair of vertices in an $n$-vertex weighted directed graph. Floyd–Warshall solves it in $O(n^3)$ time, and for decades no algorithm beat $n^{3-\delta}$ for any constant $\delta>0$ on graphs with polynomially bounded integer weights. In 2026, Alman and Vassilevska Williams (arXiv:2610.06783) gave a deterministic $O(n^{2.99942})$ algorithm, the campaign's first entry. Later entries tightened the accounting to $2.9983$ and $2.99791$.

This entry records the deterministic exponent $2.996001$. It roughly doubles the saving below $3$ compared with $2.99791$, and it matches what was previously only known with randomized hashing.

Setting

The model is the campaign's fixed deterministic word RAM (foundation mission: Truly Subcubic APSP on a Word RAM). A finite program uses add, subtract and multiply modulo $2^W$, indirect load and store, a sign branch, and accept or reject, on words of width $W \ge b(\log_2 n + 1)$. Inputs have integer weights of absolute value at most $n^\kappa$ for a fixed $\kappa$, and there are no negative cycles. The machine has no source of randomness; the algorithm behind this entry is deterministic.

Formalization target

The goal is the campaign template with the value $2.996001$:

which says there is a deterministic word-RAM program that solves APSP in $O(n^{2.996001})$ steps.

How the bound arises

The algebraic core is the thin-product data structure of Alman and Vassilevska Williams: for an $N\times D$ by $D\times N$ integer product it answers requested entries $W$ in $\tilde O(N^2D^{-\Gamma} + N D^{a} + |W| D^{q})$. Two local refinements of that construction sharpen the exponents:

1. Pruned encodings. Encoding branches with more than $m$ copies of the distinguished symbol $P_0$ are never materialized, giving $a(c) = \bigl(\tfrac12 cH(1/c) + (c-1)\ln 3\bigr)/\ln 4$.
2. Exact binomial tail. The box preprocessing is bounded by its actual binomial sum, giving $\Gamma(c,\theta) = \bigl(cH(1/c) - cH((1-\theta)/c) - \theta\ln 9\bigr)/\ln 4$, with $q(\theta) = \bigl(H(\theta)+\theta\ln 9\bigr)/\ln 4$.

The main new step is a deterministic filtering reduction. Moduli are chosen one small prime factor at a time, using exact thin-product witness counts to certify positive answers and to eliminate whole blocks of unresolved queries. Repeated filtering removes the need to scan individual modular witnesses, which was the bottleneck of earlier deterministic reductions (the prime-by-prime idea is suggested in footnote 9 of the source paper, after Fischer, Kaliciak and Polak). With middle blocks of size $n^{\varepsilon/2}$ this yields all-edges Exact Triangle in $n^{3-\delta+o(1)}$, where

and deterministic bit scaling transfers the bound to min-plus product and APSP with polylogarithmic overhead.

The exact rational parameters $c = 21.2733$, $\theta = 0.111731$ and $\varepsilon = 0.056846$ satisfy the thin regime $\varepsilon(a+\Gamma) < 1$ with margin $1.16\times10^{-6}$, and give $\delta > 0.00399928$. Hence APSP runs in $n^{2.99600072+o(1)}$, and the gap $2.996001 - 2.99600072 > 0$ absorbs the subpolynomial factor.

Significance

This is the first deterministic entry near $2.996$. Earlier analyses reached about $2.99601$ only by repeating random-prime hashing, which this word-RAM model cannot express. The deterministic filtering closes that gap.

Selected references

• J. Alman and V. Vassilevska Williams, Truly Subquadratic 3SUM and Truly Subcubic APSP via Triangles in Sparse Lopsided Graphs (2026). https://arxiv.org/abs/2610.06783
• Deterministic APSP in $O(n^{2.996001})$: an explicit refinement of the thin-product method, technical note, 6 October 2026. This is the source of $2.996001$ and has not been peer reviewed.