Jump to content

Matrix multiplication with exponent at most 9/4

From OpenAI Aftermath
Revision as of 20:48, 13 October 2026 by Aftermath bot (talk | contribs) (Palomar registry links (UC-0037): two 9/4 extensions; Cureton's Lean formalization of the Dedekind zero-free region)

Matrix multiplication with exponent at most 9/4 is the subject of a manuscript dated 2 October 2026 in OpenAI's public mathematics collection (github.com/openai/math), with two companion manuscripts dated 24 September 2026. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

The original results

  • Claim. For every ε > 0, two n × n complex matrices can be multiplied using Oε(n9/4+ε) arithmetic operations; in particular the exponent of matrix multiplication over C satisfies ω ≤ 9/4. The companion manuscripts state ω < 2.258, a dual exponent α > 0.465 and ω(1, 0.709, 1) < 2.092 in characteristic zero, and ω < 2.371054886006746 over every fixed field (summary in the collection's contents list).
  • Method, as described in the paper's introduction. The proof combines explicit tensor degenerations with Strassen's spectral viewpoint. It derives inequalities for character values on polynomial-multiplication tensors and uses their discrete growth to bound the values on matrix multiplication. The central finite construction separates blocks that already have independent variables on two of the three tensor legs, using a finite Fourier projection and a degeneration that retains the correct block labels.
  • Sources (openai/math repository, commit adc7f12):
  • Formalization, as described by the repository. The scope note lean/docs/107.md states that the Lean formalization proves ω(C) ≤ 9/4, α > 0.465 and ω(C; 1, 0.709, 1) < 2.092, and ω(F) < 2.371054886006746 for every field F, including fields of positive characteristic. The model counts additions, subtractions and multiplications in finite division-free programs; the note states that the result concerns arithmetic complexity, not bit complexity or practical crossover sizes. The comparator statements are MatrixMultiplication.lean and MatrixFields.lean.
  • Catalogue status. The AIM open-problem collection (MColbrook/AIM, not affiliated with the American Institute of Mathematics) lists the 9/4 manuscript as partial progress on its problem 028 ("Is the matrix-multiplication exponent two?"), after an AI statement-level comparison on 13 October 2026 (checked 14 October 2026).
  • Earlier published bound. J. Alman, R. Duan, V. Vassilevska Williams, Y. Xu, Z. Xu and R. Zhou, More Asymmetry Yields Faster Matrix Multiplication (arXiv:2404.16349, v3, 19 August 2026), state ω < 2.371177, using the numerical optimization of Dupont et al. (arXiv:2608.16884).

Public follow-up work

Date Work Relation Public claim Public status (checked 14 October 2026)
2026-10-07 J. Zuiddam, jzuiddam/omega-nine-quarters-all-fields (GitHub) Extension (formal) A Lean proof that ω(F) ≤ 9/4 for every field F, derived from OpenAI's Lean library at commit adc7f12. According to the README, only the Fourier separation step uses more of C than an algebraically closed field; the proof replaces the period 5M by 3M − 2 or 3M − 1 (whichever is nonzero in the field), works over an arbitrary algebraically closed field, and adds a descent to every field. The README states: "Developed with AI assistance (Claude); verified by the Lean kernel and the comparator", and reports only the standard axioms.
2026-10-07 P. Uznański, Rectangular matrix multiplication from shared-leg entropy (arXiv:2610.10494, v1) Extension Extends "the analysis underlying a recent matrix-multiplication result by OpenAI" to rectangular products: ω(1, k, 1) ≤ 2 for 0 ≤ k ≤ 1/2 and ω(1, k, 1) ≤ 1 + k + 1/(4k) for k ≥ 1/2. Hence ω(1, 1/2, 1) = 2 and α ≥ 1/2 (the companion manuscript states α > 0.465). Applications: Zwick's all-pairs shortest-paths algorithm for directed unweighted graphs runs in O(n2.5) time, and in O(n2.4999) with the (min,+)-product improvement of Alman and Vassilevska Williams. arXiv v1.
2026-10-07 (release v1.0.0) S. Navot (direction), selanavot/matrix-multiplication-all-fields (GitHub; Zenodo 10.5281/zenodo.23219128) Extension (formal) A Lean proof that ω(F) ≤ 9/4 for every field F, finite or infinite, of any characteristic, together with an exact coefficient-rank version. The changes to OpenAI's argument are a Fourier period of 5M or 5M + 1, interpolation nodes in the algebraic closure, and a descent with fixed overhead. The README states that the extension was found and formalized by GPT-6 Astra and GPT-6.1 Sol, and the accompanying paper generated through Codex, under Sela Navot's direction. It records a fresh Lean kernel replay and adversarial reviews by AI agents, which it says "are not human peer review". Registered in the Palomar registry as PALOMAR-2026-10-08-000005 (version 1, 8 October 2026).
2026-10-07 THM-4568, in the GitHub repository eliottcassidy2000/math Analysis (limits of the method) The properties of the symmetrized polynomial-multiplication profile used in the 9/4 proof admit a pointwise least admissible profile, which meets the rank bound exactly at exponent 9/4. So these properties alone cannot give ω < 9/4. The record also states finite-size versions of the bound. A record in a multi-agent AI research repository, labelled "PROVED (elementary …)", with AI audits kept in the same repository.
2026-10-09 (repository created; last updated 13 October) selanavot/omega_le_nine_quarters_all_rings (GitHub; Zenodo 10.5281/zenodo.23268534) Extension (formal) A Lean proof that ω(R) ≤ 9/4 for every associative unital ring R, including noncommutative rings. The README describes it as an extension of the same owner's all-fields repository. The README states that the Lean development and the paper are AI-generated with Codex under human direction, with "no claim of a better numerical bound or independent human peer review"; the repository description calls it work in progress. Registered in the Palomar registry as PALOMAR-2026-10-11-000007 (version 1, 11 October 2026).
2026-10-10 acprk, openai-math-followups (GitHub) Analysis; check States the same exact tightness of the 9/4 argument (crediting THM-4568 for the core statement), and that a list of further valid inequalities (concavity along a + b = const, higher determinant filtrations, bivariate multiplication, some laser extractions) also cannot give a bound below 9/4. Also rechecks the all-fields extension, crediting the repository above, with its own Lean lemmas. The README states that the work was done with Claude and Codex as assistants. The repository also treats two other OpenAI result families.
  • R. Zadeh, A faster matrix multiplication algorithm through structured optimization (arXiv:2610.10593, v1, 6 October 2026), states ω < 2.37115924 within the Coppersmith–Winograd combination-loss framework, improving the bound 2.371177. Version 1 does not cite the OpenAI manuscripts.

Notes

  • Several follow-ups state substantial AI assistance, as recorded in the table.
  • The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
Retrieved from "https://openai-aftermath.mathnt.net/index.php?title=Matrix_multiplication_with_exponent_at_most_9/4&oldid=42"