Complexity Theory

Motivation

Combinatorial optimization problems are routinely solved by writing the convex hull of their feasible solutions as the feasible region of a linear program. When that convex hull has exponentially many facets, a classical trick is to add auxiliary variables: a polytope with many facets may be the linear projection of a higher-dimensional polyhedron with few. The spanning tree polytope, the permutahedron and the parity polytope all have compact descriptions of this kind. This raises the question of whether every polytope of an NP-hard problem might also have one, which would yield a polynomial-size linear program for that problem.

In the late 1980s several papers claimed polynomial-size linear programs for the traveling salesman problem (TSP). Yannakakis (STOC 1988; JCSS 1991) refuted all such claims at once by showing that every symmetric extended formulation of the TSP polytope has exponential size. He asked whether the symmetry assumption could be removed. Fiorini, Massar, Pokutta, Tiwary and de Wolf (STOC 2012; J. ACM 2015) answered the question: every extended formulation of the TSP polytope, symmetric or not, has $2^{\Omega(\sqrt n)}$ inequalities.

Timeline.

• 1990: De Simone shows that the correlation polytope is linearly isomorphic to the cut polytope.
• 1991: Yannakakis proves the factorization theorem (extension complexity equals the nonnegative rank of a slack matrix) and the exponential lower bound for symmetric formulations of the TSP and perfect matching polytopes.
• 1992: Razborov proves the distributional lower bound for set disjointness.
• 2003: de Wolf shows that the support of $M(n)_{ab}=(1-a^\top b)^2$ needs $2^{\Omega(n)}$ rectangles to cover.
• 2012/2015: Fiorini et al. prove $\mathrm{xc}(\mathrm{CUT}(n))=2^{\Omega(n)}$, $\mathrm{xc}(\mathrm{TSP}(n))=2^{\Omega(\sqrt n)}$, and a $2^{\Omega(\sqrt n)}$ bound for stable set polytopes of some graphs on $n$ vertices.
• 2013: Kaibel and Weltge give a short combinatorial proof of the correlation-polytope bound, with constant $C=\log_2(3/2)$.
• 2014: Rothvoss proves $2^{\Omega(n)}$ for the perfect matching polytope.

Setting

Let $\iota$ be a finite index set. An extended formulation (EF) of a set $P\subseteq\mathbb R^{\iota}$ is a linear system $E^{=}x+F^{=}y=g^{=}$, $E^{\le}x+F^{\le}y\le g^{\le}$ in variables $(x,y)\in\mathbb R^{\iota}\times\mathbb R^{k}$ such that $x\in P$ exactly when some $y$ satisfies it. Its size is the number of inequalities. The extension complexity $\mathrm{xc}(P)$ is the least size of an EF of $P$.

A polytope is the convex hull of finitely many points. A face of $P$ is $P$ itself or its intersection with a valid hyperplane, and a facet is a maximal proper face. A polytope $Q$ is an extension of $P$ if $\pi(Q)=P$ for some linear map $\pi$. Given $P=\{x : Ax\le b\}=\mathrm{conv}(V)$, the slack matrix has entries $S_{ij}=b_i-A_iv_j$. The nonnegative rank $\mathrm{rank}_+(M)$ is the least $r$ with $M=TU$, where $T\ge 0$ has $r$ columns and $U\ge 0$ has $r$ rows.

For $n$-bit strings $a,b$, $a^\top b$ is the number of common ones, and $M(n)$ is the $2^n\times 2^n$ matrix $M_{ab}=(1-a^\top b)^2$. A 1-monochromatic rectangle cover of its support is a family of products $R_1\times R_2$, each containing only entries with $M_{ab}\ne 0$, that together contain all of them.

On the complete graph $K_n=(V_n,E_n)$, $\chi^F\in\mathbb R^{E_n}$ is the characteristic vector of an edge set $F$ and $\delta(X)$ is the cut of $X\subseteq V_n$. The polytopes are

Formalization targets

Goal: Theorem 12

The constant is left unfixed, so the goal survives any improvement of it.

Milestones, in attack order

• Razborov's distributional bound (displayed in the proof of Theorem 1) and Theorem 1: every 1-rectangle cover of the support of $M(n)$ has $2^{\Omega(n)}$ rectangles.
• Lemma 2 and Theorem 3 (Yannakakis): $\mathrm{rank}_+(S)\le r$ $\iff$ an extension with at most $r$ facets $\iff$ an EF with at most $r$ inequalities.
• Theorem 4: $\mathrm{rank}_+(M)$ is at least the rectangle covering bound of its support (already proved on the platform, referenced).
• Theorem 5: $\mathrm{COR}(n)$ is linearly isomorphic to $\mathrm{CUT}(n+1)$. Lemma 6: $\langle 2\,\mathrm{diag}(a)-aa^\top,x\rangle\le 1$ is valid for $\mathrm{COR}(n)$, with slack $M_{ab}$ at $bb^\top$.
• Theorem 7: $\mathrm{xc}(\mathrm{CUT}(n+1))=\mathrm{xc}(\mathrm{COR}(n))\ge 2^{Cn}$.
• Lemma 9: $\mathrm{xc}$ does not increase under taking faces or linear images. Lemma 11: $\mathrm{TSP}(q)$ with $q=O(n^2)$ has a face that is an extension of $\mathrm{COR}(n)$.
• Stable sets: Lemma 8 and Theorem 10, $\mathrm{xc}(\mathrm{STAB}(G_n))=2^{\Omega(\sqrt n)}$ for some graph $G_n$ on $n$ vertices.

Significance

The theorem rules out every polynomial-size linear programming formulation of the TSP polytope, in any number of auxiliary variables, which settles Yannakakis's question. The cut polytope bound does the same for max-cut, and the stable set bound for the stable set problem on general graphs. The results do not depend on P vs NP: they concern one specific model of computation, linear programs whose feasible region projects onto the polytope. They started a line of work on extension complexity, including perfect matching (Rothvoss), approximate EFs and semidefinite lifts.

Formalizing the result would produce a machine-checked chain from a communication-complexity bound to a polyhedral one. The paper's results are proved; the input of Theorem 1, Razborov's bound, is only cited, and is posed here as a separate target. To our knowledge none of these statements has a formal proof in Lean or another proof assistant. The polyhedral layer (Yannakakis's theorem, faces and extensions) and the matrix layer (nonnegative rank, rectangle covers) can be reused for later extension-complexity results.

Difficulty

The obvious approach, bounding the number of facets of the TSP polytope, does not work: extended formulations exist precisely because a projection can have far more facets than the lifted polyhedron. Any lower bound must cover every lifting at once, which means working with the nonnegative rank of a slack matrix rather than with any concrete formulation. Ordinary rank is no help, because $M(n)$ has rank $O(n^2)$. The step that carries the weight is Razborov's distributional bound for disjointness, a nontrivial piece of communication complexity. On the polyhedral side, Lemma 11 needs a reduction from 3SAT to a directed and then an undirected Hamiltonian cycle problem, realized as a face of $\mathrm{TSP}(q)$ with $q=O(n^2)$. Theorem 12 also needs a monotonicity of $\mathrm{xc}(\mathrm{TSP}(n))$ in $n$ that the paper only indicates.

Formalization scope

• Everything is over $\mathbb R$. Points of $\mathbb R^d$ are functions $\iota\to\mathbb R$ on a finite type. $\mathbb R^{E_n}$ has one coordinate per unordered edge of $K_n$ (non-diagonal elements of Sym2 (Fin n)). $\mathbb R^{n\times n}$ is indexed by ordered pairs, and the Frobenius product is the dot product over ordered pairs. Bit strings are Fin n → Bool.
• $\mathrm{xc}$ and $\mathrm{rank}_+$ are natural numbers (sInf of the attainable sizes), never $\infty$, so no lower bound can hold through an infinite value. The size of an EF counts inequalities only.
• Every $2^{\Omega(f(n))}$ is $\exists C>0\,\exists N\,\forall n\ge N$, $2^{Cf(n)}\le\cdot$ (real power). Every $O(n^2)$ is a constant $c$ with $\le c\,n^2$, uniform in $n$.
• Theorem 7 and Lemma 11 carry an added $n\ge 1$: at $n=0$ the printed statements fail, since $\mathrm{COR}(0)$ is a point with $\mathrm{xc}=0$ and no positive $q\le c\cdot 0$ exists.
• "Linearly isomorphic" in Theorem 5 is an injective linear map carrying $\mathrm{CUT}(n+1)$ onto $\mathrm{COR}(n)$, because the two ambient spaces have different dimensions.
• In Theorem 3, $\dim P\ge 1$ is "$P$ has two distinct points". Faces include $\emptyset$ and $P$, facets are maximal proper faces, and facets are counted with an explicit finite family.
• Ruled out: a TSP polytope over ordered pairs, all cycles or directed tours, a weakened isomorphism in Theorem 5, and an extension complexity valued in $\mathbb N\cup\{\infty\}$ that is infinite on a broken EF definition.
• Welcome contributions: proofs of any milestone, in particular Lemma 2 and the factorization theorem (reusable for every later extension-complexity result), Theorem 5, and the face construction of Lemma 11; a proof of the monotonicity of $\mathrm{xc}(\mathrm{TSP}(n))$ in $n$ as a supporting lemma.

Selected references

• S. Fiorini, S. Massar, S. Pokutta, H. R. Tiwary, R. de Wolf, Exponential lower bounds for polytopes in combinatorial optimization, J. ACM 62(2), Art. 17, 2015. https://doi.org/10.1145/2716307
• M. Yannakakis, Expressing combinatorial optimization problems by linear programs, J. Comput. Syst. Sci. 43(3), 441–466, 1991. https://doi.org/10.1016/0022-0000(91)90024-Y
• A. A. Razborov, On the distributional complexity of disjointness, Theoret. Comput. Sci. 106(2), 385–390, 1992. https://doi.org/10.1016/0304-3975(92)90260-M
• R. de Wolf, Nondeterministic quantum query and communication complexities, SIAM J. Comput. 32(3), 681–699, 2003. https://doi.org/10.1137/S0097539702407345
• C. De Simone, The cut polytope and the Boolean quadric polytope, Discrete Math. 79(1), 71–75, 1990. https://doi.org/10.1016/0012-365X(90)90056-N
• V. Kaibel, S. Weltge, A short proof that the extension complexity of the correlation polytope grows exponentially, Discrete Comput. Geom. 53, 397–401, 2015. https://doi.org/10.1007/s00454-014-9655-9
• T. Rothvoss, The matching polytope has exponential extension complexity, J. ACM 64(6), Art. 41, 2017. https://doi.org/10.1145/3127497

Motivation

Maximizing a nonnegative submodular set function without constraints contains Max Cut, Max Directed Cut and facility-location problems as special cases. In the value-oracle model an algorithm knows nothing about the function except the values $f(S)$ of the sets $S$ it queries, and it is judged by the number of queries it makes. Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave constant-factor algorithms in this model and matching limits on what any algorithm can do. For symmetric functions, such as cut functions of undirected graphs, a uniformly random set already achieves $\tfrac12$ of the optimum in expectation (Theorem 2.1 of the paper). The question this mission formalizes is whether any algorithm can do better, and the answer given by Theorem 4.5 is: not without exponentially many value queries. The same factor $\tfrac12$ was later shown to be achievable for general (non-symmetric) nonnegative submodular functions by Buchbinder, Feldman, Naor and Schwartz (FOCS 2012 / SIAM J. Comput. 2015), so the bound of Theorem 4.5 is the tight limit of the whole problem in the value-oracle model.

Timeline:

• 2007 (FOCS) / 2011 (SIAM J. Comput.): Feige, Mirrokni and Vondrák prove that no algorithm with subexponentially many value queries achieves $(\tfrac12 + \epsilon)$ of the optimum on symmetric nonnegative submodular functions, and give $\tfrac25$ for general functions.
• 2011: Vondrák's symmetry-gap framework (SIAM J. Comput. 42(1), 2013) generalizes the construction to constrained problems.
• 2012: Buchbinder, Feldman, Naor and Schwartz give a randomized $\tfrac12$-approximation for general nonnegative submodular functions, matching the bound.

Setting

Let $[n] = \{0, \dots, n-1\}$ be the ground set, with $n$ even. A set function $f : 2^{[n]} \to \mathbb{R}$ is submodular if $f(S \cup T) + f(S \cap T) \le f(S) + f(T)$ for all $S, T$, symmetric if $f([n]\setminus S) = f(S)$ for all $S$, and $\mathrm{OPT}(f) = \max_{S} f(S)$.

Fix an integer $m$ with $1 \le m \le n/2$ and write $\epsilon = m/n$, so that $\epsilon n$ is an integer. For integers $k, \ell$ put

For a set $C \subseteq [n]$ with $|C| = n/2$ and $D = [n] \setminus C$, the hard instance is $f_C(S) = f(|S\cap C|, |S\cap D|)$. The cut function of the complete graph is $g(S) = |S|(n-|S|)$, with maximum $\tfrac14 n^2$. A set $Q$ is balanced for $C$ if $\bigl||Q\cap C| - |Q\cap D|\bigr| \le m$; on balanced sets $f_C = g$.

A deterministic adaptive $q$-query algorithm $A$ chooses each query from the answers received so far, and after $q$ answers outputs a set $A(h)$ when run against an oracle $h$. A randomized algorithm is a distribution $\mu$ over deterministic ones, with expected value $\mathbb{E}_{A\sim\mu}[h(A(h))]$.

Formalization targets

Goal: Theorem 4.5 with the constants of its proof

For every such $n, m$:

1. every $f_C$ with $|C| = n/2$ is nonnegative, symmetric and submodular, with

2. for every $q < e^{\epsilon^2 n/8}$ and every randomized $q$-query algorithm $\mu$ there is a $C$ with $|C| = n/2$ and

Hence the ratio attained is at most $\frac{1}{2(1-2\epsilon+2\epsilon^2)} + 4e^{-\epsilon^2 n/8} = \tfrac12 + \epsilon + O(\epsilon^2) + 4e^{-\epsilon^2 n/8}$.

Milestones

• Theorem 1.2, the Chernoff bound for independent variables in $[-1,1]$.
• Submodularity of $f_C$.
• The value $\mathrm{OPT}(f_C) = \tfrac12 n^2(1 - 2\epsilon + 2\epsilon^2)$, attained at $S = C$.
• A fixed query is unbalanced for at most a $2e^{-\epsilon^2 n/4}$ fraction of the half-size sets $C$.
• If all queries are balanced, the algorithm cannot distinguish $f_C$ from $g$.
• The deterministic case of the bound, averaged over $C$.

Significance

The theorem shows that the factor $\tfrac12$ for symmetric submodular maximization, and hence for unconstrained submodular maximization in general, cannot be improved by any algorithm that uses a subexponential number of value queries, whatever its running time. It is an information-theoretic bound and needs no complexity assumption. Along with the later matching $\tfrac12$-approximation, it settles the value-oracle approximability of the problem. The construction, a function equal to a symmetric function on "balanced" sets and larger elsewhere, is the prototype of the symmetry-gap technique used for many later oracle lower bounds.

The result is proved in the paper. No machine-checked version is known to exist: the platform has no value-oracle or query-lower-bound statement. Formalizing it requires a precise model of adaptive randomized query algorithms, a concentration bound for the hypergeometric distribution, and a finite verification of submodularity of an explicit two-regime function, and it fixes the constants that the printed statement leaves as $O(\cdot)$ terms.

Difficulty

Two steps of the printed argument do not go through as written. First, the proof bounds the probability that a fixed query is unbalanced by citing the Chernoff bound for independent variables, but for a uniformly random half-size set $C$ the count $|Q\cap C|$ is hypergeometric, and the summands are not independent. A bound for sampling without replacement is needed instead. Replacing the balanced partition by independent coin flips is not an option: then $|C| \ne n/2$ in general, and the function is no longer the paper's instance.

Second, the argument counts only the queries, but the value an algorithm receives is $f_C$ of its output, which equals $g$ of the output only if the output is balanced as well. That event has to be controlled too.

Finally, submodularity of $f_C$ must be checked across the boundary $|k-\ell| = \epsilon n$ between the two regimes, where the formula changes.

Formalization scope

• The ground set is Fin n with $n$ even; $\epsilon n$ is an integer $m$ with $1 \le m$ and $2m \le n$, following the paper's "assume that $\epsilon n$ is an integer". Sets are Finset (Fin n), and all values are real.
• $\mathrm{OPT}$ is Finset.sup' over all subsets. There is no junk value.
• The partition $(C, D)$ is uniform over half-size sets; probabilities over it are counts of n/2-subsets divided by $\binom{n}{n/2}$, written multiplied out.
• A deterministic algorithm is a pair of decision rules query, output : List ℝ → Finset (Fin n) making exactly $q$ adaptive queries with arbitrary real answers. A randomized algorithm is a PMF over deterministic algorithms, which covers every randomization with countable support. The algorithm sees $f$ only through query answers; it never receives $C$.
• Pinned-down constants. The printed theorem, "fewer than $e^{\epsilon^2 n/8}$ queries" and "expected value at least $(\tfrac12+\epsilon)\mathrm{OPT}$", is not what the proof gives for one and the same $\epsilon$. On the proof's instances $\mathrm{OPT} = \tfrac12 n^2(1-2\epsilon+2\epsilon^2)$, and the ratio held is $\frac{1}{2(1-2\epsilon+2\epsilon^2)} > \tfrac12 + \epsilon$. The formal goal states the explicit bound the proof establishes. The literal printed pair, stated for the proof's family with the same $\epsilon$, is false: the zero-query algorithm that outputs a fixed half-size set gets at least $\tfrac14 n^2 > (\tfrac12+\epsilon)\mathrm{OPT}$.
• Added term. The error term $2e^{-\epsilon^2 n/4}$ for the output set is added to the paper's $2e^{-\epsilon^2 n/8}$.
• Ruled-out trivializations. A restricted algorithm class (non-adaptive, deterministic, or one that must return a queried set) would give a different, weaker theorem. So would a bound that lets the algorithm read $C$, which would make the statement false. Both the instance's properties (nonnegativity, symmetry, submodularity, the value of OPT) and the bound are part of the goal, so an empty or degenerate family cannot satisfy it. The quantifier order is: for every algorithm there is an instance.
• Needed infrastructure: a value-oracle algorithm model; tail bounds for the hypergeometric distribution (Hoeffding's inequality for sampling without replacement), which Mathlib lacks; averaging over a PMF of algorithms. The algorithm model and the hypergeometric bound are reusable for other oracle lower bounds. Proofs of any milestone, and alternative derivations of the balance bound, are welcome.

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM J. Comput. 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• N. Alon, J. H. Spencer, The Probabilistic Method, Wiley (source of Theorem 1.2).
• W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, J. Amer. Statist. Assoc. 58(301):13–30, 1963. https://doi.org/10.1080/01621459.1963.10500830
• J. Vondrák, Symmetry and Approximability of Submodular Maximization Problems, SIAM J. Comput. 42(1):265–304, 2013. https://doi.org/10.1137/110832318
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM J. Comput. 44(5):1384–1402, 2015. https://doi.org/10.1137/130929205

Motivation

The nearest common ancestor problem asks, for a rooted tree and two of its vertices $x$ and $y$, for the deepest vertex that is an ancestor of both, written $\operatorname{nca}(x,y)$. It appears as a subroutine in string algorithms (suffix trees), in graph algorithms (path queries, dominators) and in the analysis of set-union structures. Aho, Hopcroft and Ullman (On finding lowest common ancestors in trees, SIAM J. Comput. 5, 1976) posed it in several versions, differing in how much the tree changes while the queries are answered.

Harel and Tarjan (Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13, 1984) study how the answer depends on the machine model. On a random-access machine, where addresses can be computed arithmetically, they preprocess a static tree in linear time and then answer each query in constant time. On a pointer machine, where memory can only be traversed by following pointers, their §2 shows that no representation of the tree allows constant-time queries: $\Omega(\log\log n)$ steps are needed in the worst case. This mission formalizes that lower bound.

Timeline.

• 1976: Aho, Hopcroft and Ullman give an $O(\log\log n)$-per-query random-access algorithm for static trees.
• 1976: van Leeuwen (Finding lowest common ancestors in less than logarithmic time, unpublished report, reference [14] of Harel–Tarjan) gives an $O(n + m\log\log n)$ algorithm for static trees that runs on a pointer machine.
• 1984: Harel and Tarjan prove Theorem 1, the matching $\Omega(\log\log n)$ lower bound for pointer machines, and the $O(1)$-per-query random-access algorithm.

Setting

A pointer machine stores its data as a collection of nodes. Each node has a fixed number of fields, and a pointer field holds either a node or nil. The machine can follow a pointer from a node it holds, but it cannot compute an address. Following Harel and Tarjan (p. 340), a static tree is represented by a list structure: each tree vertex $v$ is represented by a single node $\mathrm{rep}(v)$, distinct vertices by distinct nodes, and the structure may contain further nodes that represent no vertex. Each node has two pointer fields; the paper reduces any fixed number of pointers to two "without loss of generality". To answer a query on $x$ and $y$, the machine is given pointers to $\mathrm{rep}(x)$ and $\mathrm{rep}(y)$ and must return a pointer to $\mathrm{rep}(\operatorname{nca}(x,y))$.

The node $b$ is accessible from $a$ in $j$ steps or less if it can be reached from $a$ by following at most $j$ pointers. Write $\mathrm{acc}_j(a)$ for the set of such nodes. A run of $t$ steps from input nodes $a$ and $b$ is a sequence $n_1,\dots,n_t$ in which each $n_s$ is the content of a pointer field of a node among $a, b, n_1, \dots, n_{s-1}$. A query with answer $c$ is answered in $k$ steps if some run of at most $k$ steps holds $c$.

The tree is the complete binary tree $T$ of height $h$, with $n = 2^h$ leaves. Its vertices are the words $w \in \{0,1\}^{\le h}$ (the root-to-vertex path, $0$ = left), the ancestors of $v$ are its prefixes, the depth of $w$ is $|w|$ and its height is $h - |w|$. Then $\operatorname{nca}(x,y)$ is the longest common prefix of $x$ and $y$. Logarithms are binary: $\lg = \log_2$.

Formalization targets

Goal: Theorem 1 in the explicit form of its proof

For every $h$, every node type, every list structure with two pointers per node and every injective representation $\mathrm{rep}$ of the complete binary tree with $n = 2^h$ leaves: if every nca query on two leaves is answered in $k$ steps, then

This is the last display of the proof (p. 341), which is what the paper's $\Omega(\log\log n)$ means. The representation is arbitrary and is quantified before the query bound, so the bound holds for every representation.

Milestones: the claims of the proof

1. A query answered in $k$ steps reaches only nodes in $\mathrm{acc}_k(\mathrm{rep}(x)) \cup \mathrm{acc}_k(\mathrm{rep}(y))$.
2. $|\mathrm{acc}_j(a)| \le 2^{j+1} - 1$ for every node $a$.
3. With $A_x$ the set of vertices whose nodes are accessible from $\mathrm{rep}(x)$ in $k$ steps or less: for a nonleaf $w$ with children $u, v$, either $w \in A_x$ for every leaf $x$ below $u$, or $w \in A_y$ for every leaf $y$ below $v$.
4. A vertex of height $i \ge 1$ lies in $A_x$ for at least $2^{i-1}$ leaves $x$.

where $L$ is the set of leaves.

Significance

The result. Theorem 1 shows that van Leeuwen's pointer-machine algorithm for static trees is optimal up to a constant factor, and that the constant-time queries of the paper's §§3–5 depend on address arithmetic. It is an early nontrivial lower bound for pointer machines on a natural problem; the paper compares it with Tarjan's lower bound for disjoint-set union on a pointer machine (J. Comput. System Sci. 18, 1979).

Formalizing it. The theorem is proved in the paper; as far as could be determined no machine-checked version exists, and Mathlib has no pointer-machine model. The mission produces an explicit, reusable definition of pointer-machine runs and accessibility together with a complete proof of the explicit bound. A formal model of this kind is the precondition for stating any other pointer-machine lower bound.

Difficulty

The statement must hold for every representation, including structures with many auxiliary nodes and arbitrary pointers between tree nodes. Arguing about one natural representation, such as parent pointers, where a leaf is far from its ancestors, says nothing about other representations: a structure with shortcut pointers or auxiliary nodes may bring some ancestors close to some leaves, and the bound must survive every such choice. In the formal setting the counting also has to handle overlaps: nodes reachable from several leaves, nodes that represent no vertex, and pointer cycles.

Formalization scope

• Model. Nodes form an arbitrary type N, not necessarily finite. ptr : N → Fin 2 → Option N gives the two pointer fields (none = nil), and rep : Vertex h → N is required to be injective. acc ptr j a is defined recursively. Run ptr a b t held is an inductive predicate for runs of $t$ steps, AnsweredIn asks for some run of at most $k$ steps holding the answer, and AnswersLeafQueriesIn ptr rep k requires this for every pair of leaves.
• Conventions.
  • Two pointer fields per node, as the paper's "without loss of generality" reduction allows; the reduction itself is not formalized.
  • Only queries on two leaves are assumed answerable. This is weaker than all queries, so the theorem is at least as strong as the paper's.
  • Time is counted as pointer-following steps. Mutation of the structure during a query and non-pointer fields are not modelled: neither lets the machine hold a node it has not reached by following pointers. The clause "the algorithm remembers nothing between queries" is built into the static structure.
  • Vertex h is {s : List Bool // s.length ≤ h}, nca is the longest common prefix, and a separate theorem identifies it with the Appendix's deepest common ancestor. $n = 2^h$ counts leaves, not vertices.
  • $\lg$ is Real.logb 2. For $h = 0$ Lean's $\log_2 0 = 0$ gives the true statement $k > -2$; for $h \ge 1$, $\lg\lg n = \log_2 h$.
  • Cardinalities in the milestones are Set.encard in $\mathbb N \cup \{\infty\}$, so finiteness is part of each claim. Divisions are cleared: $h\,2^h \le 2\sum_x |A_x|$.
• Ruling out trivial formalizations. The hypothesis AnswersLeafQueriesIn is satisfiable: the parent-pointer representation answers every leaf query in $h$ steps. If rep were not injective, a constant rep would answer every query in zero steps, so injectivity is kept in the goal. The milestones do not need it and do not assume it.
• Infrastructure. The goal needs finite-set counting over the leaves of the complete binary tree and a double count over heights. The run and accessibility definitions are reusable for other pointer-machine arguments. Proofs of the milestones, and of the ℕ form $h < 2^{k+2}$ that the goal reduces to, are welcome.

Selected references

• D. Harel, R. E. Tarjan, Fast Algorithms for Finding Nearest Common Ancestors, SIAM J. Comput. 13(2):338–355, 1984. https://doi.org/10.1137/0213024
• A. V. Aho, J. E. Hopcroft, J. D. Ullman, On finding lowest common ancestors in trees, SIAM J. Comput. 5(1):115–132, 1976. https://doi.org/10.1137/0205011
• A. Schönhage, Storage modification machines, SIAM J. Comput. 9(3):490–508, 1980. https://doi.org/10.1137/0209036
• R. E. Tarjan, A class of algorithms which require nonlinear time to maintain disjoint sets, J. Comput. System Sci. 18(2):110–127, 1979. https://doi.org/10.1016/0022-0000(79)90042-4

Motivation

Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an $O(n\log n)$ bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.

Setting

A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.

An input consists of two bit strings $x,y$ of the same positive length $n$, separated by $\#$. The strings are read most significant bit first, with leading zeros permitted. If $\operatorname{val}(x)$ denotes the represented natural number, the required output is exactly the $2n$-bit binary representation of $\operatorname{val}(x)\operatorname{val}(y)$, padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define $L(n)=\max(\lceil\log_2 n\rceil,1)$.

Target

The full target is

This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants $c>0$ and $n_0$ such that every pair of $n$-bit inputs, for $n\ge n_0$ and $n\ge1$, halts within

steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger $\kappa$ gives a stronger asymptotic saving because $L(n)\ge1$.

Each entry supplies its own exact numerical value and identifies the construction that motivates it. Historical and new entries use the same machine definition. A proposed value may be recorded while its complete proof is still open; it becomes a proved record only when the goal has a verified proof. Numerical certificates are supporting results with their own scope, and do not establish a complete machine time bound.

Significance

A proof for any positive value would give a strict asymptotic improvement over $n\log n$. Such an improvement would contradict the proposed $\Omega(n\log n)$ lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.

Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.

Difficulty

A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.

Formalization scope

The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.

The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.

Selected references

• D. Harvey and J. van der Hoeven, Integer multiplication in time O(n log n), Annals of Mathematics 193(2), 563–617 (2021). Paper.
• OpenAI, Integer multiplication below n log n, preprint (23 September 2026), pinned manuscript revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source.
• D. Colkitt and community contributors, A sharper exponent for integer multiplication, research repository (2026), revision 56b66d58297deca1d7dd130247d720e960f77a37. Checkpoint and attribution.

Motivation

Multiplying two binary integers is a basic task in computational complexity. The relevant resource here is the number of individual steps made by a machine whose tapes can only be accessed through moving heads. Harvey and van der Hoeven established an $O(n\log n)$ bound in this model. The OpenAI manuscript proposes a positive saving in the exponent of the logarithm. Subsequent constructions explore larger savings. The formalization target is the complete computation and its time bound, including the analytic and implementation arguments needed to connect a finite construction to every input length.

Setting

A deterministic multitape Turing machine has a fixed finite alphabet, a fixed finite state set, and a fixed finite number of tapes. Each tape extends in one direction and has one head. A step reads the symbols under the heads, changes state, writes at those positions, and moves each head by at most one cell. The alphabet contains distinct blank, start-marker, zero, one, and separator symbols. Tape zero is the read-only input tape; tape one is the output tape; further tapes are available for work. The halting state freezes the configuration.

An input consists of two bit strings $x,y$ of the same positive length $n$, separated by $\#$. The strings are read most significant bit first, with leading zeros permitted. If $\operatorname{val}(x)$ denotes the represented natural number, the required output is exactly the $2n$-bit binary representation of $\operatorname{val}(x)\operatorname{val}(y)$, padded with leading zeros and followed by blanks. All tapes begin with a preserved start marker. Define $L(n)=\max(\lceil\log_2 n\rceil,1)$.

Target

The full target is

This asserts the existence of one machine that computes the exact product correctly for every positive input length, together with constants $c>0$ and $n_0$ such that every pair of $n$-bit inputs, for $n\ge n_0$ and $n\ge1$, halts within

steps. Constants, alphabet, states, and tape count are independent of the input length. The number is an exact real value. Larger $\kappa$ gives a stronger asymptotic saving because $L(n)\ge1$.

Each entry supplies its own exact numerical value and identifies the construction that motivates it. Historical and new entries use the same machine definition. A proposed value may be recorded while its complete proof is still open; it becomes a proved record only when the goal has a verified proof. Numerical certificates are supporting results with their own scope, and do not establish a complete machine time bound.

Significance

A proof for any positive value would give a strict asymptotic improvement over $n\log n$. Such an improvement would contradict the proposed $\Omega(n\log n)$ lower bound, while remaining consistent with the known upper bound. The tracked value concerns asymptotic growth; it does not measure the runtime of a practical implementation. No claim about a currently fastest implementation follows from a larger saving.

Formalizing the full target connects exact finite calculations to a uniform algorithm. The community repository explicitly treats the original framework and remaining all-size interfaces as assumptions of its current evidence. In this mission those steps must be proved before the goal can be marked Proved. They are not added as hypotheses that would weaken the full target. Earlier published theorem statements and finite certificates may be reused with their original attribution and proof status.

Difficulty

A finite network certificate can establish a concrete role count or a rational margin, but does not itself supply a machine for every input length. A complete proof must establish correctness of the recursive construction, admissibility of its parameters, precision and error guarantees, and the cost of moving data on tapes. Counts of algebraic operations alone do not account for this last resource. The difficult connection is between these separate contracts and the single uniform machine quantified by the goal.

Formalization scope

The goal imports the existing public Definitions.Def_IntMul_MultitapeModel bundle and uses IntMul.KappaBound directly. No alternative machine or cost model is introduced. Natural numbers describe input lengths, head positions, and step counts; real numbers describe the asymptotic constant and exponent. The real power has base at least one. Correctness is required even below the asymptotic threshold. Inputs of length zero and malformed inputs are outside the specified task.

The input and output conventions exclude a machine that merely decides a predicate about the product. The entire output tape must contain the required product and then blanks. Neither failure to halt nor correctness on a finite collection of test inputs meets the target. The work tapes and final head positions are unconstrained. Reusable contributions include machine composition with explicit costs, exact encodings, analytic estimates, and proofs that the finite certificates imply the contracts required by the recursive algorithm. Every such contribution should state its own assumptions and conclusion explicitly.

Selected references

• D. Harvey and J. van der Hoeven, Integer multiplication in time O(n log n), Annals of Mathematics 193(2), 563–617 (2021). Paper.
• OpenAI, Integer multiplication below n log n, preprint (23 September 2026), pinned manuscript revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source.
• D. Colkitt and community contributors, A sharper exponent for integer multiplication, research repository (2026), revision 56b66d58297deca1d7dd130247d720e960f77a37. Checkpoint and attribution.

Status

A full Lean proof of this bound is already on the platform: NLogN.KFTop.kappa_bound (theorem f904f4ef), which also proved IntMul.Kappa.openai_theorem_1. It formalizes the OpenAI manuscript's construction (Prop 7/8 networks, τ = 1−2^-50, crude assembly) on top of a verified multitape-machine compiler and the Harvey–van der Hoeven O(n log n) machine. It uses only the standard axioms.

Certify the classical quadratic separation between sensitivity and block sensitivity: $\alpha\ge2$.