A lower bound for $⟨3,2,m⟩$ matrix multiplication

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\mathrm{/}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 $⟨3,2,5⟩$ 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.