发表机构
Millennium Research（千禧研究）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该工作用 Lean 4 机器验证了 Gardam 提出的无挠 $\tilde{A}_2$ 格不具有唯一乘积，给出了显式有限子集见证（大小 32 和 28）及证书，是首个此类形式化验证。
AI 中文摘要
Kaplansky 的零因子猜想断言：域上无挠群的群环没有零因子。该猜想对每个具有唯一乘积性质的群都成立，因此反例只能来自不具有唯一乘积的无挠群。在 2021 年的讲座中，Gardam 宣布无挠的 $\tilde{A}_2$ 格 $\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$ 不具有唯一乘积，并将其作为一个新的候选群提出：它具有性质 (T)，而已知的证明该猜想的方法不适用于它。据我们所知，该宣布的证明尚未发表。我们给出了一个由 Lean 4 内核检查的证明，并针对 Mathlib 的 UniqueProds 类进行陈述。见证是一对显式的有限子集，$|A| = 32$ 且 $|B| = 28$，其中 896 个乘积中的每一个都与另一个乘积重合。对于 658 个乘积，证书是自由群中的恒等式；其余 238 个证书是共轭关系的显式乘积，共 970 个共轭，通过自由归约检查。一个到 $\mathbb{Z}/42$ 的同态表明，每一对 $(u,v)$ 与其伙伴 $(u',v')$ 作为群元素对不同，这正是定理所要求的。连同到交错群 $A_4$ 的同态，它还表明所列出的词是两两不同的，因此这些集合恰好有 32 和 28 个元素。见证和证书来自一个不可信的搜索程序，并由 Lean 重新检查。该开发仅使用公理 propext、this http URL 和 this http URL，没有 sorry 和 native_decide。数学陈述是 Gardam 的。据我们所知，这是证明助手中首次验证无挠群中的唯一乘积失败；$\Gamma$ 的无挠性取自 Gardam，未在此处形式化。
英文摘要
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 $Γ= \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 $Γ$ is taken from Gardam and is not formalized here.
Comments10 pages, 1 table. Use of an LLM is disclosed in Section 10. Lean 4 sources and certificates: https://github.com/ibrahimmian36/Karanos
