Proves \omega\le9/4 over ℂ, giving O_\varepsilon(n^{9/4+\varepsilon}) arithmetic operations for square matrix multiplication. In characteristic zero, some inner dimension na with a > 0.465 permits n^{2+o(1)} rectangular multiplication. Further square bounds give ω < 2.258 outside finitely many positive characteristics and ω < 2.371054886006746 over every fixed field. (Lean)
Manuscripts (3)
An Upper Bound of 9/4 for the Matrix Multiplication Exponent
October 2, 2026 · source · Lean formalization available · cite as \cite{OAI:Matrix-Multiplication-Nine-Fourths-October-2-2026}
We prove that the exponent of matrix multiplication over the complex numbers is at most 9/4.
Complex Matrix Multiplication Below 2.258 and Rectangular Bounds (secondary writeup)
September 24, 2026 · source · Lean formalization available · cite as \cite{OAI:Complex-Matrix-Multiplication-Below-2.258-and-Rectangular-Bounds-September-24-2026}
Over every field of characteristic zero, we prove that the square matrix-multiplication exponent satisfies ω < 2.258, the dual exponent satisfies α > 0.465, and \omega(1,0.709,1)\lt 2.092. The strict square and k = 0.709 rectangular bounds also hold over every field except possibly in one finite set of positive characteristics, in the arithmetic-operation model.
Staggered extraction for exact matrix multiplication over every field
September 24, 2026 · source · Lean formalization available · cite as \cite{OAI:Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026}
We prove that the arithmetic exponent of square matrix multiplication over every fixed field satisfies ω < 2.371054886006746. This includes every positive characteristic.
Result 107 · Theoretical computer science. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.
Source: https://github.com/openai/math/blob/main/CONTENTS.md