Matrix Multiplication from Polynomial Packings: A Constructive and Elementary Proof of $ω\le9/4$
Rafael Pass
cs.CC
Oct 20, 2026 · v2
TL;DR
Aristotle generated an approximately 3,600-line Lean 4 formalization of the matrix-multiplication identities and the operation bound, using Mathlib's matrix definitions.
Abstract
We give a self-contained constructive proof that the matrix multiplication exponent satisfies $ω\le9/4$. In a recent breakthrough, OpenAI \cite{original} established this bound in the model of exact scalar arithmetic over the complex numbers, using non-constructive arguments in Strassen's asymptotic spectral framework. We explicitly construct a Strassen-style matrix multiplication identity and obtain the bound by ordinary block recursion. For every $γ>0$, the resulting algorithm multiplies two $n\times n$ integer matrices using $O(n^{9/4+γ})$ integer arithmetic operations. As an independent contribution, we develop a framework of polynomial packings—methods for reducing many polynomial multiplications to fewer ones using linear operations. We isolate and generalize a construction of OpenAI \cite{original} to obtain a simple packing, and show how packings can be composed to amplify their “compression rate", which finally yields Strassen-like identities.
Problem
OpenAI recently proved the matrix multiplication exponent bound ω ≤ 9/4, but the argument is non-constructive and relies on Strassen's asymptotic spectrum over the complex numbers. The goal is an explicit, elementary, constructive algorithm reaching the same bound using integer arithmetic.
Approach
The authors introduce polynomial packings: ways of reducing many polynomial multiplications to fewer ones using linear operations. They generalize OpenAI's three-for-one gadget to a (c+2)-for-c packing and amplify its compression by composing packings over multiple variables. Tensoring then yields a fixed Strassen-style block identity, which is applied recursively. The AI system Aristotle produced a Lean 4 formalization of the identities and the resulting operation bound; the authors note they did not independently verify it.
Results
For every γ>0, the explicit recursive algorithm multiplies n×n integer matrices in O(n^{9/4+γ}) integer operations, giving ω ≤ 9/4 constructively. The Lean formalization is about 3,600 lines, compared with about 20,700 lines in OpenAI's development.
