Motivation

Schönhage and Strassen conjectured in 1971 that $n\log n$ is the optimal order of growth for multiplying two $n$-bit integers on a multitape Turing machine. Harvey and van der Hoeven proved the matching upper bound $O(n\log n)$ (Annals of Mathematics, 2021). In September 2026, a preprint by OpenAI, Integer multiplication below $n\log n$, claimed that this bound can itself be beaten by a power of the logarithm, in the same model. If correct, the upper half of the conjecture's "$\Theta(n\log n)$" is false. Two independent follow-up projects then increased the exponent saving $\kappa$ by many orders of magnitude. This mission targets the strongest claimed saving and takes the earlier claims as milestones.

Timeline (multitape Turing model; all bounds are of the form $O(n(\lg n)^{1-\kappa})$).

• 2021: Harvey and van der Hoeven, $\kappa=0$, that is, $O(n\log n)$. Published and refereed.
• 23 September 2026: OpenAI preprint, $\kappa=2^{-182}$ (Theorem 1 of the preprint). The preprint has not been refereed.
• October 2026: D. Colkitt, integer-mult-bounds, a series of patches to the OpenAI manuscript with checked numerical certificates, reaching $\kappa=2^{-30}$. The project describes this as conditional on the OpenAI manuscript and as having had no independent review.
• October 2026: S. Jain, integer-mult-kappa, building on both, reaching $\kappa=3666565558019/10^{17}\approx3.67\times10^{-5}>2^{-15}$ ("round six"). It is also stated to be conditional and unreviewed. Its numerical certificate is checked by computation in the Lean kernel, but the analytic facts behind that certificate are taken as premises.

Setting

A $k$-tape Turing machine, in the conventions of Montanaro's Computational Complexity lecture notes (§3, §3.4), has the following parts:

• a finite alphabet containing a blank $\square$ and a start symbol $\triangleright$;
• a finite set of states with a start state $\mathrm{START}$ and a distinct halting state $\mathrm{HALT}$;
• $k\ge2$ tapes: a read-only input tape, an output tape, and $k-2$ work tapes. Each tape is infinite in one direction, has its own head, and holds $\triangleright$ in its first cell and nowhere else.

In one step the machine reads the symbol under every head, writes a symbol under every head, moves each head by at most one cell (never left of $\triangleright$), and changes state. Once in $\mathrm{HALT}$ it stays there unchanged.

For $x\in\{0,1\}^n$ (most significant bit first), $\operatorname{val}(x)$ is the integer that $x$ represents, and $\operatorname{bin}_k(z)$ is the length-$k$ binary representation of $z$. A machine computes the product if, for every $n\ge1$ and all $x,y\in\{0,1\}^n$, when started on input $\triangleright\,x\#y$ it reaches $\mathrm{HALT}$ with the output tape holding exactly $\triangleright\,\operatorname{bin}_{2n}(\operatorname{val}(x)\operatorname{val}(y))$ followed by blanks. Its running time $T(n)$ is the largest number of steps on any pair of $n$-bit inputs. With $\lg n=\max(\lceil\log_2n\rceil,1)$, define

$$\mathrm{KappaBound}(\kappa)\iff \exists\,M\text{ computing the product with }T(n)=O\big(n(\lg n)^{1-\kappa}\big).$$

Formalization targets

Goal

$$\mathrm{KappaBound}\!\left(\tfrac{3666565558019}{10^{17}}\right).$$

Milestones: the earlier, weaker bounds

1. $\mathrm{KappaBound}(0)$: Harvey–van der Hoeven, Theorem 1.1. This is stated as a milestone of the companion mission, in the same machine model, and is referenced here.
2. $\mathrm{KappaBound}(2^{-182})$: OpenAI, Theorem 1.
3. $\mathrm{KappaBound}(2^{-30})$: Colkitt's ternary five-subset checkpoint.

Each milestone is implied by the goal, because $(\lg n)^{1-\kappa}$ decreases in $\kappa$. Each one is also a published claim in its own right and a natural intermediate formalization target. The $\kappa=0$ and $\kappa=2^{-182}$ constructions are the ones that the later claims rely on.

Significance

The result. Any $\kappa>0$ shows that $n\log n$ is not the optimal running time for multitape machines, which refutes the upper half of the Schönhage–Strassen conjecture as usually stated. The OpenAI preprint also derives the same bound for exact division and integer square roots (its Corollary 2). Larger values of $\kappa$ quantify how far below $n\log n$ multiplication can go. The bound is a statement about growth rates, and the constants involved are astronomically large.

Formalizing it. None of the three positive-$\kappa$ results has been refereed, and the two follow-ups explicitly depend on the OpenAI manuscript. Their written arguments, their computer-checked combinatorial certificates (rank sums, moment bounds, rational margins), and the full multiplication theorem have not been formally verified. Machine-checking any of the milestones would be the first independent confirmation of the corresponding claim. A formal disproof, or a formal identification of a gap, would be equally informative.

Difficulty

Fourier-based multiplication scans $\Theta(n)$ stored bits at each of $\Theta(\log n)$ transform levels, so any algorithm that performs those levels one at a time pays $\Theta(n\log n)$ for data movement and arithmetic alone. Beating this requires both moving data and carrying out butterfly layers at cost $o(V\log n)$ on a tape that is accessed sequentially, where $V$ is the stored volume. In the preprint this is done with recursive linear networks whose total number of smaller calls is strictly less than (number of roles) × (arity). The follow-ups improve $\kappa$ by finding better networks and tighter parameter choices, all certified by large exact computations. Each claim therefore combines a long analytic argument, a Turing-machine implementation, and a finite certificate, and all three must be formalized.

Formalization scope

• Machine model. The definitions are in IntMul_MultitapeModel, shared with the Harvey–van der Hoeven mission, and follow the $k$-tape conventions of Montanaro's lecture notes. Tapes begin with $\triangleright$. There is a $\mathrm{HALT}$ state that freezes the configuration. Tape $0$ is a read-only input tape holding $\triangleright\,x\#y$, and tape $1$ is the output tape, which must hold exactly $\triangleright$, then the product bits, then blanks. Running time is the number of steps until $\mathrm{HALT}$.
• The bound. As in the notes' definition of $O(\cdot)$: there are $c>0$ and $n_0$ with $T(n)\le c\,n(\lg n)^{1-\kappa}$ for $n\ge n_0$, and correctness is required for every $n\ge1$. Following the papers, $n$ is the length of each operand. The exponent $1-\kappa$ is a real power of a number that is at least $1$.
• No trivial solutions. A machine that fails to halt, or halts with a wrong output, on any well-formed input fails the definition. A proof must exhibit one fixed machine for all $n$.
• Infrastructure needed: Turing-machine composition with cost accounting; the Harvey–van der Hoeven reduction; the Nussbaumer synthetic transforms; the interchange and butterfly-layer networks of the preprint, with their rank and moment certificates; and the parameter assembly. The machine library and the certificate-checking infrastructure can be reused in other complexity missions.
• Welcome contributions: formal verification of the published certificates; formalization of the preprint's linear-network propositions; and machine-checked counterexamples to any step.

Selected references

• OpenAI, Integer multiplication below $n\log n$, preprint, 23 September 2026. https://github.com/openai/math/blob/main/preprints/Integer-multiplication-below-n-log-n-September-23-2026/paper.pdf
• D. Colkitt, A sharper exponent for integer multiplication (integer-mult-bounds), research draft, 2026. https://github.com/CrocSwap/integer-mult-bounds
• S. Jain, Integer multiplication: a conditional witness above $2^{-15}$ (integer-mult-kappa), research draft, 2026. https://github.com/Swapnil-jain/integer-mult-kappa
• D. Harvey, J. van der Hoeven, Integer multiplication in time $O(n\log n)$, Annals of Mathematics 193(2), 563–617, 2021. https://doi.org/10.4007/annals.2021.193.2.4
• A. Schönhage, V. Strassen, Schnelle Multiplikation großer Zahlen, Computing 7, 281–292, 1971. https://doi.org/10.1007/BF02242355
• H. J. Nussbaumer, Fast polynomial transform algorithms for digital convolution, IEEE Transactions on Acoustics, Speech, and Signal Processing 28(2), 205–215, 1980. https://doi.org/10.1109/TASSP.1980.1163372