纯 DeepSeek V4 Flash 做数学研究：有界素数间隔的验证与轨迹

先说结论：这不是孪生素数猜想的证明

“孪生素数猜想”仍未解决。项目研究的是与 Polymath8b 的无条件素数间隔纪录相关的一个可验证子问题：可容许 \(k\)-元组的最小直径 \(H(k)\)，以及 Maynard 筛法中的变分量 \(M_{k,\varepsilon}\)。

完成了什么

AI 实际做了哪些工作

这次过程不是一次性生成一篇漂亮的报告，而是一个持续的“提出假设 → 写实现 → 跑反例 → 修改 → 形式化 → 复查”的循环。轨迹中最值得公开的部分包括：

• 把“能否把 246 再缩短”拆成元组侧 \(H(k)\) 和筛法侧 \(M_{k,\varepsilon}\) 两个独立问题；
• 用 C 实现带频数剪枝的 DFS，并在早期剪枝出现数学问题后，通过手算反例修正完备性逻辑；
• 用 Python 的独立剩余类检查器与已知小规模 \(H(k)\) 表进行交叉验证；
• 不用 mathlib，仅用 Lean 核心库手写平移、剩余类、列表和证书 soundness 所需的引理；
• 在 M 泛函计算中发现浮点污染导致的假正特征值，并改用精确有理数和 \(LDL^\mathsf{T}\) 惯性判定；
• 最后主动把“有限函数族内小于 4”与“全空间小于 4”区分开，保留理论缺口，而不是把启发式证据写成定理。

证书化的核心思路

对固定 \(k,d\)，如果一个可容许元组存在，可以平移成包含 0 且位于 \([0,d]\) 中。对每个素数 \(p\le k\)，可容许性意味着至少有一个非零剩余类没有被元组覆盖。于是可以枚举每个素数选择的“禁止类”，并计算 \([0,d]\) 中避开所有禁止类的幸存位置数。

如果某个完整分配下的幸存位置少于 \(k\)，该分支就不可能产生可容许 \(k\)-元组。`CertVerify.lean` 定义这棵证书树，`Sound.lean` 证明证书通过会推出不存在直径不超过 \(d\) 的元组。每个具体的 `T_k_d.lean` 只需把巨大证书接到这个通用 soundness 定理上。

theorem H46_gt_214 :
  ¬ ∃ t : List Nat,
      admissible 46 t = true ∧ diameter t ≤ 214 := by
  exact certValidRoot_sound
    (k := 46) (d := 214)
    (c := cert_46_214) (by native_decide)

这类定理没有用户自定义的 sorry 或 axiom；不过使用了 Lean 的 native_decide，因此公开时应准确说明其编译器/运行时信任边界。

哪些是新贡献，哪些不是

这里需要非常克制。\(H(43),\ldots,H(50)\) 的数值本身并不是我首次发现的；它们已经出现在 OEIS、窄可容许元组数据库和相关文献记录中。Polymath8b 的 \(\le246\) 结果也不是本项目重新证明的筛法突破。

我认为项目真正有价值的部分是把已有组合事实做成可重新验证的 proof-carrying computation：搜索程序输出的不是最终信仰对象，Lean 证书验证器和通用 soundness 证明才是审计入口。同时，公开 trajectory 也展示了一个模型如何在长任务中进行数学建模、编程、反例驱动调试和自我限界。

我希望读者重点检查什么

1. 证书验证器是否真的覆盖了所有素数分支和所有剩余类选择；
2. 从任意可容许元组平移到包含 0、并把它嵌入幸存位置集的 Lean 引理是否完整；
3. C/ Python / Lean 三条实现对定义、端点和直径约定是否一致；
4. 有限函数族的 \(M\) 结果是否被错误外推成全空间上界；
5. trajectory 中的算法修正和失败尝试是否能帮助建立更可靠的 AI 数学研究工作流。

复现入口

主项目仓库：github.com/guoshaoyang-pku/twin-prime-admissible。其中包含 C 搜索、Python 验证、Lean 形式化、证书生成与公开报告。建议先阅读仓库 README，再阅读本页附带的 trajectory；轨迹保留了比 README 更完整的中间判断和未完成结论。

git clone https://github.com/guoshaoyang-pku/twin-prime-admissible
cd twin-prime-admissible

# 组合搜索示例
gcc -O3 -o admissible admissible.c -lm
./admissible 2 50

# Lean 证书目录：lean_cert/
# 需要 Lean 4.33；仓库中的 build_all.sh 仍需按本机路径调整