Motivation

The matrix-multiplication exponent measures how the arithmetic complexity of multiplying square matrices grows with the ir dimension. Known upper bounds come from constructing large independent matrix products inside tensor powers whose asymptotic rank is controlled. Improving the extraction, rather than finding a lower-rank starting tensor, has driven several recent advances.

Alman, Duan, Vassilevska Williams, Xu, Xu, and Zhou improve the combination-loss analysis by allowing all three variable directions to be treated differently. Their original fourth-power computation gives the bound $\omega<2.371339$. The mission targets the slightly weaker rational endpoint $2.37134$, keeping the historical result distinct from the later AlphaEvolve numerical improvement incorporated into the latest manuscript. More Asymmetry Yields Faster Matrix Multiplication, version 2, SODA 2025.

Setting

Fix an arbitrary field $K$. The matrix-multiplication tensor $\langle a,b,c\rangle_K$ represents multiplication of an $a\times b$ matrix by a $b\times c$ matrix. A tensor's rank is the least number of pure tensors summing to it. The existing Lean definition matMulExp K is the infimum of $\log R(\langle n,n,n\rangle_K)/\log n$ for integer dimensions $n\ge2$, with value $3$ at the excluded dimensions $0$ and $1$. This definition, and the existing equivalence with the Strassen-preorder exponent, remain unchanged.

The source tensor is the literal fourth power $T=CW_5^{\otimes4}$ of the Coppersmith–Winograd tensor. The public parenthesization is $(CW_5\otimes CW_5)\otimes(CW_5\otimes CW_5)$. Its asymptotic rank is at most $7^4=2401$. Its canonical coarse components are indexed by triples $(i,j,k)$ with $i+j+k=8$. This is the fourth-power, recursion-level-three specialization described in Section 7, not the eighth-power specialization used by the later optimization note. More Asymmetry, Section 7.

A complete split distribution records frequencies of entire fine-grade words, rather than only the marginal split at the next recursion step. At level $\ell\ge1$, these words have length $2^{\ell-1}$ over the alphabet $\{0,1,2\}$. Three such distributions describe the X-, Y-, and Z-variable blocks. A restricted constituent power keeps only blocks approximately consistent with those distributions, in maximum-coordinate distance at most a specified $\varepsilon\ge0$. An interface tensor is a tensor product of these restricted constituent powers. The approximation tolerance and all three distributions are part of the interface. More Asymmetry, Definitions 3.4–3.6 and 4.1.

Formalization targets

The goal is the unconditional field-uniform statement

$$\forall K\;[\mathrm{Field}(K)],\qquad \operatorname{matMulExp}(K)<\frac{237134}{100000}.$$

Its binders and exponent definition match the existing Schönhage and Stothers goals; only the declaration name and endpoint differ. No optimizer result, characteristic condition, distribution, or assumed value surplus is a hypothesis of the root.

The compact proposal has four milestones and the root, totaling five review items. The milestones concern literal fine-to-coarse source restrictions; the fourth-power rank budget; an actual strict six-symmetrized value surplus at the chosen parameter; and the conditional implication from that surplus to the exponent bound. Existing proved source and rank theorems are reused. The open surplus target contains the new complete-split extraction and exact numerical obligations, which are described separately in the proof outline rather than hidden in an opaque certificate definition.

The chosen internal parameter is $\tau_0=3952233/5000000$, so

$$2.371339<3\tau_0=2.3713398<2.37134.$$

The substantive value target is the existence of a real $V>2401$ such that the actual source has six-symmetrized $\tau_0$-value at least $V$ in the existing finite-witness semantics. The strict slack leaves room to translate limiting extraction rates into strict lower bases. Neither the existence of that surplus nor a completed exact numerical certificate is claimed at proposal time.

Significance

This formalization would capture a new structural improvement, not a re-optimization of the same DWZ square data. Its distinguishing feature is sequentially obtaining the necessary ownership properties for X, then Y, then Z, while preserving more useful fine blocks. The resulting complete-split and interface-tensor theory is also the mathematical foundation for the later AlphaEvolve optimization. More Asymmetry, Sections 2, 4–6; Dupont et al., Section 2.

The known mathematical result is not an open conjecture. The open work is its machine-checked reconstruction. The earlier square and Stothers roots are marked Proved. The newer DWZ fourth-power root has an accepted reduction but remains Open. Its literal fourth source, rank budget, sixfold-symmetry bridge and entropy-certificate infrastructure can be reused independently of that unfinished endpoint. A proof of the numerical DWZ bound alone would not imply the smaller bound targeted here.

Difficulty

The old hashing interface guarantees both coarse X- and Y-block uniqueness. The new method initially requires only coarse X-block uniqueness. Fine Y-block compatibility and usefulness must then establish the ownership needed for the subsequent Z-stage. Applying a theorem whose hypotheses already demand coarse Y uniqueness would discard the new method's essential advantage. Six coordinate permutations create six regions whose parameters and output interfaces must remain consistent. More Asymmetry, Section 4.1 and Figure 1.

Removing incompatible fine blocks creates holes. The relevant repair theorem concerns holes in all three modes and a quantitative supply of broken interface copies. It cannot be replaced without proof by the older square-specific Z-only repair interface. The global and recursive stages also carry subexponential losses and approximation tolerances; their limiting order must be explicit. Numerical feasibility is a separate obligation: floating-point parameters and optimization success are not exact normalization, marginal, entropy, or logarithm proofs. More Asymmetry, Theorem 4.2, Theorems 5.3 and 6.4, and Section 7.

Formalization scope

The environment is pinned to Mathlib 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e and Lean v4.29.0-rc3. The development reuses TensorObj, MMObj, restrictions, degenerations, tensor powers, existing tau-value predicates, and matMulExp. The root is uniform over arbitrary fields. Source relations remain target-first: a restriction of A from B is written Restrict A B. A collection of overlapping constituent restrictions must not be relabeled as an external direct sum.

Complete split distributions, simultaneous three-mode projections, interface tensors, region permutations, and explicit finite extraction maps form reusable infrastructure. Exact rational profiles require compatible lengths; approximate profiles require their stated tolerance and limiting argument. No constant-valued replacement for tensor value, vacuous witness hypothesis, or certificate that merely assumes the desired extraction is admissible.

The authors' released code and parameter archive is the provenance source for the original computation. Versioned archive and witness hashes belong to the companion source audit. The optimization program need not be formalized: an exact certificate checker must establish its own normalization, support, marginal and interval conditions. Contributions to complete-split interfaces, sequential ownership, three-mode repair, recursive extraction, entropy certificates, and finite source-to-exponent bridges all advance this mission.

Selected references

• Josh Alman, Ran Duan, Virginia Vassilevska Williams, Yinzhan Xu, Zixuan Xu, and Renfei Zhou, More Asymmetry Yields Faster Matrix Multiplication, SODA 2025. Pinned version 2.
• Authors' code and parameters for the original fourth-power bounds. OSF release.
• Ran Duan, Hongxun Wu, and Renfei Zhou, Faster Matrix Multiplication via Asymmetric Hashing, FOCS 2023. Version 5.
• Emilien Dupont et al., Improving the matrix multiplication exponent with modern optimization and AlphaEvolve, 2026 preprint. Version 1.