Automated Lower Bounds for Small Matrix Multiplication Complexity over Finite Fields

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\"aser 2003). Our search program finds the proof in under an hour on a laptop, and the resulting certificate verifies in seconds.