The rank of 3×3 matrix multiplication over F2 is 23

The rank of the tensor of 3×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 F2 and among all bilinear algorithms with integer coefficients. The proof uses the substitution method in the form developed in recent work of D'Ambrosio, Wang and Yang et al.: a subspace S of the space of first factors contains at most r − R(S) first factors of a decomposition of length r, where R(S) is the rank of the tensor modulo S. We raise the known lower bounds on R(S) for 111 of Wang's 496 symmetry classes of subspaces. One of these bounds, R(S) ≥ 21 for a point spanned by a matrix of rank one, forces the 22 first factors of a decomposition of length 22 to be distinct. A 27×27 flattening of the tensor gives further constraints on the ranks of the first factors, and a separate enumeration shows that, when at least 14 first factors have rank one, no line in a certain orbit of lines contains two first factors. A computer search then lists, up to symmetry, all sets of 22 matrices that satisfy these constraints, and 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 by checkers whose soundness is proved in Lean. The largest checks are evaluated as compiled code, so the proof relies on the Lean compiler in addition to its kernel. Mathematics Subject Classification (2020): 68Q17, 15A69; 68V05, 68V15.