一个困扰物理数学界 122 年的问题，被 10 个 Claude Sonnet 5.5 智能体在一夜之间完成了形式化证明。
根据 MarsBit 转引微信公众号「新智元」内容，这次实验围绕汤姆逊问题的 N=7 情形展开：把 7 个电子放在球面上，在彼此排斥的条件下，寻找总能量最低的排布。结果显示，10 个 Claude Sonnet 5.5 在 15 个小时内互发 1270 条消息，写出 17895 行 Lean 代码，最终证明「五角双锥」是最低能量构型。
122 年悬而未决的 N=7 问题
报道提到，这道题最早可以追溯到 1904 年。电子发现者 J.J. 汤姆逊当年在提出「葡萄干布丁」原子模型时，试图研究电子在原子中的排布方式。虽然该模型后来被卢瑟福推翻，但相关数学问题保留下来，成为后来所说的「汤姆逊问题」。
问题的表述并不复杂：把 N 个电子放在球面上，它们相互排斥，怎样排布才能让总能量最低。难点在于，拉开某两个电子的距离，可能又会让其他电子变得更拥挤，因此不能只看局部距离，而要对整体构型给出严格证明。
过去 122 年里，只有少数情形被严格证明。2、3、4、6、12 个点的情形依靠几何对称性得到解决；5 个点直到 2013 年，才由数学家 Richard Schwartz 借助计算机完成证明；8 个点则在今年 9 月 18 日由 Kryvonos、Liehr、Taylor 三位数学家上传至 arXiv，并使用 Lean 做了形式化。
7 个点一直是中间空缺的一环。长期以来，数值模拟反复指向同一个构型：五角双锥，也就是赤道上均匀分布 5 个电子，南北两极各 1 个，对应理论能量值约为 14.4529774142。但数值结果并不等于数学证明，因为只要逻辑上没有完全闭合，就无法彻底排除某个极其隐蔽、能量更低的构型存在。
10 个智能体在 Lean 环境中协作 15 小时
这次任务由来自 Vals AI 的 Hung Tran 交给一个由 10 个 Claude 组成的虚拟实验室。实验开始前，人类只设定了任务边界：将 10 个 Claude Sonnet 5.5 智能体全部调到「最大算力投入」状态，放入交互看板和 Lean 证明环境，目标是证明五角双锥是 7 个电子在球面上的最低能量排布。
输入信息显示，研究者没有给出具体步骤，只提供了两个固定的 Lean 定理陈述，以及 9 个可能的探索方向。之后的 15 个小时里，证明过程由智能体自行推进。
在这段时间内，10 个 Claude 一共产生了 1270 条技术讨论消息。部分智能体尝试某条路线后发现无法推进，会把失败结果贴出来；另一些则接着修改；也有智能体发现不同路径之间可以合并。随后，其中一个 Claude 主动承担「集成者」角色，把已经验证通过的部分逐步汇总进同一个文件 Solution.lean。
整个流程有一条硬性规则：任何没有通过检查器的内容都不算数。证明必须能够从零复现编译，必须与题面严格一致，也不能额外引入公理。最终，系统得到一份 17895 行的 Lean 形式化证明。
证明如何展开：先切分构型空间，再锁定唯一性
报道称，这份证明的核心做法，是按照任意两个电子之间的最小内积 m，把连续构型空间切分成多个区域分别处理。
区域一：m ≥ -0.90
在这一部分，不存在任何一对电子接近反极点。Claude 使用了一个 5 次三点半定规划边界，并结合可由内核直接检验的精确整数数据，证明该区域内任意构型的能量都至少比五角双锥高 3×10⁻⁴。
区域二：m < -0.90
这一部分更难，因为会出现接近反极点的电子对。智能体又把它继续拆分。
- 对 [-0.99, -0.90] 的 5 个切片，每个切片使用一个严格的三点凭证排除，得到的能量下界比最优能量高约 2.6×10⁻⁶。
- 对极冠区域 m ≤ -0.99，则使用高精度凭证进行约束。该凭证给出的能量下界仅比五角双锥能量低 2.3×10⁻¹⁶。
报道将这一差距描述为一个极窄窗口，它把潜在竞争构型压缩到了五角双锥附近极小的邻域中。随后，Claude 继续使用区间算术刚性论证和精确二阶局部极小值定理，最终完成唯一性的锁定。
另一个关键点在于，所有数值凭证都被舍入并转换成精确整数和有理数。这样一来，整个证明脱离了浮点误差，也不再依赖外部求解器，建立在精确代数运算之上。
Lean 与 nanoda 双重验证
验证结果也给出了具体数据。
- Lean 内核全量编译在 599 秒内通过，其中 lake build 耗时 344 秒，共完成 8928 个编译任务。
- 独立内核 nanoda 校验了 47854 个声明，结果为零错误。
- 在负对照实验中，仅修改证明数据中的一个整数，nanoda 就会立刻报错并中止。
报道特别强调了这一点：改一个整数就报错，说明证明数据与形式化结构之间的约束非常紧，验证并不是靠模糊容忍完成，而是严格建立在可检验的一致性上。
从「会解题」到「会做研究」
这篇文章把此次实验放在更大的数学 AI 演进脉络中来看。过去谈论 AI 做数学，更多是指它能对一道题给出答案；而这次展示的是另一条更完整的链条：找证明路线、并行试错、判断哪些方向值得继续、把可验证代码整合起来，最后再交给机器验收。
按原文说法，这次任务中没有人类介入证明过程，也没有预设分工。10 个 Claude 自行讨论、自行分工、自行整合代码，并通过最终验证。
文章最后写道，这 10 个 Claude 在一个通宵里做成的，不只是一个百年猜想的证明，也是在展示 AI 已经可以与人类一起做数学研究。
本文来自微信公众号「新智元」，作者为「ASI启示录」。MarsBit 对该内容进行了发布。