oai-math-revised beta

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

Complex Matrix Multiplication Below 2.258 and Rectangular Bounds

OpenAI · September 24, 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

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

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

Formalization

  • OpenAI, Matrix multiplication with exponent at most 9/4 — Lean scope notes (OpenAI math release, lean/docs/107.md, 2026-10-06). Lists this paper as accompanying the Lean development, which records $\alpha>0.465$ and $\omega(\mathbb C;1,0.709,1)<2.092$ together with $\omega(\mathbb C)\le9/4$; the notes say the square statement implies this paper's 2.258 bound. [family-level]
  • Jeroen Zuiddam, ω(F) ≤ 9/4 over every field, in Lean (Lean 4 repository, verification reported 2026-10-07). Generalizes the family’s complex $9/4$ proof to every field through modified Fourier periods and descent, reporting kernel and Comparator verification and disclosing Claude assistance. [family-level]
  • Sela Navot, Matrix multiplication over arbitrary fields (Lean 4 repository, verification reported 2026-10-06). Extends the family’s $9/4$ proof to arbitrary fields, with exact coefficient identities, positive-slack operation bounds and documented kernel replay, developed by GPT-6 Astra and GPT-6.1 Sol under Navot’s direction. [AI-generated per source] [family-level]
  • Sela Navot, Matrix multiplication: ω ≤ 9/4 over every ring (Lean 4 repository, version 0.1.0; accessed 2026-10-21). Extends the family’s $9/4$ construction through exact integer tensor identities to division-free programs over arbitrary associative unital rings, including noncommutative rings, with verification records and an accompanying manuscript. [AI-generated per source] [family-level]

News and blogs

Elsewhere

Independent sites; their content is not reviewed here.

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

From OpenAI's README for this paper:

Verification

First check the numerical payload and build-input inventory:

python3 -B verification/scripts/check_certificate.py

A zero exit status confirms input integrity only; it does not execute the numerical proof.

The full square-certificate replay requires Python 3.9 or later, POSIX fork, a C++17 compiler with signed 128-bit integers, a 64-bit long, arithmetic signed right shift, UndefinedBehaviorSanitizer, and GMP C++ headers and libraries. Keep Python and C++ assertions enabled. From this paper directory, run:

certificate_output="$(python3 -c 'import pathlib, tempfile, uuid; print(pathlib.Path(tempfile.gettempdir()).resolve() / ("matrix-square-certificate-" + uuid.uuid4().hex))')"
python3 -B verification/certificate/reproduce.py --cxx 'g++ -fsanitize=undefined -fno-sanitize-recover=all' --work-dir "$certificate_output"
python3 -B verification/certificate/verify_manuscript_bounds.py --work-dir "$certificate_output"

Both commands must exit successfully. They check finite arithmetic interfaces; the tensor constructions and analytic allowances remain statements proved in the manuscript.

Run the default rectangular checks in a fresh writable copy because they write results beside their inputs:

rectangular_work="$(mktemp -d)"
cp -R verification/certificates "$rectangular_work/certificates"
python3 -B "$rectangular_work/certificates/checks/run_checks.py"

The default checks use only the Python standard library and succeed with a zero exit status. Optional --numerics diagnostics require mpmath==1.3.0 and are high-precision evaluations, not rigorous interval certificates.

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: