Motivation

The matrix-multiplication exponent measures how the arithmetic cost of multiplying square matrices grows with their dimension. An improvement in this exponent is relevant both to algebraic complexity and to algorithms whose running times depend on matrix multiplication. This mission formalizes a known improvement using the fourth power of the Coppersmith–Winograd tensor; it does not claim a new mathematical record.

Duan, Wu, and Zhou identify a loss that arises when constituent tensors are analyzed independently although some of their finer components can coexist inside a shared variable block. Their asymmetric-hashing method recovers part of this combination loss. The paper's headline result concerns the eighth power. Its separate fourth-power computation reports $2.371919$ in Table 3, printed page 78. The present target is the slightly weaker exact rational endpoint $2.37193$. Duan–Wu–Zhou, Faster Matrix Multiplication via Asymmetric Hashing.

Setting

Fix an arbitrary field $K$. The matrix-multiplication tensor $\langle a,b,c\rangle_K$ encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix. Its tensor rank is the smallest number of pure tensors whose sum is that tensor. The existing Lean definition matMulExp K takes the infimum of $\log R(\langle n,n,n\rangle_K)/\log n$ over integers $n\ge2$, with the value $3$ at the two excluded small dimensions. This definition is reused without alteration.

A restriction applies a linear map separately to each of a tensor's three variable spaces. A degeneration allows polynomial families of such maps and takes an appropriate leading coefficient. The order of the Lean relation is target first: Restrict A B means that $A$ is obtained from $B$. A direct sum uses disjoint variable spaces; a collection of overlapping restrictions does not constitute a direct sum.

The Coppersmith–Winograd tensor $CW_q$ has border rank at most $q+2$. This mission fixes $q=5$ and uses the literal tensor $T=(CW_5\otimes CW_5)\otimes(CW_5\otimes CW_5)$, whose asymptotic-rank budget is $7^4=2401$. Its standard coordinate partition has 45 coarse components $T_{ijk}$ indexed by nonnegative integers $i+j+k=8$. Each coarse component consists of ordered products of square components, whose grades sum to $(i,j,k)$. Duan–Wu–Zhou, Sections 3 and 6–8.

A restricted-splitting value pair consists of a lower value bound and a prescribed distribution on finer Z-variable blocks. In a tensor power, Z-blocks with the wrong empirical split distribution are removed before measuring value. Sixfold symmetrization, using all permutations of the three modes, is part of this definition. Keeping the scalar and discarding the prescribed distribution loses information required by the recursion. Duan–Wu–Zhou, Definition 3.9, Equation (3), and Definition 8.1.

Formalization targets

The goal is precisely

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

It has the same field quantification and exponent definition as the completed Schönhage and Stothers goals. Only the name and rational endpoint change. No distribution, optimizer, characteristic restriction, or unproved value bound is a hypothesis of this goal.

The supporting targets concern the literal fourth-power source; prescribed-splitting component values; the recursive and global extraction inequalities of Equations (34) and (25); an exact certificate for the released fourth-power computation; and the value-to-exponent implication of Theorem 3.2. The proof outline distinguishes stable formal statements from source-level tasks whose complete Lean interfaces still require development. It does not turn an unspecified certificate into an assumption that the desired extraction exists.

The compact milestone list contains four precise statements: the literal fine-to-coarse product restriction; the fourth-power asymptotic-rank bound; existence of a strict six-symmetrized value surplus; and the conditional implication from that surplus to the goal. Together with the root, these are five review items. The first, second, and fourth milestones are marked Proved. The surplus remains Open. An accepted root reduction links the surplus to the proved capstone; it is a proof sketch, not a proof of the exponent bound. Recursive component extraction and exact numerical certification remain substantial work inside that open target.

The planned internal parameter is $\tau=790643/1000000$. Thus $3\tau=2.371929<2.37193$. The substantive value obligation is a strict surplus over $2401$ for the actual fourth-power source, with asymptotic losses absorbed by choosing strict lower rates. The exact certificate must establish this surplus; neither its existence nor its numerical slack is presently claimed as proved.

Significance

The result would extend the formalized Stothers endpoint $2.3737$ to an asymmetric fourth-power bound. More importantly, it would provide restricted-splitting interfaces that can support subsequent higher-power and more-asymmetric analyses. The mathematical improvement is already established in the cited paper. The task here is to reconstruct its argument with machine-checked statements, concrete tensor maps, and exact numerical bounds.

The earlier square and Stothers mission roots are marked Proved. Reusable infrastructure includes polynomial degenerations, tensor powers, direct-sum value witnesses, hashing and hole-repair lemmas, the literal fourth-power grading, and the final exponent bridge. Two additional literal fourth-power support/restriction bridges and an additive entropy certificate with directed-log inputs are also marked Proved. These statuses do not imply that the new restricted-value recursion or numerical witness is already formalized.

Difficulty

The central difficulty is retaining the correct dependence between each value bound and its prescribed split distribution. The released fourth-power data contains consumer-specific copies of square value pairs. Equal coarse grades do not justify identifying their chosen distributions. The 21 positive fourth-power components use the six-region recursion, whereas the 24 components with a zero coordinate require the boundary merging argument. Duan–Wu–Zhou, Equation (34), Section 7.3, and released implementation.

Global hashing must additionally control competitors with the same marginals, shared Z-blocks, missing fine blocks, and subexponential losses. An isolated restriction into each constituent is insufficient to establish a simultaneous extraction. Numerical optimization presents a separate issue: floating-point normalization and approximate maximum-entropy computations are not exact feasibility or entropy proofs. Exact marginal constraints, positivity domains, and directed error bounds must all be checked.

Formalization scope

The environment is pinned to Mathlib 777aaa61dcd2a1258d2b4962dbe983ede4d23b2e and Lean v4.29.0-rc3. The development reuses TensorObj, MMObj, Degenerates, HasTauValueAtLeast, the six-symmetrized value infrastructure, and matMulExp. All endpoint theorems remain uniform over arbitrary fields. Finite profiles use exact integer counts; rational distributions must have compatible unbounded lengths before an asymptotic statement is invoked. Real limiting rates are represented with explicit strict slack where the existing finite-witness predicate does not guarantee endpoint attainment.

No constant-valued replacement for tensor value, opaque witness carrying its desired conclusion, or external direct sum substituted for overlapping source blocks is admissible. New definitions must specify the actual coordinate projections and restrictions they represent. The authors' optimizer is used to find candidate data, not trusted as a proof oracle. Contributions to restricted-power semantics, consumer-specific square pairs, boundary merging, recursive extraction, exact entropy bounds, and source-to-exponent bridges are all directly relevant to the goal.

Selected references

• Ran Duan, Hongxun Wu, and Renfei Zhou, Faster Matrix Multiplication via Asymmetric Hashing, FOCS 2023. Full paper, version 5.
• Duan–Wu–Zhou, accompanying optimization and verification code, including power4_dup_2.371919.mat. Authors' release.
• A. M. Davie and A. J. Stothers, Improved Bound for Complexity of Matrix Multiplication, Proceedings of the Royal Society of Edinburgh Section A 143(2), 2013. DOI.
• Arnold Schönhage, Partial and Total Matrix Multiplication, SIAM Journal on Computing 10(3), 1981. DOI.