Papers With

← All papers
First page of A lower bound for $\langle 3,2,m \rangle$ matrix multiplication

A lower bound for $\langle 3,2,m \rangle$ matrix multiplication

Askar Tsyganov, Uliana Parkina, Sergey Samsonov, Maxim Rakhuba

cs.CC Sep 18, 2026 · v1 cs.DS
formalization algebra
Read PDF arXiv abstract Code
TL;DR
The lower-bound proof for the bilinear complexity of ⟨3,2,m⟩ matrix multiplication is formally verified in Lean 4 against Mathlib.
Abstract
We prove that, over any field, the bilinear complexity of multiplying a $3\times 2$ matrix by a $2\times m$ matrix is strictly greater than $24m/5$. In particular, every exact bilinear algorithm for multiplying a $3\times 2$ matrix by a $2\times 5$ matrix requires at least $25$ multiplications. Together with the Hopcroft-Kerr upper bound, this proves that the $\langle 3,2,5\rangle$ matrix multiplication tensor has rank exactly $25$. The proof has been formally verified in Lean 4, with the formalization available at https://github.com/fallnlove/mm325_proof.
Problem

Determining the exact tensor rank (bilinear complexity) of multiplying a 3×2 matrix by a 2×m matrix over an arbitrary field, specifically improving the known lower bound of 24m/5.

Approach

The authors refine an existing argument to prove strictly that R_K(⟨3,2,m⟩) > 24m/5 over any field, using a normalization lemma bounding the dimension of spans of linear forms and constructing subspaces via kernel/image dimension counting. The proof idea was obtained with the aid of an AI system. The entire argument was mechanically checked in Lean 4 against Mathlib (Lean 4.19.0).

Results

They prove R_K(⟨3,2,m⟩) > 24m/5 for all fields, improving prior bounds by one when m is divisible by 5, giving R_K(⟨3,2,5⟩) ≥ 25; combined with the Hopcroft-Kerr upper bound, this determines the exact rank of ⟨3,2,5⟩ as 25.