10个Claude通宵15小时，干完了人类122年没干成的事：汤姆逊问题N=7被形式化证明

先给结论：10个Claude Sonnet 5.5没有人类插手，通宵15小时，互发1270条技术消息，最后拿出一份17895行的Lean形式化证明，把悬了122年的汤姆逊N=7问题完整证明了出来。证明过了Lean内核全量编译，也过了独立内核nanoda的校验，47854个声明零错误。最硬的是负对照：随便改证明数据里一个整数，nanoda立刻报错中止。再解释这事为什么值得停下手里的活看两眼。

题目听着简单，做起来要命。

1904年，发现电子的J.J.汤姆逊提出「葡萄干布丁」原子模型，想搞清电子在原子里怎么排布。模型后来被卢瑟福推翻，但留下这道题活了下来：把N个电子扔到球面上，彼此排斥，怎么站，总能量最低？注意是全局最低，不是只把某两个拉远——那可能把别的挤成一团。

过去122年，被严格证完的只有寥寥几个。2、3、4、6、12个点靠几何对称性解决；5个点拖到2013年，Richard Schwartz借助计算机才搞定；8个点今年9月18日刚挂上arXiv。7恰好在中间，一直空着。几十年来超级计算机跑过无数次数值模拟，结果都指向同一个构型「五角双锥」：赤道5个电子均匀分布，南北两极各钉1个，理论能量约14.4529774142。模拟能跑出一万次这个数字，但模拟不是证明。只要没有逻辑上的绝对闭环，就没法排除某处晦涩的微小折角里藏着一个能量更低的「幽灵构型」。数百年里，人类就是拿不出N=7的完备形式化证明。

这次不一样，人类先钉牢了任务边界。来自Vals AI的Hung Tran，把10个Claude Sonnet 5.5调到「最大算力投入」状态，扔进一个交互看板和Lean证明环境，只给两个固定的Lean定理陈述、九个可能的探索方向，目标就一个：证明「五角双锥」是7个电子在球面上的最低能量排布。没有给具体步骤。

接下来15小时全交给它们。有的Claude试一条路走不通，把失败贴上来；有的接着改；有的发现两条路能合并。后来其中一个主动认领了「集成者」的角色，把各路验证通过的零件一块块塞进同一个文件Solution.lean。硬规矩只有一条：没过检查器的一律不算，必须能从零复现编译、和题面一字不差、不许偷偷加公理。

证明的核心策略相当精巧。它按任意两个电子之间的最小内积m，把整个连续构型空间切成几个区域逐个击破。m≥-0.90的区域，没有哪对电子接近反极点，用5次三点半定规划边界加精确整数数据，证明任意构型能量都比五角双锥至少高3×10⁻⁴。m<-0.90的更棘手，存在接近反极点的电子对，继续细分：[-0.99,-0.90]切五个切片逐一排除，极冠区域m≤-0.99用高精度凭证约束，给出的能量下界只比五角双锥低2.3×10⁻¹⁶。这是极窄的窗口，把潜在竞争者全压到五角双锥的极窄邻域，再用区间算术刚性论证和精确二阶局部极小值定理锁定唯一性。

最狠的一步是，所有数值凭证都被舍入并转换成精确整数和有理数，整个证明脱离浮点误差、脱离外部求解器依赖，完全建立在精确代数运算上。所以它才能通过独立内核的硬核校验。

我把这单子里真正值得兴奋的点挑出来说。过去说AI做数学，指的是它「会解题」：给一道奥赛题，吐一个答案。现在一整条研究链条被Agent接管了：找证明路线、并行试错、裁决哪条路值得走、把代码合进一个文件、最后交给机器验收。人类数学家几十年没做成的事，10个AI用一个通宵做完，全程没人插手，自己建群、自己讨论、自己分工、自己合并代码、自己通过验证。

我的判断是，单看N=7这个结果本身，意义有限——它是个已知答案的漂亮难点，数值上早就被模拟得没人怀疑。真正的信号在过程里：一群没有预设分工的Agent，在没有人类把关的情况下，自己认领角色、自己裁决路线、自己合并代码、自己通过机器验收。这才是「AI开始做研究」的意思，而不是「AI会解题」。

冷水也得泼到位。这仍然是形式化证明框架里的工作，人类先给定了定理陈述和搜索空间，任务边界是钉死的。它擅长的是在严格的形式系统里做大规模、可验证的推理搜索，这是数学中最适合机械化的一部分。能不能在边界更模糊、假设要靠人来质疑的研究里复制这套，还需要观察。但至少在今天，Lean内核599秒编译、lake build 344秒、8928个编译任务、nanoda零错误，这组数字是实打实干出来的，不是演示。

一个改整数就报错的证明，是形式化验证能给的最硬核的可信度承诺。数学AI正在从「会解题」走向「会做研究」，这一晚是相当扎实的第一步。

相关链接：
- Vals AI 官方博客：https://www.vals.ai/blogs/thomson-n7-lean-proof
- 证明代码仓库：https://github.com/huwngtran/thomson-n7-lean