2026 年 9 月 28 日，Vals AI 研究员 Hung Tran 发布了一项结果：十个 Claude Sonnet 5.5 智能体在约 15 小时内协作产出一份 17895 行的 Lean 4 形式化证明，证明对象是汤姆逊问题（Thomson problem）的 N=7 情形。证明通过了 Lean 内核全量编译、标准公理检查，以及一个独立实现的第二内核（nanoda）对 47854 条声明的逐条校验。证明源码、验证脚本和全部日志已在 GitHub 开源（huwngtran/thomson-n7-lean）。
这个结果的信息量不在「AI 又解出一道题」。数值模拟几十年前就能算出 N=7 的答案大概长什么样，这次补上的是另一个层面的东西：数学意义上的证明，即在连续的构型空间里排除所有其他可能。模拟收敛一万次也只是证据积累，证明要求的是逻辑闭环。这两件事的差别，是这个案例值得逐层拆开的原因。
汤姆逊问题卡在哪里
1904 年，发现电子的 J.J. Thomson 提出的问题很朴素：把 N 个带负电的点电荷放到单位球面上，彼此排斥，最终哪种排布的总静电能最低？能量由库仑势对所有点对求和定义：E(x) = Σ 1/‖xi − xj‖。
这个问题越到大的 N 越难给出严格答案。截至这次工作之前，被完整证明的情形是：N=2、3、4、6、12 依靠几何对称性解决；N=5 拖到 2013 年，由 Richard Schwartz 借助计算机辅助完成；N=8 的证明今年 9 月刚由 Kryvonos、Liehr、Taylor 三人挂上 arXiv（编号 2609.22077），同期还有 Joseph Tooby-Smith 和 Alex Zughaid 搭建的配套 Lean 形式化。N=7 恰好夹在这些结果之间，长期空着。
N=7 的预期答案是正五角双锥：赤道均匀分布 5 个电子，南北两极各 1 个。它的总能量有解析表达式：E(P) = 1/2 + 5√2 + 5/(2sin(π/5)) + 5/(2sin(2π/5))，约等于 14.4529774142。数值搜索每次都收敛到这个构型，但「每次都算出它」和「证明只有它能取到最小值」之间隔着一整个连续空间：任何一个极狭窄区域里都可能藏着一个能量更低的竞争构型，而模拟永远扫不完所有区域。
证明策略：按最小内积切分空间
智能体交付的证明用了一个经典的处置思路：把无限的构型空间切成有限块，每块用一种工具关掉。切分的轴是任意两个电子之间内积的最小值 m，它刻画了构型中「最接近对跖的一对点」有多接近。
| 区域 | 覆盖范围 | 使用的工具 | 与最优能量的差距 |
|---|---|---|---|
| Case 1 | m ≥ −0.90 | 5 次三点半定规划边界（Bachoc–Vallentin 型，经 Cohn–Woo 适配于能量问题），数据为精确整数 | 任何构型 E ≥ E(P) + 3×10⁻⁴ |
| 五个切片（slab 1–5） | m ∈ [−0.99, −0.90]，按 [−0.99,−0.98]、[−0.98,−0.96]、[−0.96,−0.94]、[−0.94,−0.93]、[−0.93,−0.90] 分片 | 每片一个严格三点证书 | 每片能量下界高出 E(P) 约 2.6×10⁻⁶ |
| 极冠（cap） | m ≤ −0.99 | 高精度三点证书 | 证书给出的下界仅比 E(P) 低 2.3×10⁻¹⁶ |
前两类区域直接排除：落在里面的构型能量明显偏高。真正的难点全部被压缩到极冠里，因为那个 2.3×10⁻¹⁶ 的间隙意味着任何潜在竞争者都必须挤在五角双锥内积模式附近的极窄管道中。最后一步，区间算术的刚性论证加一个精确的二阶局部极小值定理，证明在这个管道里五角双锥是唯一的局部极小，从而完成唯一性证明：任何最优构型只能是五角双锥经过旋转、反射或重新标号后的样子。
拼装完的最终形态很轻：两个主定理各只有几行，把极冠、五个切片和 Case 1 的结论粘在一起。
证书机制：数值找到，整数验证
这份证明里另一项关键技术选择，是对浮点数的彻底清除。半定规划（SDP）边界和三点证书最初都是数值求解器找到的，浮点结果天然带着舍入误差，而 Lean 内核不做近似计算。处理办法是把所有数值凭证舍入成精确的整数或有理数，再交给内核逐一检验。
这样处理之后，证明的有效性不再依赖「求解器算得够准」。求解器的角色退化为「找候选」，验证完全由精确代数运算接管。这也是负对照实验能成立的前提：改动 Case 1 数据里的任何一个整数，第二内核 nanoda 立刻报错中止。误差要么不存在，要么让整个验证失败，没有中间地带。
五道验证关卡
Hung Tran 对最终文件跑了五项独立检查，全部记录在仓库的 verification 目录：
| 检查 | 建立的事实 | 结果 |
|---|---|---|
| 干净构建 | 每一步类型检查通过、每个证明目标关闭 | 599 秒完成，其中 lake build 344 秒，共 8928 个任务 |
| 公理检查 | 证明只依赖 Lean 标准公理 | 仅 propext、Classical.choice、Quot.sound |
| Comparator 比对 | 证明的正是挑战文件里固定的那两个定理陈述 | 260 秒通过，判定文本为 "Your solution is okay!" |
| 第二内核 nanoda | 用独立实现的内核核对导出的证明项 | 47854 条声明，零错误 |
| 负对照 | 篡改一个整数必须被检出 | nanoda 立即中止 |
公理检查这一项值得单独说明：propext、Classical.choice、Quot.sound 是 Lean 的三个标准公理（外延性、经典选择、商构造），除此之外没有引入任何额外假设，也没有使用 native_decide 这类绕过内核的捷径。仓库的 check.sh 会扫描源码中的 sorry（未证明占位）、native_decide 和元编程痕迹，逐行核对论文到 Lean 代码的引用索引，最后自动执行一次「把不等号翻转、验证必须被拒绝」的负对照。
智能体是怎么协作的
实验的组织方式：人类给出的输入是两个固定的 Lean 定理陈述（一个证能量下界，一个证唯一性）和九个初始探索方向，其中包括移植 N=8 的先例方法、线性规划边界、按组合类型切分、构建经验证的证书引擎等。之后是约 15 小时的自主运行，智能体在留言板上写了 1270 条消息。
协作中出现了自发的分工。有的智能体沿一条路线推进失败后把失败结论贴出来，避免后来者重走；有的发现两条路线可以合并；一个智能体主动认领了「集成者」角色，负责把各路通过验证的证明件合并进单一的 Solution.lean 文件。一条硬规则贯穿全程：候选证明只有通过检查器（可复现的构建、与挑战文件的精确比对、公理检查）才算数，通不过的中间成果一律不计。
这套流程里人类的实际输入是题面、初始方向和验收标准，过程干预为零。方向由机器提议、丢弃与合并，这条路走通与否全部由检查器裁决。
复现门槛与这条路的边界
仓库把复现做成了一条命令：克隆后在根目录执行 bash formal/check.sh。它会校验两个关键文件的 sha256（Solution.lean 为 6545e982 开头）、扫描违禁构造、拉取钉死的 Mathlib 缓存（Lean v4.34.1，Mathlib 提交 d13f23b）、全量构建、打印公理、执行 Comparator 比对和第二内核校验，最后跑负对照。在一台 48GB 内存的 Mac 上全程 599 秒；最低要求是 14GB 内存加 10GB 磁盘。完整证明只依赖 Mathlib 一个外部库。
两个边界需要如实标注。其一，仓库自述「Statement not human-certified. Not peer reviewed.」：定理陈述本身与文献一致，但这份证明尚未经过同行评审，形式化社区的独立复核仍是后续步骤。其二，这份证明站在今年 9 月 N=8 工作的方法论地基上：Bachoc–Vallentin 型半定规划边界、Tooby-Smith 与 Zughaid 的 Lean 基础设施都是人类数学家的既有成果，证书的数值搜索仍由 SDP 求解器完成。智能体的增量在于把「按最小内积切分、逐区配备证书、精确化验证」这条完整链路自主走通，并在 15 小时内交付了机器可验证的成品。汤姆逊问题的一般 N 仍是开放问题，这份证明覆盖的只是 N=7。
来源：
- Vals AI 官方博客：A Lean Proof of the Thomson Problem for Seven Electrons（vals.ai/blogs/thomson-n7-lean-proof）
- 证明仓库：github.com/huwngtran/thomson-n7-lean（含论文、验证日志、复现脚本）
- N=8 先例：Kryvonos, Liehr & Taylor, arXiv:2609.22077