Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Jain round six — multiplication in time O(n(lg⁡n)1−κ)O(n(\lg n)^{1-\kappa})O(n(lgn)1−κ), κ=3666565558019/1017>2−15\kappa=3666565558019/10^{17}>2^{-15}κ=3666565558019/1017>2−15

Open
IntMul.Kappa.jain_round6

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

complexity-theoryinteger-multiplication

Jain's round-six witness. In the fixed finite-alphabet Turing-machine model with a fixed number of one-dimensional tapes, two nnn-bit integers can be multiplied exactly in time

T(n)=O(n(lg⁡n)1−κ),κ=36665655580191017≈3.66657×10−5>2−15.T(n)=O\big(n(\lg n)^{1-\kappa}\big),\qquad\kappa=\frac{3666565558019}{10^{17}}\approx3.66657\times10^{-5}>2^{-15}.T(n)=O(n(lgn)1−κ),κ=10173666565558019​≈3.66657×10−5>2−15.

This is the strongest exponent saving claimed so far in the line of work started by the OpenAI preprint. It combines copied retained centres, retained point totals and a two-stage complex interchange with the networks and parameter assembly of the earlier drafts. The project states that the claim is conditional on the OpenAI manuscript and on Colkitt's framework, and has not had independent review. Its moment certificates and parameter assembly are checked in the Lean kernel, with the analytic inequalities they rely on taken as premises.

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.Kappa

theorem jain_round6 : KappaBound (3666565558019 / 10 ^ 17) := by sorry

end IntMul.Kappa
Source
S. Jain, Integer multiplication: a conditional witness above 2^-15 (integer-mult-kappa), research draft, https://github.com/Swapnil-jain/integer-mult-kappa (README headline, Round six; scripts/certificate_round6.py, lean/Round6.lean; commit f2176bc), stated as conditional on 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 and on D. Colkitt, https://github.com/CrocSwap/integer-mult-bounds
Read-back

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

Claim. There is a deterministic multitape Turing machine that multiplies nnn-bit integers in time O(n (lg⁡n)1−κ)O\big(n\,(\lg n)^{1-\kappa}\big)O(n(lgn)1−κ). Here κ\kappaκ is the exact real number

κ  =  36665655580191017  =  0.00003666565558019  ≈  3.6666×10−5,\kappa \;=\; \frac{3666565558019}{10^{17}} \;=\; 0.00003666565558019 \;\approx\; 3.6666\times 10^{-5},κ=10173666565558019​=0.00003666565558019≈3.6666×10−5,

so the exponent is exactly 1−κ=0.999963334344419811-\kappa = 0.999963334344419811−κ=0.99996333434441981. The power (lg⁡n)1−κ(\lg n)^{1-\kappa}(lgn)1−κ is the real power function, and it is always applied to a base ≥1\ge 1≥1. The theorem has no hypotheses or free variables. All of its content sits in the definitions below, which are unfolded here.

Logarithm. For a natural number nnn, define lg⁡n=max⁡(⌈log⁡2n⌉,1)\lg n = \max(\lceil \log_2 n\rceil, 1)lgn=max(⌈log2​n⌉,1). Here ⌈log⁡2n⌉\lceil\log_2 n\rceil⌈log2​n⌉ is the least j∈Nj\in\mathbb Nj∈N with n≤2jn \le 2^jn≤2j, which is 000 for n∈{0,1}n\in\{0,1\}n∈{0,1}. So lg⁡1=lg⁡2=1\lg 1 = \lg 2 = 1lg1=lg2=1, lg⁡3=lg⁡4=2\lg 3=\lg 4 = 2lg3=lg4=2, lg⁡5=3\lg 5 = 3lg5=3, and so on. Always lg⁡n≥1\lg n \ge 1lgn≥1. The bounding function is

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

Machine model. A machine MMM consists of the following data:

  • a finite alphabet Σ\SigmaΣ containing five pairwise distinct symbols: blank □\square□, start symbol ▹\triangleright▹, and the symbols 000, 111 and #\##;
  • a finite state set KKK with a start state qstartq_{\mathrm{start}}qstart​ and a halting state qhalt≠qstartq_{\mathrm{halt}}\neq q_{\mathrm{start}}qhalt​=qstart​;
  • a number of tapes k≥2k\ge 2k≥2, where tape 000 is the input tape, tape 111 is the output tape, and the rest are work tapes;
  • a transition function δ:K×Σk→K×(Σ×{←,−,→})k\delta: K\times\Sigma^k\to K\times(\Sigma\times\{\leftarrow,-,\rightarrow\})^kδ:K×Σk→K×(Σ×{←,−,→})k.

The transition function must satisfy four constraints:

  1. Start symbol. Whenever tape iii scans ▹\triangleright▹, it writes ▹\triangleright▹ back and does not move left.
  2. No new start symbols. Whenever tape iii scans a symbol other than ▹\triangleright▹, it does not write ▹\triangleright▹.
  3. Halting freezes. In state qhaltq_{\mathrm{halt}}qhalt​, δ\deltaδ keeps the state qhaltq_{\mathrm{halt}}qhalt​, rewrites every scanned symbol unchanged and moves no head. The configuration is therefore frozen from then on.
  4. Read-only input. On tape 000, the written symbol always equals the scanned symbol. The input head may still move.

A configuration consists of a state, a content function N→Σ\mathbb N\to\SigmaN→Σ for each tape (cells 0,1,2,…0,1,2,\dots0,1,2,…, infinite to the right only) and a head position in N\mathbb NN for each tape. One step works as follows. Apply δ\deltaδ to the current state and the kkk scanned symbols. Overwrite each scanned cell with the prescribed symbol. Move each head by −1-1−1, 000 or +1+1+1. A move of −1-1−1 uses truncated subtraction, so position 000 would stay at 000, but constraint 1 already rules this out at cell 000. Finally, adopt the new state.

Encodings. For a bit string x=x1⋯xmx=x_1\cdots x_mx=x1​⋯xm​, write val(x)=∑ixi2m−i\mathrm{val}(x)=\sum_i x_i 2^{m-i}val(x)=∑i​xi​2m−i, with the most significant bit first and val(empty)=0\mathrm{val}(\text{empty})=0val(empty)=0. For naturals ℓ,z\ell, zℓ,z, the string binℓ(z)\mathrm{bin}_\ell(z)binℓ​(z) has length exactly ℓ\ellℓ, and its iii-th entry is bit ℓ−1−i\ell-1-iℓ−1−i of zzz, for i=0,…,ℓ−1i=0,\dots,\ell-1i=0,…,ℓ−1. So it is zzz written in binary, most significant bit first, left-padded with zeros, and truncated to the low ℓ\ellℓ bits if z≥2ℓz\ge 2^\ellz≥2ℓ.

On input (x,y)(x,y)(x,y), the initial configuration is as follows:

  • the state is qstartq_{\mathrm{start}}qstart​;
  • tape 000 holds ▹ x # y □□⋯\triangleright\, x\,\#\, y\,\square\square\cdots▹x#y□□⋯, with each bit written as the symbol 000 or 111;
  • every other tape holds ▹ □□⋯\triangleright\,\square\square\cdots▹□□⋯;
  • all heads are on cell 000.

"MMM halts with output www at time ttt" means this: after exactly ttt steps from that configuration, the state is qhaltq_{\mathrm{halt}}qhalt​, and the entire output tape equals ▹ w □□⋯\triangleright\, w\,\square\square\cdots▹w□□⋯. That is, cell 000 holds ▹\triangleright▹, cells 1,…,∣w∣1,\dots,|w|1,…,∣w∣ hold the bits of www, and every later cell is blank. The work tapes and head positions are unconstrained. Because halting freezes the configuration, this is equivalent to MMM having halted by step ttt with that output tape.

Multiplying at a given length. For n∈Nn\in\mathbb Nn∈N and a real number TTT, "MMM multiplies at length nnn within TTT" means the following. For all bit strings x,yx,yx,y of length exactly nnn, leading zeros allowed, there is a t∈Nt\in\mathbb Nt∈N with t≤Tt\le Tt≤T such that MMM on input (x,y)(x,y)(x,y) halts at time ttt with output

bin2n(val(x)⋅val(y)).\mathrm{bin}_{2n}\big(\mathrm{val}(x)\cdot\mathrm{val}(y)\big).bin2n​(val(x)⋅val(y)).

Since val(x) val(y)<22n\mathrm{val}(x)\,\mathrm{val}(y)<2^{2n}val(x)val(y)<22n, this is the exact product, written with exactly 2n2n2n bits.

Full statement. There exists a machine MMM, as above, satisfying two conditions:

  1. Correctness. For every n≥1n\ge 1n≥1 there is some real TTT such that MMM multiplies at length nnn within TTT. In other words, MMM correctly multiplies every pair of equal-length inputs of positive length, with no time constraint.
  2. Time bound. There exist a real constant c>0c>0c>0 and a threshold n0∈Nn_0\in\mathbb Nn0​∈N such that, for every nnn with n≥n0n\ge n_0n≥n0​ and n≥1n\ge 1n≥1,
M multiplies at length n within c⋅n⋅(lg⁡n)1−κ.M \text{ multiplies at length } n \text{ within } c\cdot n\cdot(\lg n)^{1-\kappa}.M multiplies at length n within c⋅n⋅(lgn)1−κ.

Edge cases and scope.

  • Length n=0n=0n=0 is never constrained.
  • Nothing is required on inputs where xxx and yyy have different lengths, or on tape contents not of the form ▹ x#y\triangleright\,x\#y▹x#y.
  • There is no additive constant in the bound: for n≥n0n\ge n_0n≥n0​, the step count itself must be at most c g(n)c\,g(n)cg(n).
  • The alphabet size, number of states and number of tapes k≥2k\ge 2k≥2 are arbitrary but fixed for the one machine MMM, which must work for all lengths nnn.
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