oai-math-revised beta

Browse › Theoretical computer science › 107 Matrix multiplication with exponent at most 9/4

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

OpenAI · October 2, 2026

Lean

Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion

Edit NOTES.md · Existing issues · Source on GitHub

Abstract

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

If the PDF does not display here, open it directly: Open PDF.

Notes

No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.

Automatically collected notes (unreviewed)

work in progress

Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-23) and not checked by a person. May be wrong or incomplete. Report an error.

Follow-up works

Comments and discussion

  • Alex Meiburg, Comment #179 on “The Mathocalypse” (Shtetl-Optimized, 2026-10-09). Emphasizes the distinction between the paper’s $O_\varepsilon(n^{9/4+\varepsilon})$ guarantee and an exact $O(n^{9/4})$ bound, and discusses the dependence of constants on $\varepsilon$.
  • Abbas Mehrabian (@abbas_mehrabian), post on X (2026-10-08). Calls the ω ⩽ 2.25 algorithm "groundbreaking", notes that his team held the best bound before it, and links his explanation of the history of ω.
  • Yuval Filmus (@YFilmus), post on X (2026-10-17). Describes the proof as "outlandish, using Strassen's theory of asymptotic spectra" and notes that Sergey Gusev's constructive proof of the same bound avoids spectra but is "also quite opaque".
  • Antoine Tilloy (@AntoineTilloy), post on X (2026-10-17). Describes an AI-assisted search for explicit, non-galactic algorithms with exponents between naive cubic and the 2.25 bound, which he calls "totally impractical".

Formalization

  • OpenAI, Matrix multiplication with exponent at most 9/4 — Lean scope notes (OpenAI math release, lean/docs/107.md, 2026-10-06). The release’s scope note records $\omega(\mathbb C)\le9/4$ for finite division-free arithmetic programs with arbitrary positive exponent slack, alongside α > 0.465 and ω(ℂ;1,0.709,1) < 2.092, although it lists only the two September companions as accompanying papers. [family-level]
  • Jeroen Zuiddam, ω(F) ≤ 9/4 over every field, in Lean (Lean 4 repository, verification reported 2026-10-07). Rebuilds the release's Lean proof and extends ω ≤ 9/4 to every field, generalising the period in Proposition 3.1 for positive characteristic and modifying 41 of 143 modules, with kernel and Comparator verification; the README discloses Claude assistance.
  • Sela Navot, Matrix multiplication exponent at most 9/4 over arbitrary fields (Palomar PALOMAR-2026-10-08-000005, Zenodo 10.5281/zenodo.23219128, 2026-10-07). Fork of the release's Lean proof extending ω ≤ 9/4 to all fields via the algebraic closure and a descent argument, with exact coefficient identities and documented kernel replay; developed by GPT-6 Astra and GPT-6.1 Sol under Navot’s direction. [AI-generated per source]
  • Sela Navot, Matrix multiplication: ω ≤ 9/4 over every ring (Palomar PALOMAR-2026-10-11-000007, Zenodo 10.5281/zenodo.23268534, 2026-10-11). Lean development showing the integer-coefficient tensor-rank exponent is at most 9/4, giving division-free programs over every associative unital ring, including noncommutative rings; it states it is "AI-generated with Codex under human direction". [AI-generated per source]

Digests and expositions

News and blogs

Elsewhere

Independent sites; their content is not reviewed here.

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}
}

Lean formalization

OpenAI provides Lean files for this family: lean/docs/107.md. The Lean statements have not been checked by people against the paper's claims.

Family 107: Matrix multiplication with exponent at most 9/4

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.

Other papers in this family: