\documentclass[11pt]{article}

\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{mathtools}
\usepackage{booktabs}
\usepackage{array}
\usepackage{enumitem}
\usepackage{microtype}
\usepackage[hidelinks]{hyperref}

\hypersetup{
  pdftitle={The rank of 4x4 matrix multiplication over F2 is at least 35},
  pdfauthor={Tejasvi Singh Tomar (ORCID 0000-0003-4668-3639)},
}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{remark}[theorem]{Remark}

\DeclareUnicodeCharacter{2080}{\ensuremath{{}_0}}
\DeclareUnicodeCharacter{2081}{\ensuremath{{}_1}}
\DeclareUnicodeCharacter{2082}{\ensuremath{{}_2}}
\DeclareUnicodeCharacter{2192}{\ensuremath{\to}}
\DeclareUnicodeCharacter{2115}{\ensuremath{\mathbb{N}}}
\DeclareUnicodeCharacter{2203}{\ensuremath{\exists}}
\DeclareUnicodeCharacter{2211}{\ensuremath{\textstyle\sum}}
\DeclareUnicodeCharacter{2227}{\ensuremath{\wedge}}
\DeclareUnicodeCharacter{00AC}{\ensuremath{\neg}}

\newcommand{\F}{\mathbb{F}}
\newcommand{\Ft}{\mathbb{F}_2}
\newcommand{\Rk}{\mathrm{R}}
\newcommand{\mm}[3]{\langle #1,#2,#3\rangle}
\newcommand{\GL}{\mathrm{GL}}
\newcommand{\spn}{\operatorname{span}}
\newcommand{\rk}{\operatorname{rk}}
\newcommand{\lb}{\operatorname{lb}}
\newcommand{\cp}{\operatorname{cap}}
\newcommand{\lean}[1]{\texttt{#1}}

\title{The rank of $4\times4$ matrix multiplication over $\mathbb{F}_2$ is at least 35}
\author{Tejasvi Singh Tomar\thanks{ORCID: \href{https://orcid.org/0000-0003-4668-3639}{0000-0003-4668-3639}.}}
\date{}

\begin{document}
\maketitle

\begin{abstract}
We prove that the rank of the $4\times4$ matrix multiplication tensor over $\Ft$ is at least $35$; the previous lower
bound was $34$. The bound follows by substitution from $\Rk_{\Ft}(\mm334)\ge27$, which also gives
$\Rk_{\Ft}(\mm344)\ge31$. Each of the three bounds is one more than what follows from $\Rk_{\Ft}(\mm333)=23$. A
flattening argument reduces the bound for $\mm334$ 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.
\end{abstract}

\noindent\textbf{Keywords:} matrix multiplication, tensor rank, bilinear complexity, lower bounds, finite fields,
computer-assisted proof, Lean.\\
\textbf{MSC 2020:} 68Q17, 15A69, 68V20.

\section{Introduction}

The rank $\Rk(\mm nmp)$ of the matrix multiplication tensor $\mm nmp$ is the least number of multiplications in a
bilinear algorithm for the product of an $n\times m$ and an $m\times p$ matrix. An algorithm for a small format can
be applied recursively to the blocks of large matrices, as Strassen's algorithm for $2\times2$ matrices is
\cite{Str69}, so the ranks of small formats also bear on the multiplication of large matrices. Even for $4\times4$
matrices the gap between the known bounds is wide. Over $\Ft$ computation enters on both sides of the gap: the best
algorithm, with $47$ multiplications, was
found by a search over $\Ft$ \cite{FBH22} (outside characteristic two the best known algorithm uses $48$
\cite{Nov25,DPS25}), and since a decomposition over $\Ft$ is a finite object, lower bounds can be attacked by
exhaustive computation. The best lower bound has been $34$. This value is the case $m=n=4$ of
Bl\"aser's inequality $\Rk(\mm nmn)\ge2mn+2n-m-2$ for $m\ge n\ge3$ \cite{Bla03}, and over $\Ft$ it also follows from
the recent determination of $\Rk_{\Ft}(\mm333)$, as we explain next.

Computer-assisted proofs have recently raised the lower bounds over $\Ft$ for several small formats. Wang
\cite[Theorem~1]{Wan26a} proved $\Rk_{\Ft}(\mm334)\ge25$ and $\Rk_{\Ft}(\mm344)\ge29$, above the values $24$ and $28$
of Bl\"aser's inequalities \cite{Bla03,Bla99}. For $\mm333$ the lower bound over $\Ft$ rose from $19$~\cite{Bla03} to
$20$~\cite{Wan26a}, $21$~\cite{Wan26b,Yan26}, $22$~\cite{RR26} (proved there over $\Ft$ and then for integer
coefficients) and $23$~\cite{Tom26}, which is the rank by Laderman's algorithm~\cite{Lad76}. The substitution step of
Lemma~\ref{lem:chain} turns $\Rk_{\Ft}(\mm333)=23$ into $\Rk_{\Ft}(\mm334)\ge26$, $\Rk_{\Ft}(\mm344)\ge30$ and
$\Rk_{\Ft}(\mm444)\ge34$. We improve each of these bounds by one.

\begin{theorem}\label{thm:main}
Over $\Ft$, $\Rk(\mm334)\ge27$, $\Rk(\mm344)\ge31$ and $\Rk(\mm444)\ge35$.
\end{theorem}

In particular, $35$ is the first lower bound above $34$ for the rank of $4\times4$ matrix multiplication over $\Ft$. A
decomposition with integer coefficients reduces modulo $2$ to a decomposition over $\Ft$ of the same length, so the
three bounds also hold for bilinear algorithms with integer coefficients. Over $\Ft$ the three ranks now lie between
$27$ and $29$, between $31$ and $38$, and between $35$ and $47$; the upper bounds $29$ and $38$ are due to
Smirnov~\cite{Smi13}.

The proof starts from a flattening. Write a decomposition as $\mm334=\sum_t a_t\otimes b_t\otimes c_t$ with $a_t$ a
$3\times3$ matrix. Grouping the row index of $a_t$ with the second factor and its column index with the third turns
$\mm334$ into a $36\times36$ matrix of full rank, to which each term contributes at most $\rk(a_t)$
(Lemma~\ref{lem:flat}). So a decomposition with at most $26$ terms has a term whose first factor has rank two or
three. Up to the symmetries $a\mapsto PaQ$ with $P,Q$ invertible there are only two such matrices, $v_2$ and $v_3$,
and a term with first factor $v$ vanishes in the quotient of $\mm334$ by $\spn(v)$. The first bound therefore follows
once each of the two quotients is shown to have rank at least $26$.

These two quotient bounds are the computational core. A short decomposition of the quotient by a subspace $E$
determines a multiset of cosets of $E$, its \emph{profile}, and the profile must respect a \emph{cap} for every larger
subspace $S$: the number of its elements in $S$ is at most the length minus a lower bound for the quotient by $S$. We
enumerate every profile that meets all caps, up to the symmetries that fix $E$, and refute the survivors: for $v_3$
there are none, and for $v_2$ there is one. The caps need lower bounds for the quotients by larger subspaces, which we
prove by induction on the dimension, about half of them by searches of the same kind.

We assume no earlier lower bound; the bounds whose values come from earlier work are proved again here. The approach
builds on the recent proofs for $\mm333$. Caps, coset profiles and the symmetry-reduced enumeration of profiles come
from D'Ambrosio~\cite{DAm26}, Wang~\cite{Wan26a,Wan26b} and Yang et al.~\cite{Yan26}. The tables of subspace bounds
and the forced-product argument come from Wang's framework~\cite{Wan26a}, and most of the bounds for larger subspaces
have the values his program computes. Yang et al.~\cite{Yan26} introduced the split flattening, of which
Lemma~\ref{lem:flat} is the analogue for $\mm334$; they also exclude profiles by weighted counting over covers of a
quotient, with certificates made of nonnegative multipliers, and our pruning step (Section~\ref{sec:search}) and the
coset counting of Section~\ref{sec:table} are of this kind. The refutation of the surviving profiles by an exhaustive
search with branching certificates follows~\cite{Tom26}; case analyses that branch on the second and third factors also
occur in the Lean proof of~\cite{RR26}.

The proof, with its searches and certificates, is checked in Lean~4 with Mathlib~\cite{dMU21,mC20}. Besides the Lean
kernel, its trust base contains one evaluation by Lean's compiler of a certificate checker that is itself proved
sound, and that evaluation must be trusted to agree with the kernel (Section~\ref{sec:lean}).
Section~\ref{sec:setting} fixes the notation,
Section~\ref{sec:reduction} reduces the theorem to the two quotient bounds, Section~\ref{sec:search} describes the
searches, Section~\ref{sec:table} the bounds for larger subspaces, Section~\ref{sec:certs} the certificates for the
leaves of the searches, Section~\ref{sec:lean} the formal proof, and Section~\ref{sec:remarks} some open questions.

\section{Setting}\label{sec:setting}

All vector spaces are over $\Ft$. Let $A=\Ft^{3\times3}$, $B=\Ft^{3\times4}$ and $C=\Ft^{4\times3}$, with standard
bases $E_{ij}$, $F_{jk}$ and $G_{ki}$. The tensor is
\[
T=\mm334=\sum_{i,j<3,\;k<4} E_{ij}\otimes F_{jk}\otimes G_{ki}\in A\otimes B\otimes C ,
\]
and in general $\mm nmp=\sum_{i<n,\,j<m,\,k<p}E_{ij}\otimes F_{jk}\otimes G_{ki}$, with the matrix units of the
spaces of $n\times m$, $m\times p$ and $p\times n$ matrices. A \emph{decomposition} of length $r$ is an equation
$T=\sum_{t=1}^r a_t\otimes b_t\otimes c_t$, and $\Rk(T)$ is the least length. For a subspace $S\subseteq A$ let
$T\bmod S=(\pi_S\otimes1\otimes1)(T)$, where $\pi_S:A\to A/S$ is the quotient map. A subspace of dimension one is a
\emph{point}.

\begin{lemma}\label{lem:quot}
$\Rk(T\bmod S)$ is the least number of terms with $a_t\notin S$, over all decompositions of $T$.
\end{lemma}

\begin{proof}
Applying $\pi_S\otimes1\otimes1$ to a decomposition kills the terms with $a_t\in S$. Conversely, lift a shortest
decomposition of $T\bmod S$ term by term; the difference from $T$ lies in $S\otimes B\otimes C$ and is a sum of terms
whose first factors lie in $S$.
\end{proof}

We write $\mathrm{QuotLB}(S,k)$ for the statement that every decomposition of $T$ has at least $k$ terms with first
factor outside $S$; by Lemma~\ref{lem:quot} it says $\Rk(T\bmod S)\ge k$. This form needs no quotient spaces, and it
is the one we formalize.

\paragraph{Symmetry.} For $P,Q\in\GL_3(\Ft)$ the map $(a,b,c)\mapsto(PaQ,\,Q^{-1}b,\,cP^{-1})$ fixes $T$, so it maps
decompositions to decompositions of the same length, and it maps the terms with $a_t\in S$ to the terms with
$a_t\in PSQ$. Hence $\mathrm{QuotLB}(S,k)$ and $\mathrm{QuotLB}(PSQ,k)$ are equivalent. We write $G_0$ for this group
acting on $A$; it has order $28{,}224$. The map $(a,b,c)\mapsto(a^{\mathsf T},c^{\mathsf T},b^{\mathsf T})$ is also a
symmetry of $T$; we do not use it, since the arguments below work with any group of symmetries. The nonzero matrices fall into three $G_0$-orbits, by rank, with $49$, $294$
and $168$ elements; we fix the representatives
\[
v_2=E_{01}+E_{10}\quad(\text{rank }2),\qquad v_3=E_{02}+E_{11}+E_{20}\quad(\text{rank }3).
\]

\section{Reduction to two quotients}\label{sec:reduction}

\begin{lemma}[split flattening]\label{lem:flat}
Every decomposition $T=\sum_t a_t\otimes b_t\otimes c_t$ satisfies $\sum_t\rk(a_t)\ge36$.
\end{lemma}

\begin{proof}
Identify $A$ with $U\otimes V$, where $U=V=\Ft^3$ carry the row and column index, and regroup $A\otimes B\otimes C$ as
$(U\otimes B)\otimes(V\otimes C)$. This regrouping is linear and turns each tensor into a $36\times36$ matrix with rows
indexed by pairs $(i,y)$ and columns by pairs $(j,z)$, where $y$ and $z$ run over the standard bases of $B$ and $C$.
The image of $T$ is $\sum_{i,j,k}(e_i\otimes F_{jk})\otimes(e_j\otimes G_{ki})$; since $(i,j,k)\mapsto(i,(j,k))$ and
$(i,j,k)\mapsto(j,(k,i))$ are both bijections onto $[3]\times[12]$, it is a permutation matrix, of rank $36$. The image
of $a\otimes b\otimes c$ is the Kronecker product of $a$ with the rank-one matrix $bc^{\mathsf T}$, of rank at most
$\rk(a)$. Subadditivity of rank gives the claim.
\end{proof}

The choice of pairing matters, since grouping the row index of $a$ with $C$ instead gives a matrix of rank only~$4$.

\begin{proposition}\label{prop:twocase}
If $\mathrm{QuotLB}(\spn(v_2),26)$ and $\mathrm{QuotLB}(\spn(v_3),26)$ hold, then $\Rk(T)\ge27$.
\end{proposition}

\begin{proof}
Take a decomposition with at most $26$ terms. By Lemma~\ref{lem:flat} the ranks of the first factors sum to at least
$36$, so some $a_{t_0}$ has rank two or three. Apply the symmetry $(P,Q)$ that sends $a_{t_0}$ to $v_2$ or $v_3$. In
the new decomposition the first factor of term $t_0$ lies in $\spn(v)$, so at most $25$ first factors lie outside it,
which contradicts the hypothesis for $v$.
\end{proof}

The two hypotheses are proved in Sections~\ref{sec:search}--\ref{sec:certs}. The other two bounds follow by the
substitution method~\cite{Pan66}; we recall the step in the form we use.

\begin{lemma}\label{lem:chain}
If $\mm nm{p+1}$ has a decomposition of length $r+m$, then $\mm nmp$ has one of length at most $r$. Moreover
$\Rk(\mm nmp)=\Rk(\mm mpn)$.
\end{lemma}

\begin{proof}
Write $\mm nm{p+1}=\sum_{j,k}F_{jk}\otimes M_{jk}$ with $M_{jk}=\sum_iE_{ij}\otimes G_{ki}$. The $m$ slices $M_{j,p}$
are linearly independent, so in any decomposition there are $m$ terms whose second factors restrict to a basis of the
coordinates $F_{\cdot,p}$; together with the $F_{jk}$, $k<p$, these $m$ second factors form a basis of the second
factor space, so the following linear map exists. The linear map of the second factor space that fixes every $F_{jk}$ with $k<p$ and sends
these $m$ second factors to zero removes those $m$ terms and adds multiples of the $M_{j',p}$ to the other slices.
Those multiples involve only the last row of the third matrix, and setting that row to zero is a linear map that turns
the result into a decomposition of $\mm nmp$ of length at most $r$. The cyclic statement holds because
$(a,b,c)\mapsto(b,c,a)$ maps decompositions of $\mm nmp$ to decompositions of $\mm mpn$.
\end{proof}

\begin{proof}[Proof of Theorem~\ref{thm:main}, given the two quotient bounds]
Proposition~\ref{prop:twocase} gives $\Rk(\mm334)\ge27$. If $\mm344$ had a decomposition of length $30=26+4$, then
Lemma~\ref{lem:chain} would give one of $\mm343$ of length at most $26$, and by cyclic invariance one of $\mm334$; so
$\Rk(\mm344)\ge31$. In the same way a decomposition of $\mm444$ of length $34$ would give one of $\mm344$ of length at
most $30$, so $\Rk(\mm444)\ge35$.
\end{proof}

\section{Lower bounds for quotients by a search}\label{sec:search}

Fix a subspace $E\ne A$ and a length $L$. To prove $\mathrm{QuotLB}(E,L+1)$ we suppose that some decomposition of
$T$ has at most $L$ terms with first factor outside $E$. Two simple observations restrict what such a decomposition
can look like.

\begin{lemma}[padding]\label{lem:pad}
If some decomposition of $T$ has at most $L$ terms outside $E$, then some decomposition has exactly $L$ terms outside
$E$, and in each of them $a_t$, $b_t$, $c_t$ are nonzero.
\end{lemma}

\begin{proof}
Drop zero terms. Some term lies outside $E$, because a functional on $A$ that vanishes on $E$ but not on all of $A$
sees a nonzero slice of $T$. While fewer than $L$ terms are outside $E$, split one of them as
$a\otimes b\otimes c=a\otimes b\otimes c'+a\otimes b\otimes(c+c')$ with $c'\notin\{0,c\}$.
\end{proof}

\begin{lemma}[caps]\label{lem:cap}
Let $E\subsetneq S\subseteq A$, and let $\lb(S)$ be a number for which $\mathrm{QuotLB}(S,\lb(S))$ holds. In a
decomposition with exactly $L$ terms outside $E$, at most $L-\lb(S)$ of those terms have $a_t\in S$.
\end{lemma}

\begin{proof}
Every term outside $S$ is outside $E$, so the number of terms outside $S$ is $L$ minus the number of outside terms in
$S$, and it is at least $\lb(S)$.
\end{proof}

The \emph{profile} of such a decomposition is the multiset of the cosets $a_t+E$ of its $L$ outside terms. By
Lemma~\ref{lem:cap}, for every strict superspace $S$ of $E$ at most $\cp(S)=L-\lb(S)$ elements of the profile lie in
$S/E$. For a point $E$ there are $417{,}198$ strict superspaces. Section~\ref{sec:table} explains where their bounds
come from.

\paragraph{Enumeration.} Number the nonzero cosets of $E$ ($255$ of them when $E$ is a point), and write a profile as
the nondecreasing sequence of the numbers of its elements. Let $H$ be a subgroup of the stabilizer of $E$ in $G_0$;
for the two points we take the whole stabilizer, of order $96$ for $v_2$ and $168$ for $v_3$, and for the searches of
Section~\ref{sec:table} the stabilizer or, when that is large, its subgroup that also fixes a few cosets. The group $H$
permutes
the cosets, and we call a sorted sequence \emph{canonical} if no element of $H$ maps it to a lexicographically smaller
sorted sequence.

\begin{lemma}\label{lem:orderly}
Every prefix of a canonical sequence is canonical.
\end{lemma}

\begin{proof}
Let $s=(s_1\le\dots\le s_L)$ be canonical, and suppose that some $h\in H$ maps a prefix $(s_1,\dots,s_k)$ to a sorted
sequence $(u_1\le\dots\le u_k)$ that is lexicographically smaller. Let $i$ be the first index with $u_i\ne s_i$, so
that $u_i<s_i$. For $j\le k$ the multiset $h(s)$ contains $u_1,\dots,u_j$, so its $j$-th smallest element is at most
$u_j$. Hence the sorted form of $h(s)$ is at most $s_j$ at every position $j<i$ and smaller than $s_i$ at position
$i$, so it is lexicographically smaller than $s$, which contradicts the canonicity of $s$.
\end{proof}

The search builds sorted sequences one element at a time. It discards a sequence if some element of $H$ maps it to a
lexicographically smaller sorted sequence. It also discards a sequence when the caps leave no room to complete it.
Suppose that $\rho$ elements remain to be chosen, and give each coset $\gamma$ that may still be chosen (no coset
before the last chosen one may) a variable $x_\gamma$, the number of its further copies, with $0\le x_\gamma\le
u_\gamma$. The bound $u_\gamma$ starts as the cap of $E+\langle\gamma\rangle$, decreases as copies of $\gamma$ are
chosen, drops to $0$ when some cap containing $\gamma$ is full, and can be lowered further by earlier pruning steps;
in every case no completion uses more than $u_\gamma$ further copies of $\gamma$. Let $b_S$ be the room that the cap
of $S$ leaves. A completion gives a solution of $\sum_\gamma x_\gamma=\rho$ and $\sum_{\gamma\subseteq S}x_\gamma\le
b_S$ for all $S$. For every vector $y\ge0$ indexed by the superspaces $S$, every such solution satisfies
\[
\rho=\sum_\gamma x_\gamma\le\sum_Sy_Sb_S+\sum_\gamma u_\gamma\max\Bigl(0,\,1-\sum_{S\supseteq\gamma}y_S\Bigr),
\]
since $\sum_\gamma x_\gamma\sum_{S\supseteq\gamma}y_S=\sum_Sy_S\sum_{\gamma\subseteq S}x_\gamma\le\sum_Sy_Sb_S$ and
$x_\gamma\bigl(1-\sum_{S\supseteq\gamma}y_S\bigr)\le u_\gamma\max\bigl(0,1-\sum_{S\supseteq\gamma}y_S\bigr)$. So a
vector $y$ for which the right side is smaller than $\rho$ proves that no completion exists. The search obtains $y$
from the dual of the linear relaxation, solved by a dense simplex method with HiGHS~\cite{HH18} as a fallback, scales
it to integers and records it, and the inequality is checked in exact integer arithmetic, so a pruning step can be
rechecked without solving anything. Inequalities of this kind, with recorded nonnegative multipliers, are used by
Yang et al.\ \cite[Sections~3.2--3.3]{Yan26}. Here the multipliers come from a linear-programming solver.

\paragraph{Coverage and leaves.} The enumeration is cut into jobs, and each job records its part of the search tree,
with every branching decision and every dual vector, as a block of a proof trace (the Lean copy of each block adds the
group element behind each discard). A trace
proves that no further profile exists only if its blocks together cover the whole search tree, that is, every subtree
that one block delegates is the root of another block. A canonical sequence of length $L$ that meets all caps is a
\emph{leaf}. For each leaf one must decide whether $T\bmod E$ has a decomposition whose first factors are the cosets of
the profile, one term for each element of the profile. Restricting $T$ to the functionals that vanish on $E$ turns this
\emph{leaf question} into a question about $L$ pairs of vectors $(b_t,c_t)$ in $\Ft^{12}\times\Ft^{12}$, whose sums of
outer products must match the slices of $T$. Section~\ref{sec:certs} refutes the leaf questions with certificates, and
Table~\ref{tab:search} gives the size of the searches.

\begin{proposition}\label{prop:search}
Let $E\ne A$, let $H$ be a subgroup of the stabilizer of $E$ in $G_0$, and suppose that every cap comes from a valid
bound $\lb(S)$. If the trace of the search covers its search tree and no leaf question has a solution, then
$\mathrm{QuotLB}(E,L+1)$ holds.
\end{proposition}

\begin{proof}
Otherwise Lemma~\ref{lem:pad} gives a decomposition with exactly $L$ terms outside $E$, all with nonzero factors. Its
profile respects every cap by Lemma~\ref{lem:cap}. Some $h\in H$ maps the profile to a canonical one. Applying $h$ to
the decomposition gives a decomposition with exactly $L$ terms outside $h(E)=E$ whose profile is the canonical one,
so by Lemma~\ref{lem:cap} that profile also respects every cap. By
Lemma~\ref{lem:orderly} no prefix of the canonical profile is discarded for symmetry, and no prefix is discarded by the
caps, so by coverage the search reaches it as a leaf. The transformed decomposition solves that leaf question, a
contradiction.
\end{proof}

The two point searches take $L=25$. The search for a larger subspace $E$ in Section~\ref{sec:table} takes
$L=\lb(E)-1$. On a machine with $180$ virtual cores, each point search finished in about half an hour.

\begin{table}[ht]
\centering
\begin{tabular}{lrrrr}
\toprule
search & searches & trace blocks & nodes & leaves \\
\midrule
$E=\spn(v_3)$, $L=25$ & $1$ & $137{,}442$ & $12{,}833{,}599$ & $0$ \\
$E=\spn(v_2)$, $L=25$ & $1$ & $7{,}296$ & $1{,}529{,}941$ & $1$ \\
larger subspaces & $367$ & $55{,}615$ & $15{,}162{,}772$ & $14{,}121$ \\
\bottomrule
\end{tabular}
\caption{The searches. Nodes are counted as recorded in the proof traces, where the root of a delegated subtree
appears in two blocks; leaves are counted once each. Of the $367$ searches for larger subspaces, $48$ have leaves; the largest, for a subspace of
dimension $3$, has $2{,}804{,}206$ nodes and $5{,}440$ leaves.}
\label{tab:search}
\end{table}

\section{Bounds for larger subspaces}\label{sec:table}

The caps need lower bounds $\lb(S)$ for the quotients by subspaces of dimension $2$ to $9$. Up to $G_0$ there are
$706$ classes of such subspaces. Four of them consist of subspaces of matrices of rank at most one, so none of their
members contains $v_2$ or $v_3$; the two point searches need the other $702$. For $628$ of these the value of $\lb(S)$
is the bound that Wang's program computes~\cite{Wan26a}. (Wang's entries impose $d$ linear constraints on the first
input; substituting them into the tensor is the reduction modulo the span $S$ of the constraint vectors, so an entry
with $d$ constraints corresponds to a class of subspaces of dimension $d$ here.) For the other $74$ we prove higher
values, first suggested by
bounds for quotients of $\mm333$~\cite{RR26,Tom26} or found by our own searches. Each value is proved by one of five
kinds of argument. Table~\ref{tab:classes} shows how they are distributed over the dimensions.

\begin{enumerate}[leftmargin=*]
\item \emph{Flattening.} Each term contributes rank at most one to each of the three flattenings of $T\bmod S$; for
  $18$ classes the largest flattening rank is the bound.
\item \emph{Forced products.} For $21$ classes we use Wang's forced-product argument~\cite{Wan26a}. Let $T'=T\bmod S$,
  and let $\varphi_1,\dots,\varphi_f$ be functionals on one of the factors, say $B$, whose slices $T'(\varphi_i)$ are
  linearly independent. Extend them to a basis $\varphi_1,\dots,\varphi_{12}$ of $B^*$ with dual basis
  $\beta_1,\dots,\beta_{12}$. In a decomposition of $T'$ of length $r$, some $f$ terms $t_1,\dots,t_f$ satisfy
  $\det(\varphi_i(b_{t_j}))\ne0$. The linear map of $B$ that kills $b_{t_1},\dots,b_{t_f}$ and fixes
  $\beta_{f+1},\dots,\beta_{12}$ sends each $\beta_i$ with $i\le f$ to $\sum_{l>f}\alpha_{il}\beta_l$ for some matrix
  $\alpha$, and it turns the decomposition into one of length $r-f$ of
  $T'_\alpha=\sum_{l>f}\beta_l\otimes\bigl(T'(\varphi_l)+\sum_{i\le f}\alpha_{il}T'(\varphi_i)\bigr)$; this is a
  substitution step in the style of Hopcroft and Kerr~\cite{HK71}. A flattening of $T'_\alpha$, or of the tensor formed
  by some of its slices, has the form $M(\alpha)=M_0+\sum_m\alpha_mN_m$, so $r\ge f+\min_\alpha\rk M(\alpha)$, and it
  suffices that $M(\alpha)$ has rank at least $\lb(S)-f$ for every $\alpha$. Wang checks this by enumerating the values
  of $\alpha$. We certify it with witnesses instead: a set $J$ of $\lb(S)-f$ columns and, for every nonzero vector $z$
  supported on $J$, a vector $y_z$ with $y_z^{\mathsf T}M_0z=1$ and $y_z^{\mathsf T}N_mz=0$ for all $m$. Then
  $y_z^{\mathsf T}M(\alpha)z=1$, so $M(\alpha)z\ne0$ for every $\alpha$ and every such $z$, and the columns in $J$ stay
  linearly independent (some classes use the same condition with rows and columns exchanged). The factor, the
  functionals, the flattening and the witnesses for each class are part of the formal proof.
\item \emph{Coset counting.} One class of subspaces $S$ of dimension $6$ has its bound from the seven subspaces
  $S+\langle c\rangle$, one for each nonzero coset $c$ of $S$, which lie in three classes of dimension $7$. Every matrix
  outside $S$ lies in exactly one of them, so in a decomposition with $r$ terms outside $S$ each of these terms lies
  outside six of the seven subspaces, and $6r\ge\sum_c\lb(S+\langle c\rangle)$.
\item \emph{Transport.} For $295$ classes a symmetry in $G_0$ maps the subspace into a subspace of larger dimension
  whose bound is known. A first factor outside the larger subspace is outside the smaller one, so the bound transfers.
\item \emph{Search.} The remaining $367$ classes get their bounds from searches as in Section~\ref{sec:search}, with
  $E$ the subspace itself.
\end{enumerate}

A search for a subspace of dimension $d$ uses only bounds for subspaces of dimension greater than $d$, and transport
and coset counting also go to larger dimensions. The bounds are therefore proved by induction on the dimension,
downward from the full space.

\begin{table}[ht]
\centering
\begin{tabular}{crrrrrr}
\toprule
dimension & flattening & forced products & coset counting & transport & search & total \\
\midrule
$2$ & & & & & $15$ & $15$ \\
$3$ & & & & $48$ & $45$ & $93$ \\
$4$ & & & & $88$ & $151$ & $239$ \\
$5$ & & $2$ & & $128$ & $109$ & $239$ \\
$6$ & $5$ & $14$ & $1$ & $31$ & $44$ & $95$ \\
$7$ & $9$ & $5$ & & & $3$ & $17$ \\
$8$ & $3$ & & & & & $3$ \\
$9$ & $1$ & & & & & $1$ \\
\midrule
total & $18$ & $21$ & $1$ & $295$ & $367$ & $702$ \\
\bottomrule
\end{tabular}
\caption{The $702$ classes of subspaces whose bounds the two point searches use, by dimension and by the argument that
proves the bound.}
\label{tab:classes}
\end{table}

\section{Certificates for the leaves}\label{sec:certs}

A leaf question asks for nonzero $b_t,c_t\in\Ft^{12}$, one pair for each element $a_t+E$ of the profile, with
$T(X)=\sum_{t:\,X(a_t)=1}b_tc_t^{\mathsf T}$ for every functional $X$ that vanishes on $E$. The certificates rest on
three facts about a sum of rank-one matrices.

\begin{lemma}\label{lem:rank}
Let $R=\sum_{t\in K}b_tc_t^{\mathsf T}$ with $u=|K|$ and all $b_t,c_t$ nonzero.
\begin{enumerate}[label=(\roman*)]
\item $\rk R\le u$.
\item If $\rk R=u$, then every $b_t$ lies in the column space of $R$, every $c_t$ lies in its row space, and for every
  $x$ with $Rx=b_t$ one has $c_t^{\mathsf T}x=1$ and $c_s^{\mathsf T}x=0$ for $s\ne t$; dually, $y^{\mathsf T}b_s$ is
  $1$ for $s=t$ and $0$ otherwise whenever $y^{\mathsf T}R=c_t^{\mathsf T}$.
\item If $\rk R\ge u-1$, then no $t\in K$ has both $b_t$ outside the column space of $R$ and $c_t$ outside its row
  space.
\end{enumerate}
\end{lemma}

\begin{proof}
(i) is subadditivity. For (ii), write $R=BC^{\mathsf T}$, where the columns of $B$ are the $b_t$ and those of $C$ are
the $c_t$. Since $u=\rk R\le\min(\rk B,\rk C)\le u$, both $B$ and $C$ have linearly independent columns, so the column
space of $R$ is that of $B$ and the row space of $R$ is the column space of $C$. If $Rx=b_t$, then
$B(C^{\mathsf T}x)=Be_t$, so $C^{\mathsf T}x=e_t$, which is the claim; if $y^{\mathsf T}R=c_t^{\mathsf T}$, then
$(y^{\mathsf T}B-e_t^{\mathsf T})C^{\mathsf T}=0$, so $y^{\mathsf T}B=e_t^{\mathsf T}$. For (iii), if $b_t$ and $c_t$ were outside
the column and row spaces, then $\rk(R+b_tc_t^{\mathsf T})=\rk R+1\ge u$; but $R+b_tc_t^{\mathsf T}=\sum_{s\ne t}
b_sc_s^{\mathsf T}$ has rank at most $u-1$.
\end{proof}

We refute each of the $14{,}122$ distinct leaves by a branching certificate, which fixes the pairs $(b_t,c_t)$ one
term at a time. At a node, let $R_X$ be what remains of $T(X)$ after the fixed pairs are subtracted, and apply
Lemma~\ref{lem:rank} to $R_X$ and the terms not yet fixed with $X(a_t)=1$. A node where (i) fails for some $X$ is
closed, and (ii) and (iii) restrict the column and row spaces available to the next pair. These rules leave a short
list of candidates for that pair. A node of the certificate names the term to be fixed, the functionals to which
(ii) and (iii) are applied, whether the symmetry reduction is used and whether the candidates are listed by $b$ or by
$c$ first, followed by one subtree for each candidate;
the checker computes the list of candidates itself, so a certificate cannot leave a candidate out. The maps
$b\mapsto bW$, $c\mapsto W^{-1}c$ with $W\in\GL_4(\Ft)$ fix every slice and reduce the first branching. A certificate
is checked by a program that replays the branching and verifies each rank claim by elimination. A search records a
leaf each time a job reaches it, and a job that ran past its budget and was redone in smaller pieces could record a
leaf twice. So $5{,}440$ of the $19{,}562$ certificate records repeat a leaf that already has one, $3{,}696$ of them
in the largest search and one in the search for $v_2$. Every record is checked.

The single leaf of the search for $v_2$ is a small example of the method. Its profile consists of $25$ cosets of
$\spn(v_2)$, $23$ of them distinct; Table~\ref{tab:leaf} lists a representative of each. Its certificate has $14$
nodes. At the root it branches on the term whose first factor is $E_{02}$. Two functionals $X$ are tight there, with
$\rk R_X=u_X=8$ and $\rk R_X=u_X=12$, and Lemma~\ref{lem:rank}(ii) together with the maps $b\mapsto bW$,
$c\mapsto W^{-1}c$ leaves $13$ candidates for the pair of that term. For each candidate the certificate names one more
term, with first factor $\texttt{101/000/101}$, $\texttt{111/000/111}$ or $\texttt{010/011/111}$, up to three tight
functionals and, in ten of the branches, one functional $X$ with $\rk R_X=u_X-1$; by (ii) and (iii) they leave no
candidate for the pair of that term, so every branch closes at depth one. The checker verifies $31$ rank claims in
all. The leaves of the larger searches need far larger certificates (Appendix~\ref{app:resources}).

\begin{table}[ht]
\centering
\small
\begin{tabular}{llllll}
\toprule
\texttt{010/000/000} ($\times2$) & \texttt{110/000/000} ($\times2$) & \texttt{001/000/000} & \texttt{011/000/000} &
\texttt{010/010/000} & \texttt{001/001/000} \\
\texttt{011/011/000} & \texttt{000/000/100} & \texttt{110/000/100} & \texttt{000/000/010} & \texttt{010/010/010} &
\texttt{001/000/001} \\
\texttt{000/001/001} & \texttt{000/000/101} & \texttt{101/000/101} & \texttt{010/001/101} & \texttt{111/001/101} &
\texttt{011/000/011} \\
\texttt{000/011/011} & \texttt{000/000/111} & \texttt{111/000/111} & \texttt{010/011/111} & \texttt{101/011/111} & \\
\bottomrule
\end{tabular}
\caption{The profile of the single leaf of the search for $v_2=E_{01}+E_{10}$: one representative of each coset, as a
$3\times3$ matrix written row by row (\texttt{010/000/000} is $E_{01}$), with the multiplicity where it is two.}
\label{tab:leaf}
\end{table}

\section{Formal verification}\label{sec:lean}

The definitions of tensor rank and of $\mm nmp$ over $\Ft$ (as \lean{ZMod 2}), and the three claims, are stated in one
short file, with tensors as functions on finite index sets. The claims and the definitions they depend on read
\begin{footnotesize}
\begin{verbatim}
def outer3 (a : Fin n₀ → R) (b : Fin n₁ → R) (c : Fin n₂ → R) :
    Fin n₀ → Fin n₁ → Fin n₂ → R :=
  fun i j k => a i * b j * c k
def RankLE (T : Fin n₀ → Fin n₁ → Fin n₂ → R) (r : ℕ) : Prop :=
  ∃ (a : Fin r → Fin n₀ → R) (b : Fin r → Fin n₁ → R) (c : Fin r → Fin n₂ → R),
    T = ∑ s, outer3 (a s) (b s) (c s)
def mmT (n m p : ℕ) : Fin (n * m) → Fin (m * p) → Fin (p * n) → ZMod 2 :=
  fun x y z =>
    if x.val % m = y.val / p ∧ y.val % p = z.val / n ∧ z.val % n = x.val / m
    then 1 else 0
abbrev T334 : Fin (3 * 3) → Fin (3 * 4) → Fin (4 * 3) → ZMod 2 := mmT 3 3 4
def Rank334 : Prop := ¬ RankLE T334 26
def Rank344 : Prop := ¬ RankLE (mmT 3 4 4) 30
def Rank444 : Prop := ¬ RankLE (mmT 4 4 4) 34
\end{verbatim}
\end{footnotesize}
\noindent with \lean{R} a commutative semiring; in \lean{mmT} the entries $(i,j)$, $(j,k)$ and $(k,i)$ of the three
matrices have the indices $x=mi+j$, $y=pj+k$ and $z=nk+i$. The main theorems \lean{rank334\_ge\_27},
\lean{rank344\_ge\_31} and \lean{rank444\_ge\_35} prove \lean{Rank334}, \lean{Rank344} and \lean{Rank444}. As a guard
against a definitional slip, the
formalization also proves that $\mm334$ does have a decomposition of length $29$, and that the tensor agrees with the
trace form $\operatorname{tr}(XYZ)$. The development uses Lean~4.30.0 and Mathlib~v4.30.0.

The lemmas and propositions of Sections~\ref{sec:reduction} to~\ref{sec:certs}, and the symmetry statements of
Section~\ref{sec:setting} that they use, are ordinary Lean proofs: the split flattening, the two-case argument and the
substitution step, padding and caps, Lemma~\ref{lem:orderly} and Proposition~\ref{prop:search} for every subspace
searched, the five kinds of argument of Section~\ref{sec:table} with the induction on the dimension, and
Lemma~\ref{lem:rank}. Lemma~\ref{lem:quot} is not needed, since the formal statements use $\mathrm{QuotLB}$. The
Lean kernel decides the following computations: the flattening and forced-product certificates, the transport
witnesses, every block of every search trace with its dual vectors and group elements, the coverage of each search,
the tables that encode the caps, and the matching of each leaf with its certificate record. The certificate checker
of Section~\ref{sec:certs} is a Lean function with a proof that every certificate it accepts refutes its leaf, and the
kernel runs it on $18{,}751$ of the $19{,}562$ records.

The remaining $811$ records, from eight of the searches for subspaces of dimension $3$, are those that try the most
candidates, and in the kernel they would need far more memory than the others (Appendix~\ref{app:resources}). All
$811$ are checked in one evaluation of the same verified checker by Lean's compiler (\lean{native\_decide}). This adds
exactly one axiom, \lean{B334.T2.nat\_ok.\allowbreak\_native.\allowbreak native\_decide.\allowbreak ax\_1\_1}, to the
final theorems, which therefore
depend only on \lean{propext}, \lean{Classical.choice}, \lean{Quot.sound} and that axiom. The axiom asserts that the
compiled evaluation of one Boolean expression returned true. Trusting it means trusting that Lean's code generator,
its evaluator and the runtime's arithmetic on natural numbers compute the checker as the kernel would. None of the
project's own definitions carries an \lean{implemented\_by} or \lean{extern} attribute: a scan of all $42{,}559$
modules finds none, and finds \lean{native\_decide} used in this one module only. Compiled by the same Lean compiler into a
standalone program, the checker accepts all of these certificates, and on $2{,}150$ mutated certificates, $53$ of
which are still valid, its verdicts agree with those of an independently written checker.

Large constants such as the search blocks are loaded from data files at elaboration time as ordinary definitions, so
a wrong data file can stop the build but cannot produce a false theorem. The statement file and the files that state
the main theorems elaborate with automatic implicit arguments disabled. Appendix~\ref{app:resources} gives the size of
the formalization and of its build.

Before the formalization, the traces and the certificates were checked by programs written separately from the search
code: a trace checker that recomputes every pruning step and the coverage, and a certificate checker for the leaves.
As a positive control for the leaf rules, we moved a known decomposition of $\mm334$ of length $29$ into the leaf
questions of $38$ subspaces of dimension $3$, where it gives a solution, and confirmed that along the path to that
solution every branching step keeps it among the candidates.

\section{Open questions}\label{sec:remarks}

Is $\Rk_{\Ft}(\mm334)$ equal to $27$, $28$ or $29$? Raising the lower bound to $28$ by the same route would need both
point quotients to have rank at least $27$, that is, the searches of Section~\ref{sec:search} with $L=26$, in which
every cap is one larger.

Can the method work over other fields? Our computations are specific to $\Ft$: over a larger finite field the
searches would be larger, and over an infinite field there would be nothing to enumerate.

Can the kernel check every certificate? The $811$ certificates that the compiler now evaluates would need either far
more kernel memory (Appendix~\ref{app:resources}) or a checker designed for the kernel.

\appendix

\section{Resources of the formal proof}\label{app:resources}

Table~\ref{tab:resources} gives the size of the formalization and of its reference build, and the measurements behind
the choice of the $811$ certificate records that the compiler evaluates. A cost model calibrated on $8$ module builds
predicts more than $7{,}600$~MiB of kernel memory, the limit for which the kernel modules of the other certificates
were sized, for $490$ of these records (all of them among the $513$ that try more than $1{,}000$ candidates), and about
$542$~GiB for the largest. The model over-predicted every one of its calibration builds, so these figures are
likely overestimates. Checking these records in the kernel is a question of memory and of checker design.

\begin{table}[ht]
\centering
\begin{tabular}{lr}
\toprule
modules of the formalization & $42{,}559$ \\
CPU time of the reference build & about $120$ core-hours \\
largest memory of one module & about $15$~GiB \\
candidates tried by each compiled record & more than $500$ \\
compiled records that try more than $1{,}000$ candidates & $513$ \\
candidates tried by the largest compiled record & $78{,}379$ \\
kernel memory per candidate tried, in probes with $169$ to $2{,}853$ tries & about $4$ to $8$~MiB \\
\bottomrule
\end{tabular}
\caption{The size of the formal proof and of its build.}
\label{tab:resources}
\end{table}

\section*{Data availability}
The Lean formalization, the data files it reads and the logs of the reference build are archived at
\url{https://doi.org/10.5281/zenodo.23749574}.

\section*{Use of AI tools}
Generative AI tools were used to find and prove the results, to write the programs and the Lean formalization, and to
draft the text.

\begin{thebibliography}{FBH{$^+$}22}

\bibitem[Bl\"a99]{Bla99}
M.~Bl\"aser, \emph{Lower bounds for the multiplicative complexity of matrix multiplication}, Comput. Complexity
\textbf{8} (1999), 203--226.

\bibitem[Bl\"a03]{Bla03}
M.~Bl\"aser, \emph{On the complexity of the multiplication of matrices of small formats}, J. Complexity \textbf{19}
(2003), 43--60.

\bibitem[D'Am26]{DAm26}
I.~D'Ambrosio, \emph{The exact $\Ft$-rank of $2\times 3$ by $3\times 4$ matrix multiplication}, Zenodo, 2026,
\url{https://doi.org/10.5281/zenodo.21895176}.

\bibitem[dMU21]{dMU21}
L.~de Moura and S.~Ullrich, \emph{The Lean~4 theorem prover and programming language}, in: Automated Deduction --
CADE~28, Lecture Notes in Comput. Sci.~12699, Springer, 2021, 625--635.

\bibitem[FBH{$^+$}22]{FBH22}
A.~Fawzi et al., \emph{Discovering faster matrix multiplication algorithms with reinforcement learning}, Nature
\textbf{610} (2022), 47--53.

\bibitem[HH18]{HH18}
Q.~Huangfu and J.~A.~J.~Hall, \emph{Parallelizing the dual revised simplex method}, Math. Program. Comput.
\textbf{10} (2018), 119--142.

\bibitem[HK71]{HK71}
J.~E.~Hopcroft and L.~R.~Kerr, \emph{On minimizing the number of multiplications necessary for matrix
multiplication}, SIAM J. Appl. Math. \textbf{20} (1971), 30--36.

\bibitem[Lad76]{Lad76}
J.~D.~Laderman, \emph{A noncommutative algorithm for multiplying $3\times 3$ matrices using $23$ multiplications},
Bull. Amer. Math. Soc. \textbf{82} (1976), 126--128.

\bibitem[DPS25]{DPS25}
J.-G.~Dumas, C.~Pernet and A.~Sedoglavic, \emph{A non-commutative algorithm for multiplying $4\times4$ matrices using
$48$ non-complex multiplications}, arXiv:2506.13242, 2025.

\bibitem[mC20]{mC20}
The mathlib Community, \emph{The Lean mathematical library}, in: Proceedings of the 9th ACM SIGPLAN International
Conference on Certified Programs and Proofs (CPP 2020), 2020, 367--381.

\bibitem[N{$^+$}25]{Nov25}
A.~Novikov et al., \emph{AlphaEvolve: a coding agent for scientific and algorithmic discovery}, arXiv:2506.13131,
2025.

\bibitem[Pan66]{Pan66}
V.~Y.~Pan, \emph{Methods of computing values of polynomials}, Russian Math. Surveys \textbf{21} (1966), 105--136.

\bibitem[RR26]{RR26}
I.~Rudich and L.-M.~Rousseau, \emph{Lower bound of $22$ for $3\times 3$ matrix multiplication over $\mathbb{Z}$},
arXiv:2610.01639, 2026.

\bibitem[Smi13]{Smi13}
A.~V.~Smirnov, \emph{The bilinear complexity and practical algorithms for matrix multiplication}, Comput. Math.
Math. Phys. \textbf{53} (2013), 1781--1795.

\bibitem[Str69]{Str69}
V.~Strassen, \emph{Gaussian elimination is not optimal}, Numer. Math. \textbf{13} (1969), 354--356.

\bibitem[Tom26]{Tom26}
T.~S.~Tomar, \emph{The rank of $3\times 3$ matrix multiplication over $\Ft$ is $23$}, arXiv:2610.11823, 2026.

\bibitem[Wan26a]{Wan26a}
C.~Wang, \emph{Automated lower bounds for bilinear complexity over finite fields}, arXiv:2603.07280, 2026.

\bibitem[Wan26b]{Wan26b}
C.~Wang, \emph{A lower bound of $21$ for $3\times 3$ matrix multiplication over $\Ft$}, arXiv:2609.06725, 2026.

\bibitem[Yan26]{Yan26}
S.~Yang et al., \emph{A structural proof of the lower bound $21$ for $3\times 3$ matrix multiplication over $\Ft$},
arXiv:2609.18722, 2026.

\end{thebibliography}

\end{document}