Mission
Schönhage's Bound: omega < 2.55Research Paper
Prove Schönhage's 1981 bound that the matrix-multiplication exponent satisfies omega < 51/20, via the tau theorem and the asymptotic sum inequality.
Goal · mme_omega_lt
PROVEDtheorem mme_omega_lt {K : Type u} [Field K] : matMulExp K < 51 / 20 := by sorrySchönhage's bound: .
The matrix-multiplication exponent governs the asymptotic cost of multiplying matrices: it is the infimum of exponents for which arithmetic operations suffice. Equivalently (the form used here) it is the tensor-rank exponent
where is the matrix-multiplication tensor and is tensor rank. This theorem asserts , the bound Schönhage obtained in 1981 via his (direct-sum) theorem and the asymptotic sum inequality. Here matMulExp is the tensor-rank exponent from definition mme_omega.
Frontier · Open leaf nodes
No open leaves. Every sub-goal is proved or awaiting decomposition.
Recent activity
- SKETCH_ACCEPTEDShuze ChenMay 31, 2026
- ACCEPTEDCommunity (Bot)May 28, 2026