Summary (Overview)

• Main result: The paper proves that the tensor rank of $3 \times 3$ matrix multiplication over $\mathbb{F}_2$ is at least 21, i.e., $R_{\mathbb{F}_2}(T_{\langle 3,3,3\rangle}) \geq 21$, combined with an explicit 23-term decomposition giving the interval $21 \leq R_{\mathbb{F}_2}(T_{\langle 3,3,3\rangle}) \leq 23$.
• Novel proof strategy: The proof combines quotient-rank (occupation) bounds with a split-flattening argument. At a hypothetical length of 20, these constraints force equality in matrix-rank subadditivity, which yields cross-factor algebraic relations that lead to a contradiction.
• Key structural insight: The forced matrix-rank profile $(n_1, n_2, n_3) = (16, 1, 3)$ makes the ranks of split-flattened summands sum to exactly 27 (the full rank), forcing a direct-sum decomposition and pairwise-annihilating idempotent relations.
• Formal verification: The complete proof, including all finite quotient bounds and certificates, is formalized in the Lean theorem prover, with all 13,438 modules passing kernel verification.
• Research provenance: The proof was developed by "Qiushi Engine," an autonomous AI research system, whose full research trajectory is documented alongside the paper.

Introduction and Theoretical Foundation

The paper addresses a fundamental open problem in algebraic complexity theory: determining the minimum number of scalar multiplications needed for $3 \times 3$ matrix multiplication. While Strassen's seven-product algorithm for $2 \times 2$ matrices [1] and Laderman's 23-product algorithm for $3 \times 3$ matrices [2] are known, the exact minimum for $3 \times 3$ over $\mathbb{F}_2$ remained open.

The theoretical framework combines several ingredients:

Tensor rank definition: The $3 \times 3$ multiplication tensor is defined as

$$T_{\langle 3,3,3\rangle} = \sum_{i,j,k=0}^{2} E_{ij} \otimes E_{jk} \otimes E_{ik} \in V \otimes V \otimes V,\tag{2.1}$$

where $V = M_3(\mathbb{F}_2)$ and $E_{ij} = e_i e_j^T$. A decomposition of length $r$ is an identity

$$T_{\langle 3,3,3\rangle} = \sum_{t=1}^{r} A_t \otimes B_t \otimes C_t, \quad A_t, B_t, C_t \in V.\tag{2.2}$$

Occupation inequality (Lemma 2.2): For a subspace $W \leq V$ and a length-$r$ decomposition, if $m(W) = |\{t : A_t \in W\}|$, then

$$m(W) \leq r - R_{\mathbb{F}_2}(T_W).\tag{2.4}$$

Split flattening: The $A$-split flattening maps the tensor to a $27 \times 27$ matrix $P = \Phi_A(T_{\langle 3,3,3\rangle})$ which is a permutation matrix of rank 27. For a simple tensor, $M(A,B,C) = A \otimes (\text{vec}(B)\text{vec}(C)^T)$ with $\text{rank}\, M(A,B,C) = \text{rank}\, A$.

The prior state of the art included Bläser's substitution argument giving the classical lower bound 19 [5], and Wang's automated framework raising the binary lower bound to 20 [8]. Wang later obtained the same numerical lower bound of 21 via capacity-constrained profile enumeration [4], but the present paper identifies a different, more structural obstruction.

Methodology

The proof proceeds through several distinct stages:

1. Finite quotient bounds

The paper establishes three families of quotient-rank bounds using a frozen catalogue of 496 subspace representatives $(W_i, \ell_i)$ under the group $G$ of tensor symmetries (which has 56,448 elements):

• Line bounds: $R_{\mathbb{F}_2}(T_{\langle a\rangle}) \geq 19$ for every nonzero $a \in V$
• All-high plane bounds: For the eight two-dimensional orbits consisting of planes whose three nonzero matrices all have rank at least two, the quotient rank is at least 19
• Affine-plane span bounds: $R_{\mathbb{F}_2}(T_K) \geq 17$ for certain three-dimensional subspaces

These bounds are derived through a combination of:

• Contraction bounds: For $L \in V$ with $W \leq H_L = \{X : \langle L, X\rangle = 0\}$, contraction gives a matrix $C_L[(j,k),(i,l)] = L_{ij}\delta_{kl}$ with $\text{rank}\, C_L = 3\,\text{rank}\, L$, yielding $R_{\mathbb{F}_2}(T_W) \geq 3\,\text{rank}\, L$
• Substitution rules: A standard method where nonzero slices force elimination of summands while preserving a flattening rank lower bound
• Integer occupation certificates: Systems of inequalities on quotient classes whose infeasibility is proved via branch trees with nonnegative multiplier combinations

2. Geometric reduction

For a hypothetical length-20 decomposition, the line cap $20 - 19 = 1$ forces all 20 first factors to be distinct. The all-high plane bounds force any two distinct high-rank factors $a, b$ (rank ≥ 2) to satisfy $\text{rank}(a-b) = 1$ (Lemma 4.1).

The affine row or column coset lemma (Lemma 4.2) then shows that the set $\mathcal{H}$ of high-rank factors must lie in an affine row or column coset. After normalization by tensor symmetries:

$$\mathcal{H} \subseteq p + R, \qquad p = \begin{pmatrix} 0 & 0 & 0 \\ 0 & 1 & 0 \\ 0 & 0 & 1 \end{pmatrix}, \qquad R = \{e_0 w^T : w \in \mathbb{F}_2^3\}.\tag{4.4}$$

3. Forced profile

The affine-plane capacities (bound 17) imply $|\mathcal{H} \cap K_\pi| \leq 3$ for each affine plane $\pi$. Since every five-element subset of $\mathbb{F}_2^3$ contains a four-point affine plane (Lemma 4.3), this forces $|\mathcal{H}| \leq 4$. Combining with the rank budget gives the forced profile (Proposition 4.4):

$$(n_1, n_2, n_3) = (16, 1, 3), \quad \sum_t \text{rank}\, A_t = 27.\tag{4.6}$$

4. Saturation and contradiction

The rank-additive saturation lemma (Lemma 5.1) states: if $P$ is invertible, $P = \sum_t M_t$, and $\sum_t \text{rank}\, M_t = n$, then

$$M_t P^{-1} M_s = \delta_{ts} M_t.\tag{5.1}$$

The product formula (Lemma 5.2) gives the crucial identity:

$$M(A,B,C) P^{-1} M(A',B',C') = M(AB'C^T A', B, C').\tag{5.2}$$

This leads to the invertibility obstruction (Proposition 5.3): in a decomposition with nonzero factors and $\sum_t \text{rank}\, A_t = 27$, at most one first factor is invertible. But the forced profile $(16, 1, 3)$ requires three invertible first factors (rank 3), a contradiction.

Empirical Validation / Results

The paper's main theorem is:

Theorem 1.1: Every exact bilinear algorithm for $3 \times 3$ matrix multiplication over $\mathbb{F}_2$ uses at least 21 scalar multiplications:

$$R_{\mathbb{F}_2}(T_{\langle 3,3,3\rangle}) \geq 21.\tag{1.1}$$

Key quantitative results include:

Finite quotient bounds (Proposition 3.1):

• $L_0(0) = 20$, $L_0(\langle a\rangle) = 19$ for all nonzero $a$
• The eight all-high plane orbits (indices 484–491) have $L_0(W_i) = 18$ (later strengthened to 19)
• The affine-plane spans have $L_0(K) = 17$

Occupation system sizes: The eight systems (3.10) each have 127 variables and 29,210 rows, with the integer branch certificates having:

Consequences for saturated decompositions (Corollary 6.1): At length 22 with all first factors nonzero and saturated (rank sum 27), the only possible profiles are:

$$(17, 5, 0) \quad \text{or} \quad (18, 3, 1).\tag{6.1}$$

Formal verification: All 13,438 modules passed Lean kernel verification, with 89 terminal declarations replayed in six groups totaling 305,731 replayed declarations. The axiom dependencies are confined to $\{\text{propext}, \text{Classical.choice}, \text{Quot.sound}\}$.

Theoretical and Practical Implications

Theoretical significance: This work establishes a new lower bound technique that goes beyond the standard substitution and restriction methods. The key innovation is the conversion of first-factor occupation constraints into cross-factor algebraic relations via the saturation mechanism. The rank-additivity saturation lemma (Lemma 5.1) is proved over an arbitrary field and is a reusable standalone result.

The proof structure reveals a general principle: when occupation bounds force equality in a rank-subadditivity inequality, the resulting direct-sum structure imposes algebraic constraints that can contradict the forced configuration. This "equality mechanism" could potentially be applied to other tensor rank problems.

Connection to related work: The row/column-coset lemma is identified as a special case of Hua's matrix-adjacency geometry [11]. The paper also provides a public comparison with Wang's proof [4] and a review draft in Tahir's repository [10], clarifying the distinct obstruction identified here.

Practical implications for algorithm search: The result constrains the search space for exact algorithms:

• Any 22-term algorithm must have A-slot profile $(17, 5, 0)$ or $(18, 3, 1)$
• At most one first factor can be invertible in any saturated decomposition
• The positive rank excess at length 21 is characterized as $\dim \ker \Sigma = \Delta_A$ (equation 6.2), identifying precisely where the argument must be extended

Formal verification implications: The complete Lean formalization demonstrates that complex computer-assisted proofs in algebraic complexity can be fully verified. The integer branch certificates and their exhaustive case splits are checked as proof terms within Lean, not trusted outputs of external solvers.

Conclusion

The paper proves $R_{\mathbb{F}_2}(T_{\langle 3,3,3\rangle}) \geq 21$ through a structural argument that combines finite quotient bounds with algebraic saturation constraints. The proof is fully formalized in Lean, establishing a new benchmark for verified results in algebraic complexity.

Main takeaways:

1. The lower bound 21 for $3 \times 3$ matrix multiplication over $\mathbb{F}_2$ is established via a novel structural argument
2. The interval $21 \leq R_{\mathbb{F}_2}(T_{\langle 3,3,3\rangle}) \leq 23$ is confirmed with an explicit 23-term witness
3. The saturation mechanism provides a reusable technique for converting rank-budget equalities into cross-factor algebraic obstructions
4. Full formal verification in Lean ensures the correctness of all finite computations and certificates

Future directions: The paper identifies that extending the method to length 21 requires:

• Stronger occupation bounds or cross-factor relations that remain effective when the kernel $\ker \Sigma$ has small positive dimension
• The interval 21–23 leaves both improved constructions and stronger lower bounds to be determined

The research trajectory documented in Section 8 provides insight into how the proof was discovered through autonomous research, from numerical experiments on deletion criteria, through quotient cores and completion problems, to the final saturation argument on the full tensor.