Claimed Collaborative

Lower bound of 21 multiplications for 3×3 matrix multiplication over every field, with a Lean proof

Andrey Ivanov, working with OpenAI models through ChatGPT and Codex, claims that every exact bilinear algorithm for multiplying two $3 \times 3$ matrices over any field uses at least 21 multiplications, with a Palomar-registered Lean proof, which would raise the bound that holds over every field from Bläser's 19 of 2003.

Lab: Independent
Model: OpenAI models through ChatGPT and Codex, versions not recorded in the repository (GPT-6 Astra and GPT-6 Sol by the author's later account to vibemathed)
Field: Computer science
Date: 2026-10-12
Human collaborators: Andrey Ivanov

Sources

Original work

GitHubAIV5/mmrank21, the Lean proof↗DOIZenodo: archived release 0.1.1↗

What was found

The bilinear complexity, or tensor rank, of $3 \times 3$ matrix multiplication sits below Laderman's 1976 algorithm with 23 multiplications, which works over every field, and over every field the best lower bound was Bläser's 19 from 2003. During 2026 a run of field-specific results closed the gap over $\mathbb{F}_2$ : 21 by Chengu Wang, 22 over $\mathbb{F}_2$ and for integer coefficients by Rudich and Rousseau, and the exact rank 23 by Tomar on 2026-10-08, each by exhaustive or certified search tied to the field. This result is uniform: the Lean theorem takes any field $K$ , any finite index set $I$ , arbitrary linear forms $a_i$ and $b_i$ and matrices $W_i$ with $AB = \sum_i a_i(A) b_i(B) W_i$ for all $A$ and $B$ , and concludes $|I| \ge 21$ , with no assumption of minimality, nonzero terms or coefficient ranks. The argument passes to an algebraic closure, picks a decomposition minimizing a rank sum in its first coefficient family, and rules out 20 or fewer terms through what the author calls conductor growth and residual reconstruction. It concerns exact bilinear complexity, not border rank or the asymptotic exponent.

Novelty check

Read the README, formalization.yaml and Challenge.lean at commit cb1557b7ea80ea66fae4714628663d8c1df7a48d on 2026-10-16, and the abstracts of the field-specific papers the repository cites (arXiv:2609.06725, 2610.01639 and 2610.11823). Those concern $\mathbb{F}_2$ or integer coefficients and do not give 21 over an arbitrary field. The repository dates the result to its Zenodo release of 2026-10-12 and makes no claim of exhaustive priority verification. Nothing in the registry covered the rank of $3 \times 3$ matrix multiplication; its matrix multiplication entries concern the asymptotic exponent.

Caveats and known objections

Graded claimed rather than formal. The Palomar registration replayed the proof at commit cb1557b against the Mathlib-only statement in Challenge.lean with Comparator, and that statement, read by vibemathed and here, is as far as either reading goes exactly the unrestricted bilinear rank of the $3 \times 3$ matrix multiplication tensor over an arbitrary field, finite fields and characteristic 2 included. But the theorem's shape is the author's own, and this registry held 2026-09-06-bollobas-nikiforov at claimed on the same kind of evidence because a curator's reading is not a named expert's; 2026-10-07-matmul-exponent-2371045 was graded formal on comparable evidence, so the precedents disagree and the weaker grade is used. An algebraic complexity theorist confirming the short statement would support formal. The repository records its review status as self-assessed, no mathematician is on record as having read the argument, and the Lean comments are mostly in Russian. Over $\mathbb{F}_2$ the bound is already superseded by Tomar's exact rank of 23, so what is new is the uniformity across fields; whether 22 or 23 holds over every field remains open. Autonomy is graded collaborative: the repository says the research and formalization were developed with substantial AI assistance in mathematical exploration and Lean under the author's direction, and records neither model versions nor prompts. vibemathed reports the author's later account that GPT-6 Astra did most of the work, with GPT-6 Sol for part of it, while he redirected dead ends and supplied missed literature; that account is not in the repository at the registered commit, and although it would make ai-led defensible, the weaker grade stands.

Machine-checked elsewhere

PalomarPALOMAR-2026-10-13-000009

AIV5/mmrank21 at cb1557b7ea80 · checked 2026-10-13

ProvedMMRank.Palomar.lower_bound

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.

Permitted axioms are exactly propext, Quot.sound and Classical.choice.

Also recorded at

vibematheda-lower-bound-of-21-for-3-3-matrix-multiplication-over-every-field

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

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.

Submit a check Challenge the grade

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

Entry history (1 event)

2026-10-16AddedEntered the registry graded Claimed and Collaborative.

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

Graded claimed for verification and collaborative for autonomy. What these mean.

Cite this entry

Plain text

whataifound.org. (2026). Lower bound of 21 multiplications for 3×3 matrix multiplication over every field, with a Lean proof. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-10-12-matmul-3x3-rank-21

BibTeX

@misc{whataifound-independent-2026-21,
  title        = {Lower bound of 21 multiplications for 3×3 matrix multiplication over every field, with a Lean proof},
  author       = {{whataifound.org}},
  year         = {2026},
  howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
  note         = {Result by Independent. Verification: Claimed. Autonomy: Collaborative.},
  url          = {https://whataifound.org/finding/2026-10-12-matmul-3x3-rank-21}
}

Related findings

Formally verifiedMatrix multiplication exponent below 2.3710449, machine-checked over every commutative ringIndependent · 2026-10-07 Formally verifiedMatrix multiplication exponent bounded by 9/4OpenAI · 2026-10-06 Author verifiedTruly subquadratic 3SUM and truly subcubic APSP, refuting two central fine-grained complexity hypothesesAnthropic · 2026-10-05

algorithms matrix-multiplication tensor-rank lower-bounds lean formalization argument

← All computer science findings in the registry