七个电荷在球面上找到了位置：17,895 行 Lean 与一次 15 小时的集体作业
把七颗同号电荷扔到一个球面上，它们互相推开，最后会停在某处。停在哪里，J.J. 汤姆孙 1904 年就问过。
把七颗同号电荷扔到一个球面上，它们互相推开，最后会停在某处。停在哪里，J.J. 汤姆孙 1904 年就问过。
汤姆孙当年问这个问题，是为了给原子建模：正电荷像布丁一样摊开，电子嵌在里面。那个原子模型后来被实验推翻了，问题是它留下的一道几何习题活了下来，而且活了一百多年。
此后 N=7 的答案一直是数值上的：算出来是五角双锥，五个点绕赤道，两极各一个。但算出极小值，跟证明其余所有构型的能量都更高，是两件难度差很远的活。
2026 年 9 月，Vals AI 放出了一份形式化证明。十个 Claude Sonnet 5.5 智能体跑了约 15 小时，产出一个 17,895 行的 Solution.lean，只 import Mathlib，确立五角双锥是 N=7 时的唯一极小解，旋转与镜像都不算新解。
🧲 七个点，和一个连续无穷的对手
汤姆孙问题的能量是所有点对的 \(1/\|x_i-x_j\|\) 之和，点对两两都算一次。
难的地方在对手的数量。要证明一个候选比其余构型都低，对手是连续的无穷集合，不是在有限张表里挑一张出来比。数值计算能跑遍几百万个随机构型，跑不完那个无穷。
N=7 还多一层麻烦。五角双锥里有两类不等价的点，极点和赤道上的顶点。证书与 Lean 类型都得把这两个角色分开处理，N=8 那套现成的机制搬不过来。
这里有个尺度可以拿来掂量。N=8 的结果同样是 2026 年 9 月才由 Kryvonos、Liehr 与 Taylor 给出的（arXiv:2609.22077），随后 Tooby-Smith 与 Zughaid 做了 Lean 开发。也就是说，八个点这道题的严格证明，比七个点只早了不到一个月。
📐 一个标量，把无穷切成三段
证明用最小的两两内积 m 做分划。两个单位向量之间的距离由内积决定，m 接近 −1 说明存在一对近似对映的点。三条区间各配一套证书：
| m 的区间 | 用的方法 | 相对 E(P) 的余量 |
|---|---|---|
| m ≥ −0.90 | 五度三点半定规划证书，基于 Bachoc-Vallentin 方法与 Cohn、Woo 的能量形式 | 高出至少 3×10⁻⁴ |
| −0.99 ≤ m ≤ −0.90 | 五块 slab 各自排除，每块一张三点证书 | 每块高出约 2.6×10⁻⁶ |
| m ≤ −0.99 | 近对映证书加区间算术，再做精确二阶局部分析 | 初步界落到 E(P) 以下 2.3×10⁻¹⁶ |
🔢 为什么一个矩阵能管住无穷多个点
半定规划证书的原理值得单说一句，它是整份证明里最不讲直觉的一环。
它从一个半正定的多项式矩阵导出一条普适的能量不等式。这个不等式对球面上任意一组点都成立，于是一次性管住了无穷多个构型。数值求解器负责找合适的系数，找到之后再取整成精确的整数或有理数，算术由 Lean 检查。
这条分工是理解整件事的关键。求解器在这里是证书的生成器，不在信任基里。就算求解器算错了，它交出来的那组精确数据过不了 Lean 这一关，证明就编不过。
最后封顶那一段不能只靠半定界，因为它的余量差一点够不到目标能量。区间算术把剩下的构型严格框在五角双锥附近，二阶计算再证明严格的局部极小性并定出等号情形。
🔍 五道检查，把信任基压到最窄
放出来的工件是单个 Solution.lean 文件。Vals 列了五步验证：
Lean 与 nanoda 两个内核互相同意，把某一个检查器本身有缺陷这种暴露面压下去。公理审计把逻辑假设摆到明面上，#print axioms 只报出 propext、Classical.choice 与 Quot.sound 三条，用的都是 Lean 的标准公理。
第五步是我最想留下的一条。把第一个 case 里的一个整数改掉，独立检查器就把证明拒了。这一步验的不是证明对，是检查器会拒绝错的证明。
🤖 十五小时里的一千二百七十条消息
工程配置是这样：十个 Sonnet 5.5 智能体共享同一个 Lean 工程，配一块留言板和 maximum-effort 档位。初始简报提了九个方向，智能体可以放弃、合并或反驳其中任何一个。15 小时里它们交换了 1,270 条消息。
其中一个智能体担任集成者，把通过验证的贡献内联进 Solution.lean。一个候选要进最终工件，得先过三关：可复现的构建、与固定定理签名比对、公理审计。
【判断】这个分工方式比"十个智能体各写各的"更有意思。并行探索要能收敛，靠的不是投票，是只有一个进程握着最终依赖图。
🧱 值得抄走的四条
Vals 在报告里总结了四条工程实践。【判断】这四条比那 17,895 行代码更容易搬进别人的项目。
- 先把定理签名钉死。机器可检查的目标一旦固定，探索过程中成功标准就不会漂。
- 搜索与信任分开。数值工具可以提候选证书，精确性交给证明助手。
- 集成要有明确归属。并行探索只有在某一个进程握着最终依赖图和构建时才有用。
- 测试你的验证器。干净构建、公理审计、独立内核、故意变异，四者抓的是不同失效模式。
⚠️ 边界在哪里
内核接受只能说明形式结论从那两条固定命题及其依赖推出。这两条命题是否忠实编码了汤姆孙问题本身，需要人另审一遍。这是形式化方法共同的缺口，机器管不了这一层。
变异测试只改了一个整数，没有做更系统的突变集。15 小时与 1,270 条消息这类过程指标由 Vals 自行记录，未见第三方复现报道。
信源：Vals AI 博客 vals.ai/blogs/thomson-n7-lean-proof 与仓库 github.com/huwngtran/thomson-n7-lean；N=8 论文 arXiv:2609.22077。 限定：本文数字来自 Vals AI 自述；汤姆孙 1904 年提出该问题一节为背景常识，未在此次检索到的一手文献中逐字核对。