Theoretical Computer Science

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,

$$\Pr_{S\sim\sigma_d}\big\{\arccos\langle \hat s, S\rangle \le \epsilon\big\} \ge \tfrac23 \;\Longrightarrow\; T \ge c_A\, d \log(1/\epsilon).$$

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

$$\Pr\{\arccos\langle \hat s, S\rangle \le \epsilon\} \le \min\Big\{1, \Big[2\epsilon\, e^{C(1+M/d^2)\lceil T/q\rceil}\Big]^{(d-1)/2}\Big\},\qquad q = \lfloor (d-1)/8 \rfloor.$$

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

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

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

$$\operatorname{MME.matMulExp}(K)\le 2.25=\frac94.$$

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

$$\texttt{TrulySubcubicAPSP.APSP.SolvedInTime}\ 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

$$\delta = \min\{\varepsilon\Gamma,\ 1-\varepsilon a,\ \varepsilon(1/2-q)\},$$

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.

Motivation

Prediction with expert advice asks how a learner should combine the forecasts of a pool of prediction algorithms when nothing is assumed about the data: the instances and labels may be chosen by an adversary, and the learner's performance is compared with that of the pool. Littlestone and Warmuth's The Weighted Majority Algorithm (Inform. and Comput. 108, 1994) introduced the multiplicative-weights master algorithm WM for binary pool predictions and proved that its number of mistakes is at most logarithmic in the pool size plus a constant times the mistakes of the best pool member. The same multiplicative update now underlies boosting, online convex optimization and approximate solvers for linear programs and zero-sum games (Arora, Hazan, Kale 2012).

In many applications the pool members do not output a bit but a degree of confidence in $[0,1]$, while the master must still commit to a binary decision. Section 5 of the paper treats exactly this setting with the algorithm WMG, and shows that WM's mistake bound survives unchanged.

Setting

A nonempty pool of $n$ prediction algorithms is run on a finite sequence of trials. In trial $k$ the pool member $i$ predicts $x_{k,i}\in[0,1]$, the master predicts $\lambda_k\in\{0,1\}$, and then the binary label $\rho_k\in\{0,1\}$ is revealed. The master keeps a non-negative weight $w_{k,i}$ per pool member, with positive initial weights. Write

$$s_k=\sum_{i=1}^n w_{k,i},\qquad \gamma_k=\frac{\sum_{i=1}^n w_{k,i}\,x_{k,i}}{s_k},$$

and $w_{\mathrm{init}}=s_0$, $w_{\mathrm{fin}}$ the total weight after the last trial.

WMG with parameter $0\le\beta<1$ predicts $\lambda_k=1$ if $\gamma_k>1/2$ and $\lambda_k=0$ if $\gamma_k<1/2$; at $\gamma_k=1/2$ either prediction is allowed. A mistake is a trial with $\lambda_k\ne\rho_k$, and $m$ is the number of mistakes. An update step multiplies every weight by a factor

$$w_{k+1,i}=F\,w_{k,i},\qquad \beta^{|x_{k,i}-\rho_k|}\le F\le 1-(1-\beta)\,|x_{k,i}-\rho_k| \tag{5.1}$$

with $0^0=1$. WMG executes an update step in every trial, or only in mistake trials; more generally (footnote 8 of the paper) in every mistake trial and possibly in others. Outside update steps the weights do not change. When the $x_{k,i}$ are binary, WMG coincides with WM.

Formalization targets

Goal: Theorem 5.1 (pp. 234–235)

For every run of WMG with $0\le\beta<1$, whatever the tie-breaking, the update criterion and the factors in (5.1), if $w_{\mathrm{fin}}>0$ then

$$m\le\frac{\ln(w_{\mathrm{init}}/w_{\mathrm{fin}})}{\ln\bigl(2/(1+\beta)\bigr)}.$$

The bound involves only the total weights, not the losses of individual pool members; Corollary 5.1 of the paper, which compares $m$ with the total absolute loss $m_i$ of each pool member, follows from it and from the lower bound in (5.1).

Milestones

1. Appendix, p. 256. In a mistake trial the total weight drops by at least a factor $(1+\beta)/2$: $s_{k+1}\le\frac{1+\beta}{2}s_k$.
2. §5, p. 235. Unless $\beta=0$ and $|\gamma_k-\rho_k|=1$ in some update trial,

$$\sum_{k\ \text{update}}\ln\bigl(1-(1-\beta)|\gamma_k-\rho_k|\bigr)\le\sum_{k\ \text{mistake}}\ln\bigl(1-(1-\beta)|\gamma_k-\rho_k|\bigr)\le m\ln\bigl(\tfrac12+\tfrac12\beta\bigr).$$

The paper gives two proofs of Theorem 5.1, one through each milestone; the second also uses Lemma 5.2, the potential lemma shared with the continuous master WMC, which is posed in the companion mission on WMC.

Significance

Theorem 5.1 says that the master's mistake count is controlled by how much total weight the pool loses, with the same constant $1/\ln(2/(1+\beta))$ as for binary pools. With equal initial weights it gives Corollary 5.1: WMG makes at most $(\log n+m_i\log(1/\beta))/\log(2/(1+\beta))$ mistakes for every pool member $i$, so pool members may report graded confidences at no cost in the master's guarantee. The same weight-potential argument is the template for the randomized master WMR of §6 and for later analyses of exponential weights.

The result is classical and proved in the paper. What this mission adds is a machine-checked statement and proof against the paper's own model: a relation that covers both update criteria, all tie-breaks at $\gamma=1/2$ and the whole interval of admissible factors, rather than a single deterministic instance. No formalization of WMG or of Theorem 5.1 is known; the platform's existing weighted-majority results (Hazan's textbook version) concern binary experts, unit initial weights and a fixed update factor.

Difficulty

The obvious argument, copied from WM, tracks the weight $q_0$ of members predicting $0$ and the weight $q_1$ of members predicting $1$. With predictions in $[0,1]$ a member supports both outcomes, and the update factor is only constrained to an interval, so the two-bucket bookkeeping must be redone for fractional contributions. The factor's upper bound $1-(1-\beta)r$ is affine in $r=|x-\rho|$, while the natural exponential factor $\beta^r$ is convex; the argument must use the right one of the two bounds of (5.1). A further subtlety is the case $\beta=0$: a factor may be $0$, the total weight can vanish, and both the logarithmic bound and the weighted average $\gamma$ degenerate.

Formalization scope

• The pool is Fin n with $n>0$, and the trials are Fin T, all trials of the sequence; weights are w : ℕ → Fin n → ℝ, with w 0 the initial and w T the final weights.
• Pool predictions are real numbers in $[0,1]$, labels and master predictions are real numbers in $\{0,1\}$.
• The update criterion is a Boolean flag per trial that must be set in every mistake trial; the factor is an arbitrary real number in the interval (5.1) for each trial and member, where $\beta^{r}$ is Real.rpow (so $0^0=1$).
• The paper writes a ratio of logarithms with the base omitted; Real.log is used.
• The case $w_{\mathrm{fin}}=0$, where the paper's bound is $+\infty$, is excluded by the hypothesis $0<w_{\mathrm{fin}}$. Without it, Lean's Real.log 0 = 0 would turn the paper's vacuous bound into the false claim $m\le0$; with it, no Lean junk value enters the statement.
• The goal must be stated for the relation, not for a single run: fixing the tie-break, updating in every trial only, or fixing $F$ to one endpoint of (5.1) would state a special case. Stating the theorem only for binary pool predictions would state Theorem 2.1 instead.

A complete development needs only finite sums, real logarithms and real powers from Mathlib. Proofs of either milestone, of the existence of a run for every input (using Lemma 5.1, $\beta^r\le1+r(\beta-1)$), and of Corollary 5.1 on top of the goal are welcome.

Selected references

• N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. https://doi.org/10.1006/inco.1994.1009
• N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Proc. 30th IEEE FOCS, 256–261, 1989. https://doi.org/10.1109/SFCS.1989.63487
• V. Vovk, Aggregating Strategies, Proc. 3rd COLT, 371–383, 1990. https://dl.acm.org/doi/10.5555/92571.92672
• S. Arora, E. Hazan, S. Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications, Theory of Computing 8, 121–164, 2012. https://doi.org/10.4086/toc.2012.v008a006

Motivation

Many security-relevant inputs are noisy and do not repeat exactly: fingerprint minutiae, iris codes, lists of personal preferences, the set of features extracted from a document. A cryptographic key derived from such an input must be reproducible from a later, slightly different reading, without storing the input itself. Dodis, Ostrovsky, Reyzin and Smith (SIAM J. Comput. 38(1), 2008; arXiv:cs/0602007) introduced secure sketches for this purpose: public helper data that lets the holder of a nearby reading recover the original exactly, while revealing as little as possible about it.

When the input is a set of features, the natural distance is the size of the symmetric difference. Juels and Sudan proposed the fuzzy vault for this setting (Des. Codes Cryptogr. 38, 2006). Section 6.2 of Dodis et al. gives a simpler, deterministic variant, the improved Juels–Sudan sketch (Construction 5), whose storage and entropy loss are both $t\log n$ for $s$-element subsets of an $n$-element universe, independent of $s$. The paper's Theorem 6.1 is the analysis of that construction. This mission formalizes it.

Setting

Laws and average min-entropy. A random variable is identified with its law. For a pair $(A,B)$,

$$\tilde H_\infty(A\mid B) = -\log_2 \sum_b \max_a \Pr[A=a \wedge B=b],$$

which equals $-\log_2 \mathbb E_{b\leftarrow B}\big[\max_a\Pr[A=a\mid B=b]\big]$, the average min-entropy of §2.4: the negative logarithm of the best probability of guessing $A$ after seeing $B$.

Secure sketches. Let $\mathcal M$ be a set with an integer-valued distance $\mathrm{dis}$. A pair of procedures $(\mathsf{SS},\mathsf{Rec})$ is an average-case $(\mathcal M,m,\tilde m,t)$-secure sketch (Definitions 3 and 4) if

1. (correctness) $\mathrm{dis}(w,w')\le t$ implies $\mathsf{Rec}(w',\mathsf{SS}(w))=w$;
2. (security) for all random variables $W$ over $\mathcal M$ and $I$ with $\tilde H_\infty(W\mid I)\ge m$, one has $\tilde H_\infty(W\mid (\mathsf{SS}(W),I))\ge\tilde m$.

The difference $m-\tilde m$ is the entropy loss.

The metric. For a finite universe $\mathcal U$ with $n=|\mathcal U|$, $\mathrm{SDif}_s(\mathcal U)$ is the set of $s$-element subsets of $\mathcal U$ with $\mathrm{dis}(w,w')=|w\triangle w'|$.

Construction 5. Identify $\mathcal U$ with a finite field $\mathcal F$ of $n$ elements and let $t\le s$.

• $\mathsf{SS}(w)$: form $p'(z)=\prod_{x\in w}(z-x)$, monic of degree $s$, and output its coefficients $a_{s-1},\dots,a_{s-t}$ of degree $s-1$ down to $s-t$.
• $\mathsf{Rec}(w',(a_{s-1},\dots,a_{s-t}))$: form $p_{\mathrm{high}}(z)=z^s+\sum_{i=s-t}^{s-1}a_iz^i$; find a polynomial $p_{\mathrm{low}}$ of degree at most $s-t-1$ that agrees with $p_{\mathrm{high}}$ on at least $s-t/2$ points of $w'$ (Reed–Solomon decoding); output the roots of $p_{\mathrm{high}}-p_{\mathrm{low}}$.

The Lean development names these charPoly, sketchCoeffs, sketch, pHigh, Step3Cond and recover, and the metric SDifS with distance sdifDist, in the namespace FuzzyExtractors.ImprovedJS.

Formalization targets

Goal: Theorem 6.1

For every finite field $\mathcal F$ with $n$ elements, all $t\le s$ and every real $m$,

$$(\mathsf{SS},\mathsf{Rec})\ \text{is an average-case}\ \big(\mathrm{SDif}_s(\mathcal F),\,m,\,m-t\log_2 n,\,t\big)\text{-secure sketch}.$$

The goal is uniform in $m$: the entropy loss $t\log n$ does not depend on the input distribution.

Milestones (the correctness half)

The paper's argument on p. 21 splits into four steps, each a milestone:

1. $p'=p_{\mathrm{high}}+q$ with $\deg q\le s-t-1$, and $p_{\mathrm{high}}=-q$ on $w$;
2. $|w\triangle w'|\le t$ implies $|w\cap w'|\ge s-t/2$, so $-q$ is a valid $p_{\mathrm{low}}$;
3. any two valid $p_{\mathrm{low}}$ coincide;
4. $\mathsf{Rec}(w',\mathsf{SS}(w))=w$ whenever $|w\triangle w'|\le t$.

A fifth, off the goal's path, records Step 2's remark that the sketch consists of the first $t$ elementary symmetric polynomials of $w$, up to sign.

The security half is the entropy bound: since $\mathsf{SS}$ takes at most $n^t$ values, $\tilde H_\infty(W\mid(\mathsf{SS}(W),I))\ge\tilde H_\infty(W\mid I)-t\log n$ (the paper cites its Lemma 3.1, which is posed in the first mission of this series and is not restated here).

Significance

The result. Theorem 6.1 gives a secure sketch for set difference whose sketch length and entropy loss are $t\log n$, which the paper shows is essentially optimal when $n\gg s$ (§6.2, via Lemma C.1 and a constant-weight code bound). It improves the original fuzzy vault, whose entropy loss the paper analyses in Appendix D and finds good only when the stored data is very large. Through the paper's generic composition with randomness extractors (Lemma 4.1), it yields fuzzy extractors for set-valued inputs in large universes, the regime of biometric feature sets.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists on Prove2Me or, to our knowledge, elsewhere. A formal proof combines three pieces of reusable infrastructure: a probabilistic layer (average min-entropy of laws on arbitrary types, and the chain-rule-type bound for a function with few values), the combinatorics of symmetric differences of equal-size sets, and the algebra of Reed–Solomon unique decoding (a low-degree polynomial is determined by its values on enough points). Each of these is useful beyond this mission.

Difficulty

No step is deep; the difficulty is in the bookkeeping. The correctness argument relies on exact degree accounting: $p_{\mathrm{high}}$ must agree with $p'$ in every coefficient of degree at least $s-t$, so that the remainder has degree at most $s-t-1$, and the uniqueness count ("two candidates agree on at least $s-t$ points") requires the threshold to be at least $s-t/2$; the paper's sentence says "more than", which does not support the argument as written. The roots of $p_{\mathrm{high}}-p_{\mathrm{low}}$ must be shown to form exactly the set $w$, with no multiplicities lost. The security half needs the average min-entropy of a joint law with a deterministic, $n^t$-valued component bounded uniformly over all auxiliary variables, including those with infinite or uncountable range, where sums are infinite sums of extended nonnegative reals.

Formalization scope

Conventions committed to in Lean:

• Laws are PMFs; the procedures are kernels M → PMF S, here deterministic (PMF.pure). Average min-entropy is the joint form above, logarithms base 2, and the auxiliary $I$ ranges over an arbitrary ι : Type (a superset of the paper's $\{0,1\}^*$), never restricted to finite types.
• The universe is the field $\mathcal F$ itself, [Field 𝔽] [Fintype 𝔽], with $n$ = Fintype.card 𝔽; the paper's "$n$ is a prime power" is then automatic.
• The paper leaves $t\le s$ implicit; every statement assumes it. No parity condition on $t$ is imposed: "at least $s-t/2$" is written $2\cdot\#\ge 2s-t$ in $\mathbb N$, which covers odd $t$.
• "Degree at most $s-t-1$" is degree < s - t, so $p_{\mathrm{low}}=0$ when $t=s$.
• The sketch is a vector in $\mathcal F^t$ indexed from $0$: entry $i$ is the coefficient of degree $s-1-i$. The storage bound $t\log n$ holds by this type and is not restated.
• $\mathsf{Rec}$ takes an arbitrary valid $p_{\mathrm{low}}$ (by choice) instead of running a decoding algorithm. The paper's "fail" output is encoded as returning $w'$, which only occurs when correctness makes no claim.
• Running time is out of scope. Theorem 6.1's clause that $\mathsf{SS}$ and $\mathsf{Rec}$ run in time polynomial in $s$, $t$ and $\log n$ is dropped, and no surrogate predicate replaces it.

A formalization that checks only correctness, drops or trivializes the entropy clause, or lets $\mathsf{Rec}$ see $w$ itself, would not be Theorem 6.1. The goal states both clauses through the definition of an average-case secure sketch, with $\mathsf{Rec}$ given only $w'$ and the sketch.

Contributions welcome: proofs of the milestones, a general lemma bounding average min-entropy loss by the logarithm of the number of sketch values (the paper's Lemma 2.2(b) and Lemma 3.1), and Reed–Solomon uniqueness lemmas stated for reuse.

Selected references

• Y. Dodis, R. Ostrovsky, L. Reyzin, A. Smith, Fuzzy Extractors: How to Generate Strong Keys from Biometrics and Other Noisy Data, SIAM J. Comput. 38(1):97–139, 2008. https://doi.org/10.1137/060651380 ; arXiv:cs/0602007v4, https://arxiv.org/abs/cs/0602007
• A. Juels, M. Sudan, A Fuzzy Vault Scheme, Designs, Codes and Cryptography 38(2):237–257, 2006. https://doi.org/10.1007/s10623-005-6343-z
• E. Agrell, A. Vardy, K. Zeger, Upper Bounds for Constant-Weight Codes, IEEE Trans. Inform. Theory 46(7):2373–2395, 2000. https://doi.org/10.1109/18.887851

Improve deterministic integer 3SUM to $O(n^{1.999112})$ time in the foundation mission’s word-RAM model.

The existing Corollary 26 routine admits the tighter bound $O(wD^{0.436}+n^2/D^{0.064})$. Keep $D=\lfloor n^{1/18}\rfloor$ and change the grouping parameter to $g=\lceil D^{0.032}\rceil$, implemented using the integer root of $D^4$ of order $125$. Balancing the instance costs and scans gives an Exact Triangle saving of $2/1125$, and the verified 3SUM reduction gives $n^{2249/1125+o(1)}$ time.

The supporting theorem establishes every rational exponent $r>2249/1125=1.999111\ldots$, including $1.999112$. This changes the algorithm’s grouping parameter and improves the earlier cutoff $1.999125$. All other model definitions and the shared reduction lemmas are reused.

Prove deterministic $O(n^{1.99913})$ time for 3SUM on polynomially bounded integers, using the same word-RAM model and definitions as the foundation mission.

The existing uniform Exact Triangle bound has saving $\delta=0.00175$. The verified 3SUM reduction yields $n^{2-\delta/2+o(1)}=n^{1.999125+o(1)}$ time, so every fixed rational exponent above $1.999125$ is attainable, including $1.99913$. This mission sharpens the bound extracted from the existing algorithm.

The supporting theorem covers all rational $r>1.999125$; it does not assert an exact $O(n^{1.999125})$ bound. The proof reuses the shared, proved APSP and 3SUM lemmas from Anthropic’s formalization.

Motivation

In online prediction, a learner makes a forecast before seeing the next label. A collection of other forecasters may offer useful advice, but the learner need not know beforehand which forecaster will perform well. Littlestone and Warmuth's Weighted Majority Algorithm (WM) gives a deterministic way to combine such advice. Its guarantees hold for every finite sequence of instances and labels, including sequences chosen without any probability model. That worst-case setting is useful when the reliability of the forecasters can change or when no data-generating distribution has been justified. The paper develops WM and several variants; this mission isolates its basic mistake bound. Littlestone and Warmuth, 1994.

Setting

A finite pool has $n$ members, each of which predicts either $0$ or $1$ on every trial. The true label on trial $t$ is $\rho_t\in\{0,1\}$, and member $i$ predicts $x_{t,i}\in\{0,1\}$. The master prediction is $\lambda_t\in\{0,1\}$. Pool members may themselves be learning algorithms, so their predictions may reflect all earlier labels. The mission treats their prediction vectors and the labels as arbitrary finite sequences; no independence or stationarity is assumed.

Each member begins with a strictly positive real weight $w_{0,i}$. Before trial $t$, let $w_{t,i}$ be its current weight. For $b\in\{0,1\}$, let $q_{t,b}$ be the sum of weights of members predicting $b$. WM predicts the value with the larger backing total. When the two totals tie, either binary prediction is allowed. After the label is revealed, WM changes weights only if its own prediction was wrong. On such a trial, each member that predicted the wrong label has its weight multiplied by a fixed factor $\beta$ with $0\le\beta<1$; every other member retains its weight. If WM predicted correctly, every weight stays as it was. This is the version of the algorithm stated in §1 of the paper. A footnote there says the bounds also apply to the variant that updates on every trial. Littlestone and Warmuth, 1994, p. 215.

Write $W_t=\sum_i w_{t,i}$ for the total pool weight at a trial boundary. Thus $W_0=w_{\mathrm{init}}$ and $W_T=w_{\mathrm{fin}}$ after $T$ trials. Let $m$ count the trials with $\lambda_t\ne\rho_t$. The default initial weights in the paper are all one, but its Theorem 2.1 permits arbitrary positive initial weights. Littlestone and Warmuth, 1994, pp. 220–221.

Formalization targets

The two milestones state the weight facts used immediately before and within Theorem 2.1. First, on each trial where WM errs,

$$W_{t+1}\le \frac{1+\beta}{2}W_t.$$

Across the whole sequence, with $m$ master mistakes, the corresponding estimate is

$$W_T\le W_0\left(\frac{1+\beta}{2}\right)^m.$$

The goal is the paper's Theorem 2.1, retaining its explicit constant:

$$m\le \frac{\log(W_0/W_T)} {\log\!\left(2/(1+\beta)\right)} \qquad\text{when }W_T>0.$$

The logarithm base is immaterial because the same base occurs above and below the fraction. The paper explicitly uses this convention for ratios of logarithms. The positive-final-weight condition represents the paper's statement that the displayed logarithmic bound is vacuous when all weight has vanished, which can happen for $\beta=0$. The whole-sequence weight estimate remains meaningful in that case. Littlestone and Warmuth, 1994, pp. 220–221.

Significance

The result limits the mistakes of a master predictor without assigning probabilities to the predictions or labels. It relates a visible property of the run, the reduction of total weight, to the number of master errors. Later bounds in the paper use this starting point to compare WM with an individual pool member and to analyze related algorithms; this mission fixes the initial, exact-constant result on which those comparisons rest. The $\beta=0$ case includes the paper's Halving Algorithm interpretation when initial weights are equal. Littlestone and Warmuth, 1994, pp. 215, 221–222.

The mathematical theorem is proved in the 1994 paper. The remaining task here is to represent its algorithm and finite-sequence bound in Lean and supply machine-checked proofs. A complete development would give later formalizations a reusable finite-pool voting and weight-update model, along with a checked potential estimate. The local draft statements compile; their proofs remain open. A separate, sorry-free local check constructs a run for every finite prediction and label sequence with a nonempty pool and valid weights and parameter, so the quantified run relation has witnesses.

Difficulty

The master can be wrong even when some pool members are right, and members may change their predictions over time. Counting one member's errors therefore does not directly control the master's error count. The exact contraction constant also depends on which side of a weighted vote the master chose, including the permitted tie case. When $\beta=0$, a single mistake can erase all weight backing the wrong label, so the logarithmic expression must be interpreted with care if no positive weight remains. These are features of the stated algorithm, rather than assumptions about how the sequence was generated.

Formalization scope

The formalization indexes pool members by Fin n and trials by Fin T. Booleans represent binary predictions and labels; weights and $\beta$ are real. A WM run is a relation on the full sequence of weights and master predictions, admitting every choice at a tied vote. Its update rule changes weights only after a master mistake, scales exactly the members that disagreed with the label, and leaves all other weights unchanged. Theorems require $0\le\beta<1$ and strictly positive initial member weights. The goal additionally requires $W_T>0$, while the two weight inequalities permit $W_T=0$. Natural logarithms instantiate the paper's common-base logarithm convention. Finite sums and a finite mistake count match the paper's finite-sequence convention.

The statement ranges over arbitrary pool predictions and labels, so it cannot be satisfied merely by selecting an easy input sequence. The run relation allows both legal outcomes of a tie; selecting one favorable tie rule would weaken the target. The sorry-free run-existence check also rules out a vacuous theorem caused by an inconsistent update relation. The paper's update-on-every-trial variant, its member-specific corollaries, and its later algorithms are outside this mission's goal.

A completed formalization needs finite sums of real weights, cardinalities of finite sets of mistake trials, a finite induction over trial boundaries, and real logarithm inequalities. The run definition and the first two bounds can be reused in the later parts of this paper's formalization. Contributions that prove the exact stated milestones or supply supporting facts about legal runs and nonnegative weights are within scope.

Selected references

• Nick Littlestone and Manfred K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. DOI: 10.1006/inco.1994.1009.

Motivation

A job shop is the basic model of a factory floor in which every job follows its own route through the machines. Minimizing the time at which the last job is finished (the finish time, or makespan) is one of the central problems of deterministic scheduling theory, and the question of which special cases admit efficient algorithms has organized much of the field since the 1950s.

For two machines the picture is sharp. Jackson (1956) showed that a two-machine job shop in which every job has at most two operations is solved by a simple rule extending Johnson's flow-shop algorithm (Jackson, Naval Research Logistics Quarterly 3, 1956; Conway, Maxwell and Miller, Theory of Scheduling, 1967, p. 105). Once a single job may have three operations, the non-preemptive problem becomes NP-complete: Lenstra, Rinnooy Kan and Brucker showed this for $n-1$ jobs with one nonzero task each and one job with three (Annals of Discrete Mathematics 1, 1977; a 1975 Mathematisch Centrum report is the paper's reference [1]). Gonzalez and Sahni (Operations Research 26(1), 1978) extended this boundary to preemptive schedules, in which a task may be interrupted and resumed later: even then the two-machine problem is NP-complete, already when only two jobs have three nonzero tasks. This mission formalizes that reduction, Lemma 5 together with Corollary 2 of their paper.

Timeline:

• 1956: Jackson, two-machine job shop with at most two operations per job, solved in $O(n\log n)$.
• 1975/1977: Lenstra, Rinnooy Kan and Brucker, the non-preemptive two-machine job shop NP-complete with $n-1$ one-task jobs and one three-task job.
• 1976: Garey, Johnson and Sethi, the non-preemptive two-machine job shop NP-complete even when problem size is measured by the sum of the task lengths (Mathematics of Operations Research 1, 1976).
• 1978: Gonzalez and Sahni, the preemptive two-machine job shop NP-complete (Lemmas 5 and 6), and the non-preemptive case again by the same reduction (Corollary 2).

Setting

A job shop has processors $P_1, \dots, P_m$ and jobs $1, \dots, n$. Job $i$ is a finite sequence of tasks; task $j$ of job $i$ must be processed on a given processor $k$ for $t_{k,i,j} \ge 0$ time units, and for every job, task $j \ge 2$ can begin only after task $j-1$ has been completed. Schedules start at time $0$. A preemptive schedule assigns to every task a finite set of time intervals $[s, f)$ on its processor, of total length $t_{k,i,j}$, such that intervals on the same processor do not overlap and every interval of task $j$ begins after task $j-1$ of the same job is completed. A non-preemptive schedule processes each task in a single interval. If $f_i(S)$ is the time at which job $i$ is completed, the finish time is $\mathrm{FT}(S) = \max_i f_i(S)$.

PARTITION: a multiset $\{a_1, \dots, a_n\}$ of nonnegative integers has a partition if some index set $u$ satisfies $\sum_{i \in u} a_i = \tfrac12 \sum_{i=1}^n a_i$.

From $a_1, \dots, a_n$, with $T = \sum_i a_i$, the paper builds the two-processor job shop $\mathrm{JS}$ with $n+2$ jobs:

• job $i \le n$: tasks $(P_2, a_i)$, $(P_1, a_i)$;
• job $n+1$: tasks $(P_1, T/2)$, $(P_2, T/2)$, $(P_1, 3T)$;
• job $n+2$: tasks $(P_2, 3T)$, $(P_1, T/2)$, $(P_2, T/2)$.

Each processor carries load exactly $5T$. In Lean, the instance is JS a : JobShopLTAS.Core.Instance 2 (n + 2), a schedule is S : Schedule (JS a) (a finite set of pieces), and the predicates are S.IsPreemptive, S.IsNonPreemptive and S.FinishedBy (5 * T a).

Formalization targets

Goal: Lemma 5 and Corollary 2

For every $n$ and every $a : \mathrm{Fin}\,n \to \mathbb N$,

$$\bigl(\exists\, S \text{ preemptive},\ \mathrm{FT}(S) \le 5T\bigr) \iff \mathrm{Partition}(a) \quad\text{and}\quad \bigl(\exists\, S \text{ non-preemptive},\ \mathrm{FT}(S) \le 5T\bigr) \iff \mathrm{Partition}(a).$$

Milestones

1. Lemma 5(a): a partition yields a non-preemptive schedule of finish time exactly $5T$ (the paper's Figure 3).
2. Observations (i)–(ii) in the proof of Lemma 5(b): in any preemptive schedule with $\mathrm{FT} \le 5T$, task $t_{2,n+1,2}$ is completed by $2T$ and $t_{2,n+2,1}$ by $4T$; no part of $t_{1,n+1,3}$ runs before $T$ and no part of $t_{1,n+2,2}$ before $3T$.
3. Lemma 5(b): without a partition, every preemptive schedule has $\mathrm{FT} > 5T$.
4. Lemma 5: the preemptive equivalence.
5. Corollary 2: the non-preemptive equivalence.

Significance

The result places the boundary of tractability for two-machine job shops exactly: at most two operations per job is solvable in $O(n\log n)$, while two jobs with three operations make the problem NP-complete, and allowing preemption does not help. The same instance serves both schedule types, because its optimum is $5T$ in either model exactly when a partition exists.

The theorem is classical and fully proved on paper; no machine-checked proof is known to exist. Formalizing it requires a precise model of preemptive schedules, which the paper treats informally, and makes explicit an argument (the "no idle time" step of Lemma 5(b)) that the paper compresses into a few sentences. The schedule model built here is shared with the other job-shop missions of this series.

Difficulty

Direction (a) is a concrete schedule and is bookkeeping. Direction (b) is the substance. The tempting argument "each processor has load $5T$, so a schedule of finish time $5T$ has no idle time, hence some set of short jobs fills exactly $[0, T/2]$ on $P_2$" is incomplete for preemptive schedules: the short jobs may be split into many pieces spread over the whole horizon, and $U$, the set of short jobs that touch $P_1$ during $[0, T]$, is defined by pieces rather than by whole tasks. Making the counting argument rigorous requires measuring idle time on each processor across arbitrary finite unions of intervals and tying the amount of processing done on $P_1$ before $T$ to the completed first tasks on $P_2$.

Formalization scope

• Processing times are real numbers; the PARTITION data are natural numbers cast to $\mathbb R$; $T$ is the real sum. Processors are Fin 2 with $P_1 = 0$, $P_2 = 1$; jobs and tasks are 0-based, so the paper's job $n+1$ is job n and job $n+2$ is job n + 1.
• Job-shop data reuse the published JobShopLTAS.Core.Instance. Schedules are finite sets of pieces (task, start, end) with positive length, following the paper's footnote 1 (p. 40). A task of length zero has no pieces and is completed when its predecessor is; it never blocks a processor.
• A non-preemptive schedule is a preemptive one with at most one piece per task. "Finish time $\le \tau$" is ∀ j, S.jobFinish j ≤ τ; "finish time $> 5T$" is the existence of a job finishing after $5T$; "finish time $5T$" in Lemma 5(a) is $\le 5T$ together with a job finishing at exactly $5T$.
• Complexity wording not formalized. "Partition $\alpha$ preemptive JOFT" and "Partition $\alpha$ nonpreemptive JOFT" (polynomial reducibility), "NP-complete", and Lemma 6 ("JOFT is in NP") are not stated. What is stated is the equivalence that the paper's proofs establish for the instance they construct, with the explicit constant $\tau = 5T$.
• The PARTITION condition is written $2\sum_{i\in u} a_i = \sum_i a_i$ in $\mathbb N$, avoiding truncated division.
• A trivializing formalization is ruled out: the schedule notion requires every task to receive its full processing time, so the empty schedule is feasible only when $T = 0$ (and then the empty index set is a partition), and the finish-time bound is over every job, so no statement holds by an unattained supremum or a default value.
• Welcome contributions: a proof of Lemma 5(a) by an explicit piece schedule; infrastructure for measuring busy and idle time of a processor in a finite piece schedule, reusable for Lemma 7 (mission 4) and the preemptive flow-shop missions; the proof of Lemma 5(b).

Selected references

• T. Gonzalez, S. Sahni, Flowshop and Jobshop Schedules: Complexity and Approximation, Operations Research 26(1), 36–52, 1978. https://doi.org/10.1287/opre.26.1.36
• J. K. Lenstra, A. H. G. Rinnooy Kan, P. Brucker, Complexity of Machine Scheduling Problems, Annals of Discrete Mathematics 1, 343–362, 1977. https://doi.org/10.1016/S0167-5060(08)70743-X
• M. R. Garey, D. S. Johnson, R. Sethi, Complexity of Flow Shop and Job Shop Scheduling, Mathematics of Operations Research 1(2), 117–129, 1976. https://doi.org/10.1287/moor.1.2.117
• J. R. Jackson, An Extension of Johnson's Results on Job Lot Scheduling, Naval Research Logistics Quarterly 3(3), 201–203, 1956. https://doi.org/10.1002/nav.3800030307
• R. W. Conway, W. L. Maxwell, L. W. Miller, Theory of Scheduling, Addison-Wesley, 1967.

Motivation

A multicommodity flow problem asks to route many source–sink demands through one capacitated network at the same time. Its min-cut (sparsest cut) is the smallest ratio, over all cuts, of the capacity crossing the cut to the demand separated by it. Routing is always limited by every cut, so the max-flow never exceeds the min-cut. For a single commodity the two are equal (Ford–Fulkerson); for many commodities they are not, and the size of the gap governs a large family of approximation algorithms for graph partitioning, layout and routing problems.

Leighton and Rao (J. ACM 46 (1999), extended abstract FOCS 1988) proved that for uniform problems, where every pair of nodes demands one unit, the gap is at most $O(\log n)$ (their Theorem 2). This mission formalizes the other half: Section 2.1 of the paper, A bad example, which shows that the $\log n$ is necessary. On a 3-regular expander graph the max-flow is a $\Theta(\log n)$ factor smaller than the min-cut, so Theorem 2 cannot be improved beyond the constant.

Timeline. Ford and Fulkerson (1956) and Elias–Feinstein–Shannon (1956): single-commodity max-flow equals min-cut. Hu (1963): equality for two commodities. Leighton and Rao (1988, journal 1999): uniform and product problems have an $O(\log n)$ gap, and expanders show it is tight. Klein, Agrawal, Ravi and Rao (1990) and later Linial–London–Rabinovich (Combinatorica 1995) and Aumann–Rabani (1998): an $O(\log k)$ gap for general demands with $k$ commodities, tight by the same expander example.

Setting

Let $V$ be a finite set of $n$ nodes. A network assigns a capacity $C(u,v)\ge0$ to every pair, symmetric and zero on the diagonal. For $U\subseteq V$ with complement $\bar U$, the cut capacity $C(U,\bar U)$ is the total capacity of the pairs with one end in $U$ and the other in $\bar U$.

In the uniform multicommodity flow problem (UMFP) every pair of distinct nodes is a commodity with unit demand. Its max-flow $f$ is the largest fraction such that $f$ units of every commodity can be routed simultaneously without exceeding any capacity (concurrent flow). Its min-cut is

$$\mathcal S=\min_{\emptyset\ne U\subsetneq V}\frac{C(U,\bar U)}{|U|\,|\bar U|}.$$

Section 2.1 takes a 3-regular $n$-node graph $G$ with unit edge capacities, so that $C(U,\bar U)=|\langle U,\bar U\rangle|$ is the number of edges between $U$ and $\bar U$, and assumes that $G$ is a $c$-edge-expander:

$$|\langle U,\bar U\rangle|\ \ge\ c\,\min\{|U|,|\bar U|\}\qquad\text{for all }U\subseteq V,$$

for a constant $c>0$. Families of such graphs exist for a sufficiently small $c$ (Margulis 1973; a random 3-regular graph has the property with high probability). Throughout, $\log$ is $\log_2$.

Formalization targets

Goal: the gap on an expander

For a 3-regular $c$-edge-expander with unit capacities and $n\ge 8$,

$$f\ \le\ \frac{6\,\mathcal S}{c\,\bigl(\lfloor\log n\rfloor-2\bigr)} .$$

This is the final display of §2.1 (pp. 794–795), with the floor that the argument actually supports (see Formalization scope). It leaves the expander family unspecified: it holds for every graph with the two properties.

Milestones, in the order the argument uses them

1. $\mathcal S\ge c/(n-1)$ for the expander (p. 794).
2. In a 3-regular graph, at most $n/2$ nodes lie within distance $\lfloor\log n\rfloor-3$ of any node.
3. Hence at least half of the source–sink pairs are at distance at least $\lfloor\log n\rfloor-2$.
4. A uniform flow of fraction $f$ uses capacity at least $\tfrac12\binom n2 f(\lfloor\log n\rfloor-2)$, and the total capacity is $3n/2$.
5. Hence $f\le 3n/\bigl(\binom n2(\lfloor\log n\rfloor-2)\bigr)=6/\bigl((n-1)(\lfloor\log n\rfloor-2)\bigr)$.

Companions: Theorem 1

Theorem 1 (p. 795) states that for any $n$ there is an $n$-node UMFP with $f\le O(\mathcal S/\log n)$. It is stated twice: conditionally on a family of 3-regular $c$-expanders (the form §2.1 proves), and unconditionally, with one constant $K$ for all $n\ge2$.

Significance

The result shows that the $O(\log n)$ max-flow min-cut gap of Leighton and Rao's Theorem 2 is tight up to the constant, and, through the same example, that the $O(\log k)$ bound for general demands is tight. Every approximation algorithm that rounds a multicommodity flow, or its dual, to a cut loses a $\Theta(\log n)$ factor in the worst case for this reason; improving on it, as Arora, Rao and Vazirani did (J. ACM 2009) with an $O(\sqrt{\log n})$ approximation for sparsest cut, requires a stronger relaxation than the flow LP.

The result is classical and proved. To our knowledge it has no machine-checked proof. Formalizing it requires the concurrent-flow LP, the uniform sparsest cut, graph distance balls in bounded-degree graphs and a counting argument that converts path lengths into capacity usage; each of these is reusable. The unconditional Theorem 1 additionally needs the existence of bounded-degree expanders on every number of nodes, which is a substantial formalization project in its own right.

Difficulty

The min-cut bound and the ball bound are elementary. The central step is milestone 4: turning "the shortest path of a commodity has at least $\ell$ edges" into "the commodity uses at least $f\ell$ units of capacity". In an arc-flow formulation a commodity is a conservation-respecting function on arcs, not a set of paths, so the step needs either a path decomposition of each commodity's flow or a weak-duality argument with unit edge lengths. The obvious attempt, summing the conservation equations directly, gives only the net flow across one cut and loses the factor $\ell$.

The unconditional Theorem 1 is hard for a different reason: the paper cites the existence of 3-regular expanders and does not prove it, and the theorem asks for every $n$, including odd $n$, where no 3-regular graph exists.

Formalization scope

Nodes are a Fintype $V$ with decidable equality and $n=|V|$. A network is a symmetric nonnegative real capacity function with zero diagonal; the unit-capacity network of a simple graph $G$ has $C(u,v)=1$ on edges and $0$ elsewhere. Commodities are ordered pairs $(s,t)$, $s\ne t$, each with demand $\tfrac12$ (the paper's footnote 2), so each unordered pair carries one unit; a flow is a nonnegative arc flow per commodity, and both directions of an edge share its capacity. The max-flow is the supremum of feasible fractions. The min-cut ranges over nonempty proper $U$ only: at $U=\emptyset$ or $V$ the ratio is $0/0$, which Lean reads as $0$ and which would make $\mathcal S=0$.

Conventions and added hypotheses:

• The floor. The page writes $\log n-2$. Its argument shows that far pairs have distance at least $\lfloor\log n\rfloor-2$, which differs from $\log n-2$ for non-integer $\log n$. The goal and milestones state $\lfloor\log n\rfloor-2$ (Nat.log 2 n), a different constant in the same $\Theta(\log n)$.
• $n\ge 8$ makes $\lfloor\log n\rfloor-2\ge1$, so the bound divides by a positive number.
• Graph distance is the extended distance, $\infty$ between components, never Lean's junk value $0$.
• Regularity is SimpleGraph.IsRegularOfDegree 3.
• Theorem 1 requires the network to be connected (the paper's standing assumption, p. 789); a disconnected network has $f=\mathcal S=0$ and would make the statement empty. Its constant is quantified before $n$.
• Polynomial-time claims are not formalized.

The hypotheses of the goal are satisfiable: the 3-cube $Q_3$ ($n=8$) is 3-regular and a $1$-edge-expander. Contributions welcome: the arc-flow path-length lemma, the ball bound for bounded-degree graphs, and an existence theorem for 3-regular expanders.

Selected references

• T. Leighton and S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46(6):787–832, 1999. https://doi.org/10.1145/331524.331526
• G. A. Margulis, Explicit constructions of concentrators, Problems of Information Transmission 9(4):325–332, 1973.
• N. Linial, E. London and Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2):215–245, 1995. https://doi.org/10.1007/BF01200757
• S. Arora, S. Rao and U. Vazirani, Expander flows, geometric embeddings and graph partitioning, J. ACM 56(2):5, 2009. https://doi.org/10.1145/1502793.1502794