Gardamの格子群が一意積性を持たないことをLeanで検証
A Machine-Checked Proof that Gardam's $\tilde{A}_2$ Lattice Does Not Have Unique Products
この論文をやさしく読む
ひとことで言うと
ある群の中で、2つの有限集合の要素を掛け合わせても、一通りの組合せからしか生じない積がないことを、証明支援ソフトLeanで検証した研究です。
何に役立つ？
零因子予想の反例候補を調べるための、検証可能な数学的証拠になります。一意積性がないことを確かめても、それだけで零因子予想の反例を得たことにはなりません。
この研究の面白いところ
探索プログラムの正しさを信頼する代わりに、出力された具体的な集合と証明書をLeanで再検証しています。積の一致だけでなく、対応する要素の組が異なることも準同型を使って確かめます。
どこまで分かった？
形式化の対象は一意積性の失敗です。群の無捩れ性は既存の結果に依拠し、今回の形式化には含まれません。初の検証例という位置付けも、著者らの把握する範囲での主張です。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
Kaplanskyの零因子予想は、体上の無捩れ群の群環には零因子が存在しないと主張する。一意積性を持つ群ではこの予想が成立するので、反例となり得るのは一意積性を持たない無捩れ群に限られる。Gardamは2021年の講義で、無捩れのÃ₂格子Γ = ⟨a, b | aba²b⁻¹a²b⁻², ab³ab⁴a⁻¹b⟩が一意積性を持たないと発表し、新しい候補群として提示した。この群は性質(T)を持ち、予想を証明する既知の方法を適用できない。著者らの知る限り、この発表の証明は公表されていない。 本研究では、MathlibのUniqueProdsクラスを用いて定式化し、Lean 4のカーネルで検証した証明を与える。その証拠は、|A| = 32、|B| = 28である明示的な有限部分集合の対であり、896個の積のそれぞれが別の積と一致する。658個の積については証明書が自由群内の恒等式であり、残り238個の証明書は関係子の共役の明示的な積で、共役は合計970個となる。これらを自由簡約によって検証する。 Z/42への全射準同型により、各組(u, v)が対応する相手(u′, v′)と群要素の組として異なることを示す。定理が要求するのはこの点だけである。交代群A₄への全射準同型と併せると、列挙した語が互いに異なることも示せるため、集合の要素数は正確に32と28である。証拠と証明書は信頼を前提としない探索プログラムで得られ、Leanで改めて検証される。この形式化が用いる公理はpropext、Classical.choice、Quot.soundだけであり、sorryもnative_decideも使用しない。 数学的な命題自体はGardamによる。著者らの知る限り、これは無捩れ群で一意積性が破れることを証明支援系で検証した最初の例である。ただし、Γが無捩れであることはGardamの結果を採用しており、ここでは形式化していない。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-17（UTC）
- 最新改訂
- 2026-09-17 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-17 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
Kaplansky's zero-divisor conjecture asserts that the group ring of a torsion-free group over a field has no zero divisors. It holds for every group with the unique-product property, so a counterexample can only come from a torsion-free group without unique products. In lectures in 2021, Gardam announced that the torsion-free $\tilde{A}_2$ lattice $\Gamma = \langle a, b \mid a b a^2 b^{-1} a^2 b^{-2}, a b^3 a b^4 a^{-1} b \rangle$ does not have unique products and presented it as a new candidate group: it has property (T), and the known methods for proving the conjecture do not apply to it. To our knowledge, no proof of the announcement has been published. We give a proof checked by the Lean 4 kernel and stated against Mathlib's UniqueProds class. The witness is an explicit pair of finite subsets with $|A| = 32$ and $|B| = 28$ in which each of the 896 products coincides with another product. For 658 products the certificate is an identity in the free group; the other 238 certificates are explicit products of conjugated relators, 970 conjugates in all, checked by free reduction. A homomorphism onto $\mathbb{Z}/42$ shows that each pair $(u,v)$ differs from its partner $(u',v')$ as a pair of group elements, which is all the theorem requires. Together with a homomorphism onto the alternating group $A_4$ it also shows that the listed words are pairwise distinct, so the sets have exactly 32 and 28 elements. The witness and certificates come from an untrusted search program and are re-checked by Lean. The development uses only the axioms propext, Classical.choice and Quot.sound, with no sorry and no native_decide. The mathematical statement is Gardam's. To our knowledge this is the first verification in a proof assistant of a unique-product failure in a torsion-free group; torsion-freeness of $\Gamma$ is taken from Gardam and is not formalized here.
著者のコメント
10 pages, 1 table. Use of an LLM is disclosed in Section 10. Lean 4 sources and certificates: https://github.com/ibrahimmian36/Karanos
arXiv ID: 2609.22380 ／ 要約の誤りについて