Davie--Stothers fourth-power bound: omega < 2.3737

Open

mme_omega_lt_23737

by marwahaha · Aug 29, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

algebraic-complexitycoppersmith-winogradlaser-methodmatrix-multiplication

Let $K$ be an arbitrary field and let $\omega(K)$ denote the exponent of square matrix multiplication over $K$ . Then

\omega(K)<\frac{23737}{10000}=2.3737.

This is a strict exact-rational consequence of the Davie--Stothers fourth-power analysis, which reports the stronger numerical endpoint $2.373689703$ . The theorem is the historical first improvement obtained by passing from the square to the fourth power of the Coppersmith--Winograd tensor.

Formalization Note The statement uses the established field-uniform matMulExp definition and imposes no characteristic restriction on $K$ .

Preamble

import Definitions.Def_mme_omega

universe u

open MME

set_option autoImplicit false

Formal statement

theorem mme_omega_lt_23737 {K : Type u} [Field K] :
    matMulExp K < 23737 / 10000 := by sorry

Source

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, Theorem 5.3 and Table 2, printed pp. 367-368; https://www.maths.ed.ac.uk/~sandy/a11164.pdf; DOI 10.1017/S0308210511001646.

Read-back

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

Blind read-back of Goal.lean

mme_omega_lt_23737

For every universe level $u$ and every type $K : \mathrm{Type}\,u$ equipped with a field structure, the imported quantity $\mathrm{matMulExp}(K)$ is strictly less than the exact quotient $\frac{23737}{10000}$ (numerically $2.3737$ when read in the real-valued codomain used by the imported quantity). The inequality is strict, equality is excluded, and there are no assumptions that $K$ is finite, has a particular characteristic, is algebraically closed, or satisfies any condition beyond being a field; the supplied file does not define $\mathrm{matMulExp}$ , so no additional meaning for that imported quantity is asserted here.

Human review

Endorsed by Shuze Chen · Aug 30, 2026
Endorsed by marwahaha · Aug 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph