Motivation

Multiplying two $n$-bit integers on a multitape Turing machine takes $O(n\log n)$ steps by the algorithm of Harvey and van der Hoeven (2021), and $n\log n$ was long conjectured to be optimal. The OpenAI manuscript Integer multiplication below $n\log n$ (September 2026) gives a machine running in time $O(n\,L(n)^{1-\kappa})$ with $\kappa = 2^{-182}$, which beats $n\log n$ by a factor that grows without bound. That theorem is now fully formalized on this platform: IntMul.Kappa.campaign_bound_inv_two_pow_182 is Proved, through the published development NLogN.KFTop.kappa_bound.

The manuscript calls its constants "deliberately conservative; no optimization is claimed." The community repository CrocSwap/integer-mult-bounds records which constants the same construction tolerates. Its patch frozen-154 keeps the original swap networks and recurrence exponents and changes only four constants of the final assembly, which raises the saving to $\kappa = 2^{-154}$. This mission formalizes that retuning.

Timeline of the saving $\kappa$ for this construction:

• 2026, OpenAI manuscript: $\kappa = 2^{-182}$, with $\varepsilon = 2^{-75}$, $c = 2^{-56}$, $\lambda' = 1 - 2^{-54}$, $\tau = 1 - 2^{-50}$. Formalized on Prove2me in October 2026.
• 2026, frozen-154 patch: $\kappa = 2^{-154}$, with $\varepsilon = c = 2^{-51}$, $\lambda = 1 - 2^{-101}$, $\lambda' = 1 - 2^{-102}$, and the same networks. Not yet formalized.
• Later community rounds (new networks, Jain's rounds six to eight) reach $\kappa \approx 10^{-4}$. They are separate entries in this campaign, and their machine-level theorems are still Open.

Setting

A multitape Turing machine has a finite alphabet, finitely many states, a read-only input tape, an output tape and finitely many work tapes. On input $x\#y$ with $x, y \in \{0,1\}^n$ it must halt with the $2n$-bit binary expansion of $\mathrm{val}(x)\cdot\mathrm{val}(y)$ on the output tape. Write $L(n) = \max(\lceil \log_2 n\rceil, 1)$. The proposition $\mathrm{KappaBound}(\kappa)$ (from IntMul_MultitapeModel) says that one such machine is correct for every $n \ge 1$ and runs in at most $C\,n\,L(n)^{1-\kappa}$ steps for all large $n$.

The OpenAI machine processes inputs of length $n$ using the parameters $b = L(n)$, $p = 6b$, $d = \lfloor b^{\varepsilon}\rfloor$ (the number of axes of the transform), $K = \lfloor d^{c}\rfloor$ (the chunk width of the transform layout), $\ell = \lceil L/d\rceil$ and $\alpha = \lceil (12 d^2 b)^{1/4}\rceil$, where $L$ is least with $4n \le 2^L b$ and $V = 2^L p$ is the bit volume. Its running time divided by $V$ is bounded by the normalized cost table (Table 1 of the manuscript)

$$N(p,d,K,\ell,\alpha) = dK + pK^{\tau-1} + \ell d^{\lambda'} + d^2(1+\ell^{\tau}) + d\,p^{1/2+\delta}\alpha + d\,p^{\delta} + (\ell + \log_2 p) + p^{\delta} + 1.$$

Each row is at most $p$ to a power below one. The seven margins below one are

$$g_1 = 1-\varepsilon(1+c),\ g_2 = \varepsilon c(1-\tau),\ g_3 = \varepsilon(1-\lambda'),\ g_4 = 1-\tau-\varepsilon(2-\tau),\ g_5 = \tfrac14-\delta-\tfrac{3\varepsilon}{2},\ g_6 = 1-\delta-\varepsilon,\ g_7 = \varepsilon,$$

and the saving is $\kappa = \tfrac12\min_i g_i$. At the manuscript's constants the minimum is $g_2 = 2^{-181}$. At the frozen-154 constants ($\tau = 1-2^{-50}$ and $\delta = 1/16$ unchanged) the minimum is $g_3 = 2^{-153}$, so $\kappa = 2^{-154}$.

The definition file IntMul_OpenAI_R154 fixes these constants, the table $N$ (named Ncost) and the parameter map dP, KP, ℓP, αP. It reuses $b$, $L$, $T$, $p$ and $V$ from the published IntMul.OpenAI.Glue, since they do not depend on the constants.

Formalization targets

Goal

$$\mathrm{KappaBound}\!\left(2^{-154}\right)$$

This is the campaign template with value $1/2^{154}$, stated over the campaign's foundation definitions.

Milestones

1. Margins: at the new constants, $2\kappa \le g_i$ for all seven margins, together with the layer conditions $\tau(1 + c/\beta) < \lambda' < 1$ (with $\beta = 1/2$) and $\lambda' - \tau - c > 0$.
2. Cost table: under the pointwise bounds $p^{\varepsilon}/12 \le d \le p^{\varepsilon}$, $p^{\varepsilon c}/24 \le K \le p^{\varepsilon c}$, $0 \le \ell \le p/(3d)$, $0 \le \alpha \le 4p^{1/4+\varepsilon/2}$, one has $N(p,d,K,\ell,\alpha) \le 50\,p^{1-2\kappa}$.
3. Parameters: for all large $n$, the concrete parameters satisfy those pointwise bounds with $p = 6L(n)$, and $0 \le V \le 48n$.
4. Reduction: a correct machine whose time is at most $C_0\big(V\cdot N \cdot (\log L(n) + 1)^A + n\big)$ for all large $n$, with any parameter sequences obeying the pointwise bounds, satisfies $\mathrm{KappaBound}(2^{-154})$.
5. Machine: there is a correct multitape machine whose time is at most $C_0\big(V\cdot N(6L(n), d, K, \ell, \alpha)\cdot(\log L(n)+1)^A + n\big)$ for all large $n$, at the concrete frozen-154 parameters.

The goal follows from milestones 3, 4 and 5 by a short argument.

Significance

The result itself. The bound improves the formally verified saving for exact integer multiplication on multitape machines from $2^{-182}$ to $2^{-154}$, a factor of $2^{28}$, without new mathematics in the networks. It also checks that the manuscript's construction is robust to its constants, which the manuscript asserts but does not exercise.

Formalizing it. The $2^{-182}$ development hard-codes $\varepsilon$ and $c$ in its parameter map (IntMul.OpenAI.Glue.dP, KP) and in the statements built on them. A development written against general constants, or a second instantiation, makes every later retuning cheap and separates what depends on the constants from what does not. Milestones 1 to 4 are short and mirror proved lemmas of the $2^{-182}$ development. Milestone 5 is the substance.

Difficulty

The cost analysis is not where the difficulty lies; it is finite arithmetic with real powers. The difficulty is milestone 5: re-establishing the machine's time bound at the new $d$ and $K$. A larger $\varepsilon$ makes $d$ grow much faster with $b$, and a larger $c$ makes the chunk width $K$ grow faster with $d$. Every lemma whose proof used the old exponents numerically must be rechecked. These include the depth guard for the recursive layers, the bound on the simultaneous-layer exponent $\lambda'$, and the requirement that the auxiliary gate counts fit in $p + 3$ bits. Reusing the $2^{-182}$ proofs verbatim fails wherever they rely on $d \le b^{2^{-75}}$ or $K \le d^{2^{-56}}$ specifically.

Formalization scope

All statements use the Mathlib environment of the campaign (0df444a, Lean v4.33.1) and the machine model IntMul_MultitapeModel: a fixed finite alphabet and state set, $k \ge 2$ one-way infinite tapes, a read-only input tape, and exact output $\mathrm{bin}_{2n}(\mathrm{val}(x)\mathrm{val}(y))$. Real powers are Real.rpow. $L(n) = \max(\lceil\log_2 n\rceil, 1)$ is IntMul.lg.

The machine milestone quantifies over one machine for all lengths. A machine that hard-codes answers for finitely many lengths still has to be correct everywhere and to meet the time bound for all large $n$, so no finite table trivializes it. The polylogarithmic factor $(\log L(n)+1)^A$ in milestones 4 and 5 matches the manuscript's statement that the slack $2\kappa$ "covers any remaining fixed power of $\log p$". It does not weaken the goal.

Contributions are welcome at every level: proofs of milestones 1 to 4, a parametric version of the Glue, KFM and KFV parameter lemmas, and sketches that split milestone 5 into the phases of the $2^{-182}$ machine.

Selected references

• D. Harvey and J. van der Hoeven, Integer multiplication in time $O(n\log n)$, Annals of Mathematics 193 (2021). https://doi.org/10.4007/annals.2021.193.2.4
• OpenAI, Integer multiplication below $n\log n$, preprint, September 2026, §8 (Table 1, equation (fixed-parameters), margin list). https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Integer-multiplication-below-n-log-n-September-23-2026
• D. Colkitt et al., integer-mult-bounds, patch frozen-154. https://github.com/CrocSwap/integer-mult-bounds/blob/main/patches/frozen-154.patch
• Prove2me, NLogN.KFTop.kappa_bound and IntMul.OpenAI.Glue.kappaBound_of_machine (the formalized $2^{-182}$ development).