发表机构
Polytechnique Montréal; Carnegie Mellon University（蒙特利尔高等商学院; 卡内基梅隆大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文证明整数上任何3x3递归矩阵乘法算法至少需22次乘法，排除优于Strassen算法的可能，基于Wang的分解方法在Lean中形式化验证。
AI 中文摘要
Strassen证明了两个2x2矩阵可以用7次乘法而非8次来完成。递归应用该算法，两个nxn矩阵的乘法需要O(n^2.807)次乘法，优于朴素的O(n^3)。目前已知最佳的3x3递归矩阵乘法算法使用23次乘法，复杂度为O(n^2.854)。已发表的最佳下界为21次（针对具有整数常数的算法），这为存在O(n^2.771)次乘法的算法留出了空间，因此并未排除存在优于Strassen算法的可能性。我们证明了对于任何具有整数常数的3x3递归算法，其乘法次数下界为22次，从而证明此类算法不可能优于O(n^2.814)次乘法，并消除了存在优于Strassen的2x2方法的3x3算法的可能性。该证明基于Wang最近提出的分解方法，他将该问题转化为496个子问题。我们为其中359个子问题提供了精确解。该证明在Lean中形式化；验证只需审查几个简短的文件。Lean形式化直接编码了关于递归矩阵乘法算法局限性的陈述，而不仅仅是关于问题秩的陈述。
英文摘要
Strassen showed that two 2x2 matrices can be multiplied with 7 multiplications instead of 8. Applied recursively, his algorithm multiplies two nxn matrices with O(n^2.807) multiplications, beating the naive O(n^3). The best known 3x3 recursive matrix multiplication algorithm uses 23 multiplications O(n^2.854). The best published lower bound of 21 (on algorithms with integer constants) leaves room for an algorithm with O(n^2.771) multiplications, and thus does not rule out the possibility of an algorithm that would beat Strassen's. We prove a lower bound of 22 multiplications for any 3x3 recursive algorithm with integer constants, proving that no such algorithm can do better than O(n^2.814) multiplications, and eliminating the possibility of a 3x3 algorithm that beats Strassen's 2x2 method. The proof builds on a recent decomposition method from Wang, who approached the problem by turning it into 496 subproblems. We provide exact solutions for 359 of them. The proof is in Lean; verification requires auditing only a few short files. The Lean formalization directly encodes statements about the limitations of recursive algorithms for matrix multiplication, as opposed to just a statement about the rank of the problem.
DOI：10.5281/zenodo.23047900, 10.5281/zenodo.23048286
