A lower bound of 21 for 3 × 3 matrix multiplication over every field

What the AI did

Andrey Ivanov posed the research task and directed the project. According to his account, GPT-6 Astra (gpt-6-astra) performed most of the work, contributing both to the development of the mathematical proof and to its Lean formalization. GPT-6 Sol (gpt-6-sol) was also used for part of the work to reduce costs. Ivanov supplied known results missed during the models' literature searches, redirected work when approaches reached dead ends, and organized the research workspace around a catalogue of results, Lean formalization, and SageMath for rapid testing of conjectures. Mathematical ideas were discussed throughout the process, but the extent to which those discussions influenced particular model-generated ideas cannot be reconstructed reliably. The AI co-developed classification describes this human-directed collaboration without assigning individual lemmas or a numerical share of the mathematical contribution to either party. Ivanov is the author and responsible maintainer. The repository's own disclosure at the registered commit (README and formalization.yaml) says the research and formalization had substantial assistance from OpenAI's ChatGPT/Codex, model versions not recorded; the model names above are the author's later clarification.

Verification

No independent mathematician has checked this yet. Read by this site on 15 October 2026, not rebuilt. The headline theorem MMRank.Palomar.lower_bound was read in Challenge.lean, which imports only Mathlib: for any field K and finite index set I, if $AB=\sum_i a_i(A)b_i(B)W_i$ for all $3\times3$ matrices $A,B$, with arbitrary linear forms $a_i,b_i$ and matrices $W_i$, then $|I|\geqslant21$. That is exactly bilinear rank (tensor rank) of the 3x3 matrix multiplication tensor: exact equality, not border rank, no restriction on the algorithm, and an arbitrary Field includes finite fields and characteristic 2. Solution.lean proves the same statement and comparator.json pairs the two. A grep of all 198 Lean files (18,829 lines) found only the deliberate sorry in Challenge.lean, which nothing imports; no axiom declarations, native_decide, unsafe, implemented_by or extern. The repository's CI run 38306224074 on commit cb1557b printed propext, Classical.choice and Quot.sound for the headline and audited 1,842 project declarations; Palomar run 38306239835 fetched the same commit and its Comparator step passed. Both logs were read here; neither build was repeated. The proof itself was not read.

Sources

• PaperRelated result over F2: exact rank 23 · Bläser 2003: the previous general lower bound of 19 · Related result over F2: lower bound 21 (Wang) · Related result over the integers: lower bound 22 (Rudich and Rousseau)
• Lean proofGitHub repository with Lean proof · Standalone statement using only Mathlib · Proved statement and proof entry point · Public theorem for arbitrary linear forms
• Problem recordBläser, Fast Matrix Multiplication (survey, 2013): the range 19 to 23
• OtherPalomar registry record, version 1 · Archived release 0.1.1 on Zenodo · Authorship and initial AI disclosure in the registered snapshot · Palomar mechanical verification of this commit · Proof overview