在二元有限域𝔽₂上，3×3矩阵乘法的秩为23
The rank of $3\times 3$ matrix multiplication over $\mathbb{F}_2$ is 23
浏览论文内容
中文总结 AI 辅助
本文证明二元有限域上3×3矩阵乘法的秩为23，通过改进子空间秩下界、结合扁平化约束与计算机搜索，排除了秩为22的可能，验证了Laderman算法的最优性。
中文摘要 AI 辅助
根据Laderman算法，二元有限域𝔽₂上3×3矩阵乘法张量的秩至多为23，且Rudich与Rousseau近期证明其秩至少为22。本文证明该秩等于23。因此，Laderman算法是𝔽₂上所有双线性算法以及所有整数系数双线性算法中使用乘法次数最少的算法。证明采用了D'Ambrosio、Wang和Yang等人近期提出的替换方法：第一因子空间的子空间S，在长度为r的分解中，最多包含r-R(S)个第一因子，其中R(S)是张量模S的秩。我们对Wang提出的496类子空间对称类中的111类，提高了已知的R(S)下界。其中一个下界（对于由秩1矩阵张成的点，R(S)≥21）强制长度为22的分解的22个第一因子必须互不相同。张量的27×27扁平化对第一因子的秩给出了进一步约束，单独的枚举表明，当至少14个第一因子的秩为1时，某一线轨道中的任意直线都不包含两个第一因子。随后的计算机搜索列出了所有满足这些约束的22个矩阵的集合（按对称性分类），精确的完备性搜索表明，这些集合都不是分解的第一因子集合。计算生成了证书，这些证书由Lean 4证明辅助工具中的检查器验证，其正确性在Lean中得到证明。最大的检查以编译代码形式执行，因此该证明除依赖Lean内核外，还依赖Lean编译器。
英文摘要
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 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)\ge 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\times 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.
