$\langle 3,2,m \rangle$ 矩阵乘法的下界
A lower bound for $\langle 3,2,m \rangle$ matrix multiplication
浏览论文内容
中文总结 AI 辅助
本文证明任意域上 $3\times2$ 与 $2\times m$ 矩阵乘法的双线性复杂度下界为 $24m/5$，结合上界确定 $\langle3,2,5\rangle$ 张量秩为 $25$，并用 Lean 4 形式化验证。
中文摘要 AI 辅助
我们证明，在任意域上，将一个 $3\times 2$ 矩阵与一个 $2\times m$ 矩阵相乘的双线性复杂度严格大于 $24m/5$。特别地，任何用于计算 $3\times 2$ 矩阵与 $2\times 5$ 矩阵相乘的精确双线性算法至少需要 $25$ 次乘法。结合 Hopcroft-Kerr 上界，这证明了 $\langle 3,2,5\rangle$ 矩阵乘法张量的秩恰好为 $25$。该证明已在 Lean 4 中形式化验证，形式化内容可在该 https URL 获取。
英文摘要
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.
发表机构
- HSE University（高等经济大学）
机构由 AI 辅助整理，请以论文原文为准。
