The rank of the tensor of $3\times 3$ matrix multiplication over the field with two elements is at most $23$ by Laderman's algorithm, and Rudich and Rousseau recently proved that it is at least $22$. We prove that it equals $23$. Hence Laderman's algorithm uses the fewest multiplications among all bilinear algorithms over $\mathbb{F}_2$ and among all bilinear algorithms with integer coefficients. The proof uses the substitution method in the form developed by D'Ambrosio, Wang and Yang et al., which bounds the number of first factors of a decomposition that lie in a given subspace of the space of first factors. We sharpen these bounds for $111$ of Wang's $496$ classes of subspaces, constrain the ranks of the first factors through a $27\times 27$ flattening of the tensor, and list, up to symmetry, all sets of $22$ first factors that satisfy these constraints. An exact completion search shows that none of them is the set of first factors of a decomposition. The computation emits certificates, which are checked in the Lean 4 proof assistant. In one formal proof the largest checks are evaluated as compiled code, and in a second one the kernel evaluates every check, so that its final theorem depends only on the three standard axioms of Lean. The Lean proofs build on the formalization of Rudich and Rousseau and import their table of bounds and their reduction for block algorithms.

翻译：暂无翻译