二元体上の3×3行列積のテンソル階数下界21を構造的に証明
A Structural Proof of the Lower Bound 21 for $3\times3$ Matrix Multiplication over $\mathbb F_2$
この論文をやさしく読む
ひとことで言うと
0と1からなる二元体で3×3行列を掛ける計算について、20項以下のテンソル分解は存在しないとする構造的な証明です。
何に役立つ？
行列乗算を少ない基本的な積で表す方法に、どのような理論的限界があるかを理解する研究です。分解を探索する際の制約にもなります。
この研究の面白いところ
20項の分解があると仮定して階数の配置を絞り込み、可逆な因子の個数に矛盾を導きます。著者らは有限計算部分を含むLean形式化も報告しています。
どこまで分かった？
下界21の主張であり、21項で実現可能だという上界の主張ではありません。結果の対象はF₂上です。Leanでの形式化は著者の報告で、ここで証明コードの実行や検証は行っていません。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
二元体F₂上の3×3行列乗算のテンソル階数が少なくとも21であることを証明する。Qiushi Engineが独立に開発したこの構造的証明は、1つのテンソル因子に関する占有制約を、3つすべての因子を結び付ける代数関係へ変換する。検証済みの商の階数の評価と有限幾何により、仮に20項の分解が存在すると、その第1因子の行列階数プロファイルは(16,1,3)でなければならない。 そのため、対応する分割平坦化された各項の階数の和は27となり、全体の分割平坦化の階数とちょうど一致する。階数の劣加法性で等号が成立することから、これらの像は直和をなす必要がある。さらに、平坦化の逆写像で正規化すると、各項は互いの積がゼロとなる冪等元になる。行列乗算の明示的な積の恒等式から、可逆な第1因子は高々1つでなければならず、プロファイルが要求する3つと矛盾する。同じ障害は、分割階数の下界を達成する22項の分解にも制約を与える。 有限の商に関する評価も含め、完全な証明はLeanで形式化されている。付随する研究過程の記録には、数値実験や商の構成から構造的証明に至るまでの、Qiushi Engineによる長期にわたる自律的研究が記されている。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-16（UTC）
- 最新改訂
- 2026-09-16 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-16 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
We prove that the tensor rank of $3\times3$ matrix multiplication over $\mathbb F_2$ is at least $21$. The structural proof, independently developed by Qiushi Engine, converts occupation constraints on a single tensor factor into algebraic relations coupling all three factors. Certified quotient-rank bounds and finite geometry force any hypothetical $20$-term decomposition to have first-factor matrix-rank profile $(16,1,3)$. The ranks of the corresponding split-flattened summands therefore sum to $27$, exactly the rank of the full split flattening. Equality in rank subadditivity forces their images to form a direct sum; normalization by the inverse flattening then makes the summands pairwise annihilating idempotents. An explicit product identity for matrix multiplication implies that at most one first factor can be invertible, contradicting the three forced by the profile. The same obstruction constrains $22$-term decompositions attaining the split-rank bound. The complete proof, including the finite quotient bounds, is formalized in Lean. The accompanying research trajectory records Qiushi Engine's long-horizon autonomous research, from numerical experiments and quotient constructions to the structural proof.
著者のコメント
27 pages. Complete Lean formalization, finite certificates, source code, and reproducibility materials are available in the accompanying public repository
arXiv ID: 2609.18722 ／ 要約の誤りについて