Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Karatsuba–Ofman: multiplication in time O(nlog⁡23)O(n^{\log_2 3})O(nlog2​3) on a multitape Turing machine

Proved
IntMul.TM.karatsuba

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

complexity-theoryinteger-multiplicationturing-machines

Karatsuba–Ofman multiplication. There is a single 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\cdot\operatorname{val}y)bin2n​(valx⋅valy), and whose worst-case running time on nnn-bit inputs is

O(nlog⁡23)≈O(n1.585).O\big(n^{\log_2 3}\big)\approx O(n^{1.585}).O(nlog2​3)≈O(n1.585).

The algorithm splits each operand into two halves and replaces four half-size products by three, giving the recurrence M(n)≤3M(⌈n/2⌉+1)+O(n)\mathsf M(n)\le3\mathsf M(\lceil n/2\rceil+1)+O(n)M(n)≤3M(⌈n/2⌉+1)+O(n).

Formalization Note The machine model is the shared IntMul_MultitapeModel (Montanaro's kkk-tape conventions: read-only input tape, output tape, ▹\triangleright▹ only in cell 000, START≠HALT\mathrm{START}\ne\mathrm{HALT}START=HALT, frozen halting state). O(⋅)O(\cdot)O(⋅) means a bound c g(n)c\,g(n)cg(n) for all n≥n0n\ge n_0n≥n0​, with c>0c>0c>0 and n0n_0n0​ depending only on the machine; sizes 1≤n<n01\le n<n_01≤n<n0​ need only correctness.

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

theorem karatsuba : MulTimeBound fun n => (n : ℝ) ^ Real.logb 2 3 := by sorry

end IntMul.TM
Source
A. Karatsuba, Yu. Ofman, Multiplication of multidigit numbers on automata, Soviet Physics Doklady 7 (1963), 595–596; see also Brent–Zimmermann, Modern Computer Arithmetic (2011), §1.3.2.
Read-back

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

Theorem IntMul.TM.karatsuba. Let

g(n)=nlog⁡23(n∈N),g(n) = n^{\log_2 3} \qquad (n \in \mathbb N),g(n)=nlog2​3(n∈N),

where the exponent is the real number log⁡23=ln⁡3/ln⁡2≈1.585\log_2 3 = \ln 3/\ln 2 \approx 1.585log2​3=ln3/ln2≈1.585 and the power is the real power function (for n≥1n \ge 1n≥1 the base is positive, so this is the ordinary value e(log⁡23)ln⁡ne^{(\log_2 3)\ln n}e(log2​3)lnn). The theorem asserts that there exists a deterministic multitape Turing machine MMM such that:

  1. (Correctness for every n≥1n \ge 1n≥1.) For every n≥1n \ge 1n≥1 and all bit strings x,y∈{0,1}nx, y \in \{0,1\}^nx,y∈{0,1}n (leading zeros allowed), MMM started on input x#yx\#yx#y halts after finitely many steps with output bin2n(val(x)⋅val(y))\mathrm{bin}_{2n}(\mathrm{val}(x)\cdot \mathrm{val}(y))bin2n​(val(x)⋅val(y)) (no time bound required in this clause).
  2. (Time bound.) There exist a real constant c>0c > 0c>0 and a threshold n0∈Nn_0 \in \mathbb Nn0​∈N (both chosen after MMM, independent of n,x,yn, x, yn,x,y) such that for every nnn with n≥n0n \ge n_0n≥n0​ and n≥1n \ge 1n≥1 and all x,y∈{0,1}nx, y \in \{0,1\}^nx,y∈{0,1}n, MMM on input x#yx\#yx#y reaches the halting state with that output within some t≤c g(n)t \le c\, g(n)t≤cg(n) steps.

Definitions unfolded. val(x)=∑ixi2∣x∣−1−i\mathrm{val}(x) = \sum_{i} x_i 2^{|x|-1-i}val(x)=∑i​xi​2∣x∣−1−i reads xxx as binary with the first (leftmost) bit most significant; val(ε)=0\mathrm{val}(\varepsilon)=0val(ε)=0. bin2n(z)\mathrm{bin}_{2n}(z)bin2n​(z) is the length-2n2n2n list whose iii-th entry (i=0,…,2n−1i = 0,\dots,2n-1i=0,…,2n−1) is bit number 2n−1−i2n-1-i2n−1−i of zzz, i.e. zzz written MSB-first, left-padded with zeros to exactly 2n2n2n bits; since val(x)val(y)<22n\mathrm{val}(x)\mathrm{val}(y) < 2^{2n}val(x)val(y)<22n this is the exact product. "Started on input x#yx\#yx#y" means: state qstartq_{\mathrm{start}}qstart​, tape 000 holds ▹ x # y □□⋯\triangleright\, x\, \#\, y\, \square\square\cdots▹x#y□□⋯ (bits as symbols 0/1\mathtt 0/\mathtt 10/1), every other tape ▹□□⋯\triangleright\square\square\cdots▹□□⋯, all heads at cell 000. "Halts with output www at step ttt" means: after exactly ttt steps the state is qhaltq_{\mathrm{halt}}qhalt​ and the whole output tape (tape 111) is ▹ w □□⋯\triangleright\, w\, \square\square\cdots▹w□□⋯ — no other non-blank cells; work tapes and head positions are unconstrained. Since qhaltq_{\mathrm{halt}}qhalt​ freezes the configuration, "some t≤Tt \le Tt≤T" is the same as halting within TTT steps. The machine model: finite alphabet containing pairwise distinct □,▹,0,1,#\square, \triangleright, \mathtt 0, \mathtt 1, \#□,▹,0,1,# (plus any extra symbols), finite state set with qstart≠qhaltq_{\mathrm{start}} \ne q_{\mathrm{halt}}qstart​=qhalt​, k≥2k \ge 2k≥2 one-way-infinite tapes (tape 000 input, read-only; tape 111 output; the rest work tapes; kkk fixed by MMM), ▹\triangleright▹ only in cell 000 and never moved left from, one step = simultaneous write/move on all tapes.

Edge cases. n=0n = 0n=0 (input "#\##") is not constrained at all. Inputs with ∣x∣≠∣y∣|x| \ne |y|∣x∣=∣y∣, or not of the form x#yx\#yx#y, are not constrained. g(n)≥1>0g(n) \ge 1 > 0g(n)≥1>0 for all n≥1n \ge 1n≥1, so no degenerate values arise. Small n<n0n < n_0n<n0​ are covered only by the untimed correctness clause. The statement concerns a single machine for all nnn (uniform), with only a big-OOO (eventual, constant-factor) bound — no explicit constant.

Human review
  • Endorsed by Shuze Chen · Oct 9, 2026

    Confirmed by the moderator at approval.

  • Endorsed by avi · Oct 9, 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