We introduce a new method for proving bilinear complexity lower bounds for matrix multiplication over finite fields. The approach combines the substitution method with a systematic backtracking search over linear restrictions on the first matrix $A$ in the product $AB = C^T$. We enumerate restriction classes up to symmetry; for each class we either obtain a rank lower bound by classical arguments or branch further via the substitution method. The search is organized by dynamic programming on the restricted matrix $A$. As an application we prove that the bilinear complexity of multiplying two $3 \times 3$ matrices over $\mathbb{F}_2$ is at least $20$, improving the longstanding lower bound of $19$ (Bläser 2003). The proof is found automatically within 1.5 hours on a laptop and verified in seconds.

翻译：我们提出了一种新方法，用于证明有限域上矩阵乘法双线性复杂度的下界。该方法将替换技术与对乘积 \(AB = C^T\) 中第一个矩阵 \(A\) 的线性约束进行系统性回溯搜索相结合。我们枚举了对称性下的约束类别；对于每个类别，我们或通过经典论证获得秩下界，或通过替换方法进一步分支。该搜索通过受限矩阵 \(A\) 上的动态规划进行组织。作为应用，我们证明了在 \(\mathbb{F}_2\) 上相乘两个 \(3 \times 3\) 矩阵的双线性复杂度至少为 \(20\)，这改进了长期存在的下界 \(19\)（Bläser 2003）。该证明在笔记本电脑上于 1.5 小时内自动完成，并在数秒内得到验证。