oai-math-revised beta

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

Staggered extraction for exact matrix multiplication over every field

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

We prove that the arithmetic exponent of square matrix multiplication over every fixed field satisfies ω < 2.371054886006746. This includes every positive characteristic.

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-21) and not checked by a person. May be wrong or incomplete. Report an error.

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 the unconditional bound $\omega(F)<2.371054886006746$ for every field, counting additions, subtractions and multiplications in division-free programs, with no numerical inequalities left as hypotheses. [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]

Possibly relevant literature (found by the agent, not checked)

News and blogs

Elsewhere

Independent sites; their content is not reviewed here.

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

From OpenAI's README for this paper:

Verification

Use Python 3.10 or later with mpmath==1.3.0, as specified in verification/data/requirements.txt. Keep assertions enabled. From this paper directory, run both interval modes with fresh output paths:

matrix_verification_output="$(python3 -c 'import pathlib, tempfile; print(pathlib.Path(tempfile.mkdtemp(prefix="matrix-all-fields-verify-")).resolve())')"
python3 -B verification/scripts/verify_parameters.py --mode interval --dps 80 --rational-log --output "$matrix_verification_output/rational-series.json"
python3 -B verification/scripts/verify_parameters.py --mode interval --dps 80 --output "$matrix_verification_output/native-log.json"

Every entry in each output's checks object should be true. The first mode uses a rational logarithm series with an explicit tail; the second is a directed native-logarithm cross-check. These calculations check the finite certificates, not the tensor constructions or limiting arguments.

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: