Asymmetric hashing square retune: omega < 2.37465

Proved

mme_omega_lt_237465

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

algebraic-complexityasymmetric-hashingcoppersmith-winogradmatrix-multiplication

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

\omega(K)<2.37465.

This is a conservative exact-rational endpoint for the square-power asymmetric-hashing analysis of the Coppersmith--Winograd tensor with parameter $q=6$ . It slightly sharpens the previously formalized $2.3747$ endpoint while retaining the same tensor construction and field-uniform conclusion.

Formalization Note The decimal endpoint is represented exactly as $237465/100000$ ; no characteristic restriction is imposed on $K$ .

Preamble

import Definitions.Def_mme_omega

open MME

universe u

set_option autoImplicit false

Formal statement

theorem mme_omega_lt_237465 {K : Type u} [Field K] :
    matMulExp K < (237465 : ℝ) / 100000 := by sorry

Source

Ran Duan, Hongxun Wu, and Renfei Zhou, Faster Matrix Multiplication via Asymmetric Hashing, arXiv:2210.10173v5 / FOCS 2023, Section 6.3 and Table 2 (printed pp. 58-59), and the square-power numerical bound in Section 8.3, Table 3 (printed p. 78); https://arxiv.org/abs/2210.10173.

View graph