Exact minimal multiplications found for specific small matrix product
A lower bound for $\langle 3,2,m \rangle$ matrix multiplication
Computational ComplexityData Structures and Algorithms
Summary
Figuring out the smallest number of multiplications needed to multiply matrices is important for speeding up calculations in many computer programs. The authors proved the exact minimum number of multiplications needed to multiply a 3-by-2 matrix by a 2-by-5 matrix, showing it cannot be done with fewer than 25 multiplications. This matches a previously known upper limit, so the exact minimal cost is now known. They also double-checked their proof using computer verification to ensure it is correct.
What this means in practice
- •For algorithm designers: Know precisely how efficient exact algorithms for multiplying 3x2 by 2x5 matrices can be, guiding optimal algorithm development.
- •For mathematics software developers: Use the verified proof to build more reliable and efficient matrix multiplication libraries with guarantees on minimal computation.
A theory result. No direct application yet.
Authors
Askar Tsyganov, Uliana Parkina, Sergey Samsonov, Maxim Rakhuba
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.