The rank of 4×4 matrix multiplication over F2 is at least 35

We prove that the rank of the 4×4 matrix multiplication tensor over F2 is at least 35; the previous lower bound was 34. The bound follows by substitution from RF2(⟨3,3,4⟩) ≥ 27, which also gives RF2(⟨3,4,4⟩) ≥ 31. Each of the three bounds is one more than what follows from RF2(⟨3,3,3⟩) = 23. A flattening argument reduces the bound for ⟨3,3,4⟩ to lower bounds for two quotients of the tensor, by the span of a matrix of rank two and by the span of a matrix of rank three. These come from exhaustive searches over the possible patterns of a short decomposition, pruned by lower bounds for quotients by larger subspaces. The whole argument, including every step of the searches, is checked in the proof assistant Lean 4, with one compiled evaluation of a verified certificate checker. The previous bound is Bläser's (2003), and RF2(⟨3,3,3⟩) = 23 is proved in the author's earlier paper (arXiv:2610.11823). The best known upper bound over F2 is 47 (Fawzi et al., Nature 2022). The Lean formalization and the data it reads are in the archive at https://doi.org/10.5281/zenodo.23749574. Mathematics Subject Classification (2020): 68Q17, 15A69, 68V20.