Formally verified AI-led

Matrix multiplication exponent bounded by 9/4

An OpenAI manuscript proves that two $n \times n$ complex matrices can be multiplied with $O(n^{9/4+\varepsilon})$ arithmetic operations, lowering the best bound on the matrix multiplication exponent from 2.371177 to 2.25, with a Lean proof that two outside researchers rebuilt and extended to every field within two days.

Lab: OpenAI
Model: Unreleased internal OpenAI model, not named in the release
Field: Computer science
Date: 2026-10-06
Problem posed: 1969 · open 57 yrs

Sources

What was found

Every improvement since Coppersmith and Winograd's 2.376 of 1990 has come from refining the laser method and has moved the third or fourth decimal place; this proof does not use that route. It works in Strassen's asymptotic spectrum, with tensor characters that add on direct sums, multiply on tensor products and are monotone under restriction. A Fourier-projection separation turns blocks that share variables on one leg into independent blocks, and applied to polynomial multiplication it gives a profile $P(a, b)$ with $P(a, 3h + a - 1) \ge 3P(a, h)$ and $P(1, b) = b$ , which force $P(a, a) \ge a^{4/3}$ ; comparing with the interpolation bound gives $t \le 3/4$ for every character and hence $\omega \le 9/4$ . Two companions in the family give $\omega < 2.258$ and $\alpha > 0.465$ in characteristic zero, and $\omega < 2.371054886006746$ over every field. The result concerns the arithmetic exponent and says nothing about practical matrix sizes.

Novelty check

Read the manuscript's introduction and the Lean scope document at commit fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb on 2026-10-12. The previous published bound is 2.371177 from Dupont and colleagues in August 2026 (2026-08-17-matmul-exponent), which the manuscript cites. A separate 2.3710449 bound over every commutative ring, LeanMMBound, was pushed to its repository hours before this release (2026-10-07-matmul-exponent-2371045). No earlier claim near 2.25 was found.

Caveats and known objections

Graded formal because the Lean proof has been rebuilt and extended outside OpenAI, not on OpenAI's own catalogue, which records its review status as unchecked. Jeroen Zuiddam, who works on the asymptotic spectrum of tensors the proof relies on, published a derived repository on 2026-10-07 importing 143 of OpenAI's modules (99 unchanged) and proving the bound over every field, restating the arithmetic model and proving the infimum is not vacuous; its CI build passed and its README reports a Comparator replay with only the three standard axioms. Sela Navot's separate extension, written with GPT-6 Astra and GPT-6.1 Sol under Navot's direction, is registered on Palomar for every field and, since 2026-10-11, every ring; each implies the complex statement. Those checks certify the Lean statement, not the manuscript: the arithmetic model is one standard definition of the exponent, and nobody outside OpenAI is on record as having read the paper's argument. Scientific American, which interviewed Virginia Vassilevska Williams, whose group set several of the previous records, on the problem's importance, still described the bound as an unverified claim on 2026-10-08. Autonomy is graded ai-led for the same reasons as the other families split from this release.

Independent checks

Jeroen Zuiddam (University of Amsterdam): Rebuilt the 143 modules of OpenAI's Lean library that the bound imports, modified 41 to remove the one use of a primitive root of unity unavailable in positive characteristic, and proved $\omega(F) \le 9/4$ for every field $F$ , with the arithmetic model kept verbatim from OpenAI's Comparator challenge. CI build passed on 2026-10-07; axioms reported as propext, Classical.choice and Quot.sound. · link ↗

Sela Navot: Independent fork extending the same proof to every field, then to every ring in a second repository; both registered on Palomar after its preflight passed. The extension was found and written by GPT-6 Astra and GPT-6.1 Sol under Navot's direction, so it is a check outside OpenAI but not a check without AI. · link ↗

Machine-checked elsewhere

PalomarMatrix multiplication exponent at most 9/4 over arbitrary fields

PALOMAR-2026-10-08-000005 · selanavot/matrix-multiplication-all-fields at 8375e73ed454 · checked 2026-10-08

ProvedComparatorChecks.omega_boundComparatorChecks.admissible_bddBelowComparatorChecks.admissible_nonemptyComparatorChecks.omega_lowerComparatorChecks.epsilon_costComparatorChecks.exact_coefficients

A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.

A derived work extending OpenAI's proof from the complex numbers to every field; the complex bound is a specialization.

PalomarMatrix multiplication: omega at most 9/4 over every ring

PALOMAR-2026-10-11-000007 · selanavot/omega_le_nine_quarters_all_rings at 9d10116c89f9 · checked 2026-10-11

The same author's further extension to every ring.

Also recorded at

vibemathedmatrix-multiplication-exponent-9-4

Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.

Disagree with these grades?

Bring a citation: a grade moves on evidence, not on argument.

Challenge this grade Submit a check

Or on GitHub: submit a check challenge the grade send a correction or send a pull request

History of this entry

2026-10-16CorrectedRecorded the vibemathed record for this result as a registration. It cites the same manuscript. No grade moved.
2026-10-12CheckedRecorded Jeroen Zuiddam's rebuild of the Lean proof over every field and Sela Navot's two Palomar-registered extensions, which are why this family is graded formal while the rest of the release stays claimed. source ↗
2026-10-12AddedEntered the registry graded Formally verified and AI-led.

Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.

Community discussion

Hacker NewsSharing AI progress in mathematics↗

Graded formally verified for verification and ai-led for autonomy. What these mean.

Cite this entry

Plain text

whataifound.org. (2026). Matrix multiplication exponent bounded by 9/4. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-10-06-matmul-exponent-nine-fourths

BibTeX

@misc{whataifound-openai-2026-fourths,
  title        = {Matrix multiplication exponent bounded by 9/4},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by OpenAI. Verification: Formally verified. Autonomy: AI-led.},
  url          = {https://whataifound.org/finding/2026-10-06-matmul-exponent-nine-fourths}
}

Related findings

ClaimedLower bound of 21 multiplications for 3×3 matrix multiplication over every field, with a Lean proofIndependent · 2026-10-12 Formally verifiedMatrix multiplication exponent below 2.3710449, machine-checked over every commutative ringIndependent · 2026-10-07 Author verifiedTruly subquadratic 3SUM and truly subcubic APSP, refuting two central fine-grained complexity hypothesesAnthropic · 2026-10-05

algorithms matrix-multiplication complexity tensors lean argument

← All computer science findings in the registry