We develop an automated framework for proving lower bounds on the bilinear complexity of matrix multiplication over finite fields. Our approach systematically combines orbit classification of the restricted first matrix and dynamic programming over these orbits with recursive substitution strategies, culminating in efficiently verifiable proof certificates. Using this framework, we obtain several new lower bounds for various small matrix formats. Most notably, we prove that the bilinear complexity of multiplying two $3 \times 3$ matrices over $\mathbb{F}_2$ is at least $20$, improving upon the longstanding lower bound of $19$ (Bläser 2003). Our search program finds the proof in under an hour on a laptop, and the resulting certificate verifies in seconds.

翻译：我们开发了一个自动化的框架，用于证明在有限域上矩阵乘法双线性复杂度的下界。该方法系统性地结合了受限第一矩阵的轨道分类、基于这些轨道的动态规划以及递归替换策略，最终生成可高效验证的证明证书。利用该框架，我们获得了多种小矩阵格式的新下界。尤为重要的是，我们证明了在$\mathbb{F}_2$上相乘两个$3 \times 3$矩阵的双线性复杂度至少为$20$，改进了长期以来$19$的下界（Bläser 2003）。我们的搜索程序在一台笔记本电脑上不到一小时即可找到该证明，生成的证书在数秒内即可完成验证。