Automated Lower Bounds for Small Matrix Multiplication Complexity over Finite Fields

TL;DR

This paper introduces an automated framework to establish lower bounds on the bilinear complexity of small matrix multiplication over finite fields, achieving new bounds with efficient verification.

Contribution

It presents a novel automated method combining orbit classification and dynamic programming to improve lower bounds for matrix multiplication complexity.

Findings

Proved the bilinear complexity of 3x3 matrix multiplication over GF(2) is at least 20.

Developed a framework that produces verifiable proof certificates.

Found the proof in under an hour on a laptop, with quick certificate verification.

Abstract

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.