发表机构
Universidad de Sevilla; University of Illinois Urbana-Champaign; Stanford University（塞维利亚大学; 伊利诺伊大学厄巴纳-香槟分校; 斯坦福大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文构造了具有3生成元9关系词且字问题不可解的群，并由此得到两个固定大小的Adian-Rabin族，进而证明$\#_7(S^2\ imes S^2)$拓扑不可识别和$\#_9(S^2\ imes S^2)$光滑不可识别，改进了先前最佳界，并提供了Lean 4形式化验证。
AI 中文摘要
我们构造了一个具有3个生成元和9个关系词的群，其字问题是不可解的。我们利用该群构造了两个固定大小的Adian--Rabin族群表示，一个具有4个生成元和11个关系词，另一个具有2个生成元和10个关系词。作为推论，$\#_7(S^2\ imes S^2)$是拓扑不可识别的，$\#_9(S^2\ imes S^2)$是光滑不可识别的。这些代数与拓扑结果改进了Borisov、Tancer和Gordon先前已知的最佳界。该群的构造基于Borisov的一个例子，并使用了额外的HNN扩张和Tietze消去来缩小表示的大小。我们还提供了代数结果的机器检查的Lean 4形式化。
英文摘要
We construct a $3$-generator $9$-relator group with unsolvable word problem. We use the group to construct two fixed-size Adian--Rabin families of group presentations, one with $4$ generators and $11$ relators, and another with $2$ generators and $10$ relators. As a consequence, $\#_7(S^2\times S^2)$ is topologically unrecognizable and $\#_9(S^2\times S^2)$ is smoothly unrecognizable. These algebraic and topological results improve the previous best known bounds by Borisov, Tancer, and Gordon. The construction of the group builds upon an example of Borisov and uses additional HNN extensions and Tietze eliminations to reduce the size of the presentation. We also provide a machine-checked Lean~4 formalization of the algebraic results.
Comments14 pages; the main results were developed by ChatGPT 5.6 Sol
