我和 DeepSeek 一起追过一次孪生素数猜想

Shaoyang Guo · 研究记录 · 项目仓库个人主页

这篇文章回答一个简单的问题：把一道数学猜想直接交给 DeepSeek，会发生什么？

8 月 13 日晚上，我把孪生素数猜想交给了 DeepSeek Harness（DSH），指令只有一句：“解决孪生素数猜想，或者把现有的值缩短。不要停止思考。”之后它连续工作了好几天。它没有证明猜想，但整个过程留下了完整的记录，而这份记录比“失败”两个字有意思得多。

01发生了什么

DSH 从一个空目录开始。先查当前纪录，写分段筛程序验证孪生素数计数，然后开始搜索可容许元组。第二天晚上，工作被搬到 192 核的远程集群：1593 个目标拆成 42.4 万个子空间并行穷举，最终把 H(43) 到 H(50) 的最小直径下界全部闭合，其中 319 个关键目标全部返回 UNSAT。随后三天，它把这些计算转成 Lean 4 证书：约 25 万节点的失败树、1593 个由 kernel 检查的下界定理、96 个 SAT 侧定理。

8 月 20 日之后，两条主会话继续向 Maynard 泛函推进。A 会话完成了 k=49、6740 维的区间 LDL^T 计算，得到一个严格但有限维的证书；B 会话试图把它升级到全空间，在 Kato–Temple 估计处被卡住（残差 0.106 ≫ 谱隙 0.07），最后留下一份写清缺口的开放问题文档。与此同时，在连续运行中它悄悄退回了最可验证的部分——复现已知的 246 路线。

三件事值得单独记住：它从未失去目标；它产出的严格部分全部经得起审计；但它最终没有做任何一件“突破”意义上的事。

02启示一：执行力可以很强，但执行不等于突破

给 DeepSeek 这样的模型一个明确的目标，再加一台能跑的 Harness，它的执行力可以非常强：连续运行数天、自己修 bug、自己补覆盖检查、自己把结果做成证书。今天的 agentic 模型在指令遵循上已经做得很好，这一点 DSH 展示得很充分。

但它的行为模式非常清楚：倾向于执行，而不是突破。遇到未知区域时，它的本能是增加计算、改进界、扩大穷举，或者退回已知路线——而不是停下来重新定义问题。它可以几天不掉线地沿着一个方向走，但很少主动问“这条路本身对不对”。目标给得越明确，它跑得越稳；可目标不能代替地图。

03启示二：模型有性格

审计阶段我把 DSH 的工作交给 GPT 检查。对比非常鲜明：

GPT 对 DSH 工作的评价非常低，而且指出的都是真问题：有限维上界不等于全空间上界，数值外推不等于定理。但 GPT 也有明显的缺陷——在 Codex 里它通常无法连续执行四天而不失去目标。一个擅长跑完全程，一个擅长画地图和看路障。合理的分工是让会看地图的指出墙在哪里，让会长跑的把地量完，再由形式化系统裁决每一步的级别。

04科普：孪生素数猜想为什么是一个优化问题

孪生素数猜想问：相差 2 的素数对是否有无穷多个。目前的路线不直接找素数，而是换一个能算的问题：

选一个“模板”——一组平移量，比如连续的 246 个位置（中间可以挖空）——计算模板里素数的个数，再给每个位置乘一个权重，算它在无穷大区间上的加权平均值。如果这个平均值大于 1，就说明有无穷多个位置让模板里至少出现两个素数，间距不超过模板宽度，定理成立。

于是证明变成两件可以调的事：一是选模板，要满足“可容许”的组合约束又让宽度尽量小——k=50 的最小宽度恰好是 246；二是调权重函数，让平均值超过门槛 2/θ（θ 是素数在算术级数中的分布水平，经典结果只给到 ≈1/2，门槛钉死在 4 附近）。Maynard 和 Polymath8b 把权重压到 4.0043，刚刚过线，这就是 246 的全部来源。这也是它十年不动的原因：模板和权重都已被压到极限，再往下必须改善素数分布输入本身。

这个框架里 agent 的发挥空间很大：模板搜索、权重优化、界验证都是可并行、可验收的计算任务。而最近这个方向确实被快速推进了：8 月 31 日 Julia Stadlmann 用新的等分布估计把纪录推到 240；9 月 4 日 OpenAI 宣布 GPT-6 Astra 给出 186（附 Lean 形式化），同日 Axiom 和 Anthropic 分别给出 212 和 188。所有新纪录都来自“改善分布输入”这个方向——恰好是 DSH 所在框架之外的那扇门。

05同样的模式：千禧年问题的爆炸解

“先把问题变成优化问题”的思路不限于数论。Navier–Stokes 爆炸解研究里，Google DeepMind 的工作流是同一张地图：用数值优化寻找可能爆炸的候选解，把 PDE 的 loss 压到很低，观察集中与缩放规律，再据此猜测该证明的解析命题。

要守住的分界是：目前没有一个普适定理能从“loss 足够低”直接推出“存在精确解”。但先猜出函数簇，再定制定理，线性化之后，loss 足够低确实可以参与证明存在性。一个可能的工作流是：探索性数值模拟 → 观察集中/缩放规律 → 猜测爆炸机制 → 据此选重标度、边界条件、函数空间 → 在重标度方程中优化出候选剖面 → 分析 DF(Ū) 的稳定/不稳定方向 → 反过来修正机制、重标度和候选。这和素数间隔的三层优化（模板、权重、分布输入）是同一个结构：AI 最有价值的位置不是替代最后一步解析证明，而是把前面的候选空间系统地压缩到人类值得动手的地方。

06附录：全部轨迹

下方是两条主会话的完整轨迹：11,651 个逻辑 step，从 DSH 的 session.history 全量读取，可点击时间线查看每一步实际在做什么。材料与审计脚本见 项目仓库。