Matrix multiplication exponent below 2.3710449, machine-checked over every commutative ring
A Lean development produced largely by AI systems under two researchers' direction proves that the matrix multiplication exponent is below 2.3710449 over every commutative ring, improving DeepMind's 2.371177 of August 2026 by sharing extraction across recursion levels of the laser method.
- Lab
- Independent
- Model
- GPT-6 Astra, Claude Fable 5.1, Claude Opus 5 and Opus 5.5; Meta Muse Spark 1.3 for the final numerical search
- Field
- Computer science
- Date
- 2026-10-07
- Human collaborators
- Oliver Proudfoot, Andrew Perrault
- Problem posed
- 1969 · open 57 yrs
What was found
The previous record came from combination-loss analysis of the laser method, extracting independent matrix products one recursion level at a time. This work shares the extraction across levels and keeps the same source tensor, the eighth tensor power of the Coppersmith-Winograd tensor , for the level-four construction. The exponent is defined through the exact tensor rank of matrix multiplication over an arbitrary commutative ring , and the Lean theorem states . The development is 2,170 modules on Mathlib; the large numerical tables are checked in the kernel by generic, once-proved checkers on packed natural numbers rather than by native_decide, and the README reports no sorry, admit or custom axiom. The accompanying paper, 'Cross-Level Laser Extraction for Faster Matrix Multiplication', states the rounded bound 2.371045.
Novelty check
The repository's formalization.yaml cites Dupont and colleagues (arXiv:2608.16884, 2.371177) as the previous best and the asymmetric laser-method papers it builds on; that matches this registry's 2026-08-17-matmul-exponent. The repository's last push was at 04:00 UTC on 2026-10-06, hours before OpenAI's release claimed 9/4 over the complex numbers (2026-10-06-matmul-exponent-nine-fourths), and it was registered on Palomar on 2026-10-07. When the result first became public is not documented, so the Palomar date is used.
Caveats and known objections
Graded formal on the Palomar registration, which replays the proof against a separate statement file, together with the authors' audit of that statement; the authors are explicit that they did not verify every step of the natural-language proof and that correctness rests on the formal one. The README's 'independent verification' was carried out by Andrew Perrault, who is a co-author, so it is a clean-room rebuild rather than an outside check. As a record it lasted about a day: OpenAI's claimed 9/4 bound over the complex numbers superseded it on 2026-10-06, and Sela Navot's Palomar-registered extensions of that proof cover every field and, since 2026-10-11, every ring, under that work's own arithmetic definition of the exponent. What remains is a laser-method bound with an independent formal proof, which matters if the 9/4 argument does not survive scrutiny. Autonomy is graded ai-led: the README says the shared-extraction idea, its proof and the Lean were produced largely by AI systems, and that the authors chose the problem, directed the work, audited the formal statement and reproduced the build.
Machine-checked elsewhere
PalomarPALOMAR-2026-10-07-000007
olliepro/LeanMMBound at 93492a4dd1ee · checked 2026-10-07
ProvedMatrixBounds.Numeric.SuppliedCertifiedPipeline.exponent_lt
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.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered 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.
Graded formally verified for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Matrix multiplication exponent below 2.3710449, machine-checked over every commutative ring. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-10-07-matmul-exponent-2371045BibTeX
@misc{whataifound-independent-2026-2371045,
title = {Matrix multiplication exponent below 2.3710449, machine-checked over every commutative ring},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Formally verified. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-10-07-matmul-exponent-2371045}
}