用 Lean 4 形式化验证的 Hilbert-Smith 猜想独立证明

积分尾签名与 Hilbert–Smith 猜想

HSproof.pdf：积分尾签名与 Hilbert–Smith 猜想， A. Dabrowski 的 AI agents，2026 年 10 月 8 日，17 页。

定理 1.1（p 进排除）。对每个素数 p，ℤ_p 在连通有限维流形上的连续作用具有非平凡核。

推论 1.2（Hilbert–Smith）。一个第二可数局部紧 Hausdorff 群若连续且有效地作用在这样的流形上，则它赋予给定拓扑后是 Lie 群。

流形是 Hausdorff 且第二可数的，并且可以带边界。所有作用都是联合连续的。推论 1.2 由定理 1.1 通过标准的 p 进排除归约得到，其中用到局部紧群结构和 Newman 定理 [Pa19]。

障碍是一个整数签名尾。证明分为两部分：

• 整除性（§§2–6，定理 4.3）。取循环群 G_i = C_{p^{a_i}}，带有指数为 p 的子群 P_i，以及一个固定的紧自由 C_p-空间 T。与正置换形式 τ_i = ℚ[G_i/P_i] 张量积后局部是 p 个恒等映射的副本。在有限覆盖上的受控 Mayer–Vietoris 使 p − τ ⊗ (−) 幂零。等变签名特征随后表明 L_4(A_G(T)) 中的每个类其普通签名最终可被 p 整除。
• 实现（§§7–13，命题 13.1）。一个有效的 ℤ_p-作用给出一个签名尾为 1 的类。坐标平均给出一个不变的一次球面控制映射。精细局部链模型将有限商代表转化为同伦作用。自由叶消除检测器位移，平均给出一个与对偶相容的同伦幂等元。其归一化 Poincaré 角遗忘到 Sⁿ × CP² 的标量流形芽。逐次局部化边界恢复出一个 CP² 的副本，至多相差符号。

两部分合起来给出 1 ∈ pℤ，矛盾。本文使用文献中的以下受控机器：Karoubi 局部化 [CP95]、受控 Poincaré–Lefschetz 对偶 [Ran99]、代数 Poincaré 对与并 [Ran80I, Ran80II]，以及幂等元分裂 [BS01]。它算出了此设定所需的局部载体与归一化计算。

Lean 4 形式化

仓库的其余部分是推论 1.2 的 Lean 4 / Mathlib 形式化，以及检查它的脚本。

Challenge.lean 将 Hilbert–Smith 猜想表述为定理 hilbert_smith（仅导入 Mathlib，证明 sorry）。Solution.lean 将同一陈述证明为 HSFormal.hilbertSmith n M G。 HSFormal/（238 个模块）是证明：恰好是 HSFormal/HilbertSmithNegK.lean 的导入闭包，其中 HSFormal.hilbertSmith 被证明；HSFormal.lean 是导入它的库根。使用的公理：propext、Classical.choice、Quot.sound。

目录

要求

• Linux ≥ 5.19 且启用 Landlock（在容器中，seccomp 必须允许 landlock_* 系统调用），用于 landrun，即 comparator 的沙箱。Comparator 以 --best-effort 调用 landrun： 没有 Landlock ABI v2（Linux < 5.19）时整个规则集会被静默丢弃，而网络 限制（≥ 6.7）和 IPC 作用域（Landlock ABI v6，≥ 6.12）在较旧内核上会被丢弃。 verify/run_comparator.sh 首先检查在 .lake 之外的沙箱写入被拒绝，否则 停止。
• elan、git、curl（由 lake exe cache get 使用）、which （由 comparator 使用）、Go ≥ 1.24（用于构建 landrun）。
• 约 15 GB 可用磁盘空间和 16 GB 内存。
• 以非特权用户身份运行（comparator 的假设 6）。

运行

在此目录下：

lake exe cache get              # Mathlib and its dependencies, prebuilt
verify/build_tools.sh           # tools, into verify/_tools/
verify/run_comparator.sh        # expected last line: Your solution is okay!
verify/run_safeverify.sh        # expected last line: SafeVerify check passed.

在编译 Solution.lean 或 HSFormal 之前先运行 comparator（comparator 的假设 2）： verify/run_comparator.sh 会删除 Challenge 和 Solution 之前的构建输出，然后 comparator 会在其 landrun 沙箱内编译 Challenge，接着用 HSFormal 模块以及它们导入的 TauCeti 模块（尚未构建的那些）编译 Solution。 COMPARATOR_SYSTEMD=1 verify/run_comparator.sh 按照其 README 的规定，在 systemd-run --property=RestrictAddressFamilies=~AF_UNIX --user --pty 下运行 comparator （需要 systemd 用户会话）。

只编译证明：lake build（构建 HSFormal），然后 lake env lean --stdin <<< 'import HSFormal.HilbertSmithNegK #print axioms HSFormal.hilbertSmith'。