Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Theorem 1.1 in the κ\kappaκ-framework — KappaBound(0)\mathrm{KappaBound}(0)KappaBound(0): multiplication in time O(nlg⁡n)O(n\lg n)O(nlgn)

Open
IntMul.HvdH.theorem_1_1_kappa_zero

by avi · Oct 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplication

Theorem 1.1 of Harvey–van der Hoeven, in the κ\kappaκ-framework. KappaBound(0)\mathrm{KappaBound}(0)KappaBound(0) holds: there is one deterministic multitape Turing machine that, for every n≥1n\ge1n≥1 and all x,y∈{0,1}nx,y\in\{0,1\}^nx,y∈{0,1}n, halts on input x#yx\#yx#y with output bin⁡2n(val⁡(x)val⁡(y))\operatorname{bin}_{2n}(\operatorname{val}(x)\operatorname{val}(y))bin2n​(val(x)val(y)), and whose worst-case running time T(n)T(n)T(n) satisfies

T(n)=O(n(lg⁡n)1−0)=O(nlg⁡n),lg⁡n=max⁡(⌈log⁡2n⌉,1).T(n)=O\big(n(\lg n)^{1-0}\big)=O(n\lg n),\qquad\lg n=\max(\lceil\log_2n\rceil,1).T(n)=O(n(lgn)1−0)=O(nlgn),lgn=max(⌈log2​n⌉,1).

This is the paper's main theorem, written in the same form as the claimed improvements KappaBound(κ)\mathrm{KappaBound}(\kappa)KappaBound(κ) with κ>0\kappa>0κ>0. It is the baseline of that family of bounds.

Formalization Note KappaBound(κ)\mathrm{KappaBound}(\kappa)KappaBound(κ) is defined in IntMul_MultitapeModel, which uses the kkk-tape Turing machine conventions of Montanaro's lecture notes (start symbol, HALT\mathrm{HALT}HALT state, read-only input tape, separate output tape). It asserts a single machine that, for every n≥1n\ge1n≥1 and all x,y∈{0,1}nx,y\in\{0,1\}^nx,y∈{0,1}n, halts on input x#yx\#yx#y with output bin⁡2n(val⁡(x)val⁡(y))\operatorname{bin}_{2n}(\operatorname{val}(x)\operatorname{val}(y))bin2n​(val(x)val(y)), and whose worst-case running time is at most c n(lg⁡n)1−κc\,n(\lg n)^{1-\kappa}cn(lgn)1−κ for all n≥n0n\ge n_0n≥n0​, for some c>0c>0c>0 and n0n_0n0​. Here lg⁡n=max⁡(⌈log⁡2n⌉,1)\lg n=\max(\lceil\log_2n\rceil,1)lgn=max(⌈log2​n⌉,1).

Preamble
import Mathlib
import Definitions.Def_IntMul_MultitapeModel
Formal statement
namespace IntMul.HvdH

theorem theorem_1_1_kappa_zero : KappaBound 0 := by sorry

end IntMul.HvdH
Source
D. Harvey, J. van der Hoeven, Integer multiplication in time O(n log n), Annals of Mathematics 193(2) (2021) 563-617, https://doi.org/10.4007/annals.2021.193.2.4 (preprint https://hal.science/hal-02070778v2), §1, Theorem 1.1, p. 1, restated with lg n = max(ceil(log2 n),1) as in 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, §1
Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back of IntMul.HvdH.theorem_1_1_kappa_zero. The theorem has no hypotheses and no free variables; it asserts the proposition KappaBound(0)\mathrm{KappaBound}(0)KappaBound(0). Unfolding, KappaBound(κ)\mathrm{KappaBound}(\kappa)KappaBound(κ) is "multiplication is possible in time O(g)O(g)O(g)" for the bound function

g(n)  =  n⋅(lg⁡n) 1−κ(n∈N, values in R),g(n) \;=\; n \cdot (\lg n)^{\,1-\kappa} \qquad (n \in \mathbb{N},\ \text{values in } \mathbb{R}),g(n)=n⋅(lgn)1−κ(n∈N, values in R),

where the power is the real power with real exponent. With κ=0\kappa = 0κ=0 the exponent is 1−0=11 - 0 = 11−0=1, and x1=xx^{1} = xx1=x for every real xxx, so the bound function is exactly

g(n)  =  n⋅lg⁡n,lg⁡n  =  max⁡(⌈log⁡2n⌉, 1),g(n) \;=\; n \cdot \lg n, \qquad \lg n \;=\; \max\bigl(\lceil \log_2 n \rceil,\ 1\bigr),g(n)=n⋅lgn,lgn=max(⌈log2​n⌉, 1),

where ⌈log⁡2n⌉\lceil \log_2 n\rceil⌈log2​n⌉ is the natural-number ceiling logarithm (the least eee with n≤2en \le 2^en≤2e; it equals 000 for n≤1n \le 1n≤1). Thus lg⁡1=1\lg 1 = 1lg1=1, lg⁡2=1\lg 2 = 1lg2=1, lg⁡3=lg⁡4=2\lg 3 = \lg 4 = 2lg3=lg4=2, lg⁡5=⋯=lg⁡8=3\lg 5 = \dots = \lg 8 = 3lg5=⋯=lg8=3, and so on; in particular lg⁡n≥1\lg n \ge 1lgn≥1 always, and g(1)=1g(1) = 1g(1)=1, g(2)=2g(2) = 2g(2)=2, g(3)=6g(3) = 6g(3)=6, g(4)=8g(4) = 8g(4)=8.

The statement. There exists a deterministic multitape Turing machine MMM (model described below) such that both of the following hold:

  1. Correctness / totality on every length n≥1n \ge 1n≥1: for every natural number n≥1n \ge 1n≥1 there is some real number TTT such that MMM multiplies nnn-bit integers within TTT steps (definition below). Since TTT is arbitrary, this just says: for every n≥1n \ge 1n≥1 and every pair of nnn-bit strings, MMM halts after finitely many steps with the correct output.
  2. Time bound: there exist a real constant c>0c > 0c>0 and a natural number n0n_0n0​ such that for every natural number nnn with n≥n0n \ge n_0n≥n0​ and n≥1n \ge 1n≥1, MMM multiplies nnn-bit integers within c⋅n⋅lg⁡nc \cdot n \cdot \lg nc⋅n⋅lgn steps.

Nothing is required for input length n=0n = 0n=0 (both clauses exclude it), and nothing is required of MMM on inputs whose two halves have different lengths, or on any input not of the form described below. The constant n0n_0n0​ may be 000; the clause n≥1n \ge 1n≥1 is imposed separately. No explicit value of ccc or n0n_0n0​ is asserted.

"MMM multiplies nnn-bit integers within TTT steps" (for T∈RT \in \mathbb{R}T∈R) means: for all bit strings x,y∈{0,1}∗x, y \in \{0,1\}^*x,y∈{0,1}∗ with ∣x∣=n|x| = n∣x∣=n and ∣y∣=n|y| = n∣y∣=n, there is a natural number ttt with t≤Tt \le Tt≤T (compared as reals) such that after exactly ttt steps from the initial configuration on input x#yx\#yx#y:

  • the state of MMM is HALT\mathrm{HALT}HALT, and
  • the output tape (tape 111) holds exactly ▹ w1w2⋯w2n □ □⋯\triangleright\, w_1 w_2 \cdots w_{2n}\, \square\, \square \cdots▹w1​w2​⋯w2n​□□⋯, i.e. ▹\triangleright▹ in cell 000, the bit-symbols of www in cells 1,…,2n1,\dots,2n1,…,2n, and the blank □\square□ in every cell after 2n2n2n, where
w  =  bin2n(val(x)⋅val(y)).w \;=\; \mathrm{bin}_{2n}\bigl(\mathrm{val}(x)\cdot \mathrm{val}(y)\bigr).w=bin2n​(val(x)⋅val(y)).

Here val(x)=∑i=1∣x∣xi 2∣x∣−i\mathrm{val}(x) = \sum_{i=1}^{|x|} x_i\, 2^{|x|-i}val(x)=∑i=1∣x∣​xi​2∣x∣−i reads xxx as a binary numeral with the leftmost bit most significant (val\mathrm{val}val of the empty string is 000), and bink(z)\mathrm{bin}_{k}(z)bink​(z) is the list of kkk bits whose iii-th entry (i=0,…,k−1i = 0,\dots,k-1i=0,…,k−1) is bit number k−1−ik-1-ik−1−i of zzz, i.e. the binary representation of zzz most significant bit first, left-padded with zeros to length exactly kkk (higher bits of zzz, if any, are dropped). Since val(x),val(y)<2n\mathrm{val}(x), \mathrm{val}(y) < 2^nval(x),val(y)<2n, the product is <22n< 2^{2n}<22n, so www is exactly the product written in 2n2n2n bits with leading zeros. Inputs x,yx, yx,y may have leading zeros (any nnn-bit strings, including all-zero ones). Bits are written as the symbols 0↦00 \mapsto \mathtt{0}0↦0, 1↦11 \mapsto \mathtt{1}1↦1. Because the halting state freezes the configuration, "halted with the right output at some t≤Tt \le Tt≤T" is the same as "halts within at most TTT steps, with that output". The contents of the input tape and work tapes at halting are unconstrained.

The machine model. A machine MMM consists of:

  • a finite alphabet Σ\SigmaΣ containing five pairwise distinct designated symbols: blank □\square□, start symbol ▹\triangleright▹, bit symbols 0,1\mathtt{0}, \mathtt{1}0,1, and separator #\## (it may contain arbitrarily many further symbols);
  • a finite set of states KKK with designated states START≠HALT\mathrm{START} \ne \mathrm{HALT}START=HALT;
  • a number of tapes k≥2k \ge 2k≥2 (any fixed kkk, chosen with the machine): tape 000 is the input tape, tape 111 the output tape, tapes 2,…,k−12,\dots,k-12,…,k−1 work tapes; each tape has cells indexed by 0,1,2,…0,1,2,\dots0,1,2,…;
  • a transition function δ:K×Σk→K×(Σ×{←,−,→})k\delta : K \times \Sigma^k \to K \times (\Sigma \times \{\leftarrow, -, \rightarrow\})^kδ:K×Σk→K×(Σ×{←,−,→})k satisfying: (i) whenever the scanned symbol on tape iii is ▹\triangleright▹, it is rewritten as ▹\triangleright▹ and the head on tape iii does not move left; (ii) whenever the scanned symbol on tape iii is not ▹\triangleright▹, the symbol written there is not ▹\triangleright▹; (iii) δ(HALT,a)=(HALT,(ai,−)i)\delta(\mathrm{HALT}, a) = (\mathrm{HALT}, (a_i, -)_i)δ(HALT,a)=(HALT,(ai​,−)i​) for every scanned tuple aaa, so a halted configuration never changes; (iv) the symbol written on tape 000 always equals the symbol scanned there (the input tape is read-only).

A configuration is a state, the contents of every cell of every tape, and a head position ∈N\in \mathbb{N}∈N on each tape. One step reads the scanned symbols a=(ai)ia = (a_i)_ia=(ai​)i​, computes δ(q,a)=(q′,(σi,di)i)\delta(q, a) = (q', (\sigma_i, d_i)_i)δ(q,a)=(q′,(σi​,di​)i​), overwrites each scanned cell with σi\sigma_iσi​, moves each head left/stays/right according to did_idi​ (moving left from position ppp gives p−1p - 1p−1 with truncated natural-number subtraction, though by (i) and the fact that ▹\triangleright▹ sits only in cell 000 a head never actually moves left from cell 000), and sets the state to q′q'q′. The initial configuration on input x#yx\#yx#y has state START\mathrm{START}START, every head on cell 000, the input tape holding ▹ x1⋯xn # y1⋯yn □ □⋯\triangleright\, x_1\cdots x_n\, \#\, y_1 \cdots y_n\, \square\,\square\cdots▹x1​⋯xn​#y1​⋯yn​□□⋯ (bit symbols for the bits), and every other tape holding ▹ □ □⋯\triangleright\,\square\,\square\cdots▹□□⋯. Each step counts as one unit of time; there is no bound on the number of tapes, states, alphabet size, or space used, beyond their being fixed and finite for the single machine MMM, which must work uniformly for all nnn.

In summary, the theorem asserts: there is a single deterministic multitape Turing machine (in the above model) that, for every n≥1n \ge 1n≥1 and all x,y∈{0,1}nx, y \in \{0,1\}^nx,y∈{0,1}n, halts on input x#yx\#yx#y with output tape exactly ▹ bin2n(val(x)val(y)) □□⋯\triangleright\,\mathrm{bin}_{2n}(\mathrm{val}(x)\mathrm{val}(y))\,\square\square\cdots▹bin2n​(val(x)val(y))□□⋯, and there are c>0c > 0c>0 and n0n_0n0​ such that for all n≥max⁡(n0,1)n \ge \max(n_0, 1)n≥max(n0​,1) it does so within at most c⋅n⋅max⁡(⌈log⁡2n⌉,1)c \cdot n \cdot \max(\lceil \log_2 n\rceil, 1)c⋅n⋅max(⌈log2​n⌉,1) steps on every such input — i.e. integer multiplication in time O(nlg⁡n)O(n \lg n)O(nlgn) on this model.

Human review
  • Endorsed by wurtle · Oct 8, 2026

    Confirmed by the moderator at approval.

  • Endorsed by avi · Oct 8, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me