| $1$ | [[CLLZ2025](#CLLZ2025)] | Current best general upper bound. [CLLZ2025-ub-1] || $1$ | [[CLLZ2025](#CLLZ2025)] | Current best general upper bound. <a href="#CLLZ2025-ub-1">[CLLZ2025-ub-1]</a> || $0.321334$ | [[WXXZ2024](#WXXZ2024)] | Current best published lower bound. [WXXZ2024-alpha-0321334] || $0.321334$ | [[WXXZ2024](#WXXZ2024)] | Current best published lower bound. <a href="#WXXZ2024-alpha-0321334">[WXXZ2024-alpha-0321334]</a> |Family 107, “Matrix multiplication with exponent at most 9/4”, claims that the dual matrix multiplication exponent α is greater than 93/200 = 0.465 over the complex numbers.
Its Lean statement, MatrixMultiplication.lean:
theorem complex_alpha_gt_93_div_200 :
(93 : ℝ) / 200 < Arithmetic.complexAlphaSame quantity: the file defines α as the supremum of the k in [0, 1] for which multiplying an n × n^k matrix by an n^k × n matrix has exponent 2. Leaving out k > 1 changes nothing, since the exponent is then above 2. 0.465 is above this constant's last-listed lower-bound row.
Status: a Lean statement of it is published with a proof by its authors. We read the statement and it matches this constant's definition; we have not compiled the proof, and we have not read the paper.
Bounds Ledger — Dual matrix multiplication exponent (15b)
upper bound: $1$ (tracked since 2026-07-24 — no movement seen yet)
lower bound: $0.321334$ (tracked since 2026-07-24 — no movement seen yet)
Mirrored from teorth/optimizationproblems@2c1968c. These are the last-listed rows of that constant's bounds table — a listing position, not a statement that this bound is the strongest or most recent. A snapshot at that sha, not a live read.
https://u00dxk2.github.io/bounds-ledger/c/15b.html