Theoretical computer science · Result 107

Matrix multiplication with exponent at most 9/4

3 papersLean

Proves \(\omega\le9/4\) over ℂ, giving \(O_\varepsilon(n^{9/4+\varepsilon})\) arithmetic operations for square matrix multiplication. In characteristic zero, some inner dimension n^a 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.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 3

An Upper Bound of 9/4 for the Matrix Multiplication Exponent

OpenAI · October 2, 2026

We prove that the exponent of matrix multiplication over the complex numbers is at most 9/4.

Read PDF Download Source

Cite

@misc{OAI:Matrix-Multiplication-Nine-Fourths-October-2-2026,
  author = {{OpenAI}},
  title = {{An Upper Bound of $9/4$ for the Matrix Multiplication Exponent}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Matrix-Multiplication-Nine-Fourths-October-2-2026/paper.pdf}{OAI:Matrix-Multiplication-Nine-Fourths-October-2-2026}},
  year = {2026}
}

Complex Matrix Multiplication Below 2.258 and Rectangular Bounds

OpenAI · September 24, 2026

— secondary writeup 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.

Read PDF Download Source

Cite

@misc{OAI:Complex-Matrix-Multiplication-Below-2.258-and-Rectangular-Bounds-September-24-2026,
  author = {{OpenAI}},
  title = {{Complex Matrix Multiplication Below $2.258$ and Rectangular Bounds}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Complex-Matrix-Multiplication-Below-2.258-and-Rectangular-Bounds-September-24-2026/Complex-Matrix-Multiplication-Below-2.258-and-Rectangular-Bounds-September-24-2026.pdf}{OAI:Complex-Matrix-Multiplication-Below-2.258-and-Rectangular-Bounds-September-24-2026}},
  year = {2026}
}

Staggered extraction for exact matrix multiplication over every field

OpenAI · 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.

Read PDF Download Source

Cite

@misc{OAI:Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026,
  author = {{OpenAI}},
  title = {{Staggered extraction for exact matrix multiplication over every field}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026/Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026.pdf}{OAI:Staggered-extraction-for-exact-matrix-multiplication-over-every-field-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalized results bound the complex matrix-multiplication exponent by \(\omega(\mathbb C)\le9/4\), the dual exponent by \(\alpha>0.465\), and the rectangular exponent at aspect ratio \(0.709\) by \(\omega(\mathbb C;1,0.709,1)<2.092\). The dual exponent is the supremum of rectangular aspect ratios attainable with exponent \(2\). The arithmetic model counts additions, subtractions, and multiplications in finite division-free programs, with arbitrary positive exponent slack. The square bound implies the paper's weaker \(2.258\) headline bound.

The formalized result gives the unconditional bound \(\omega(F)<2.371054886006746\) for every field \(F\), including finite fields and fields of positive characteristic. The exponent counts additions, subtractions, and multiplications in finite division-free arithmetic programs, with arbitrary positive exponent slack. No numerical inequalities remain as hypotheses. The result concerns arithmetic complexity, rather than bit complexity or practical crossover sizes.

Comparator links

Result	Comparator statement
Complex square, dual, and rectangular exponent bounds	MatrixMultiplication.lean
Matrix-multiplication exponent over every field	MatrixFields.lean

Scope note on GitHub →