球面上放 7 个电子，怎么站最省能量。
这道题挂了 122 年。
答案早就有人猜到，却始终没人能证明。
9 月 30 日，十个 Claude Sonnet 5.5 把它补上了。
它们通宵跑了 15 个小时。
互相发了 1270 条消息。
最后交出一份 17895 行代码。
全程没有人类插手。
没有分工表，也没有组长。
十个模型自己建群，自己争吵，自己选路。
最后自己把代码并到一起。
最硬的一关是验证。
这份证明同时通过了 Lean 内核和 nanoda 两套校验。
后者是完全独立实现的内核。
改动证明数据里的一个整数，它立刻报错。
所以这不只是模型算得快。
AI 开始自己动手做研究了。
一、一道挂了一百多年的题
故事要从 1904 年说起。
那一年，汤姆逊提出了葡萄干布丁原子模型。
他想弄清电子在原子里怎么排布。
模型后来被卢瑟福推翻了。
可附带的问题留了下来。
它的名字就是汤姆逊问题。
题目一句话能说完。
把 N 个电子扔到球面上，彼此排斥。
怎么摆，总能量最低。
难就难在总能量这三个字。
只把两个电子拉开，可能把其余几个挤成一堆。
一百多年里，被严格证完的点数并不多。
5 个点拖到 2013 年，才由一位数学家借助计算机证完。
8 个点就在 9 月 18 日，刚被三位数学家挂上预印本网站。
7 个点夹在中间。
位置一直空着。
数十年来，世界各地的超级计算机反复做数值模拟。
结果都指向同一个漂亮的构型。
赤道均匀摆 5 个，南北两极各钉 1 个。
它有个名字叫五角双锥。
算出来的理论能量值约等于 14.4529774142。
问题在于，模拟不等于证明。
数值跑一万次，也排不掉某个晦涩角落里的反例。
只要逻辑没有闭环，怀疑就一直留着。
122 年里，始终没人拿出完备的形式化证明。
后来，一家做模型评测的机构接下了它。
那里的一位研究者把任务交给一间虚拟实验室。
实验室里的成员是十个 Claude。
它们统统被调到最大算力档位。
二、十个模型自己开了一场会
这场实验里，人类只做了一件事。
把任务边界钉死。
目标只有一行字。
证明五角双锥是 7 个电子在球面上的最低能量排布。
没有给具体步骤。
只给两条固定的定理陈述。
外加九个可以探索的方向。
剩下 15 个小时，全交给它们。
有的模型试一条路走不通，就把失败贴出来。
有的顺着改。
有的发现两条路其实能合并。
1270 条消息就堆在讨论区里。
再后来，其中一个模型认领了集成者的角色。
它把各路验证通过的零件，一块块塞进同一个证明文件。
硬规矩只有一条。
没过检查器的，一律不算。
必须能从零复现编译。
必须和题面一字不差地对上。
不许偷偷补上公理。
最终得到的，是一份 17895 行的形式化证明。
它不是一次成型的。
是十几轮试错之后，被拆散又重新拼起来的。
三、改动一个整数就会报错
这份证明的骨架相当精巧。
它按任意两个电子之间最小内积 m 的取值，把整个构型空间切成几块。
一块一块来。
第一块里，没有任何一对电子接近反极点。
模型用了一个五次三点半定规划边界。
再配上内核能直接检验的精确整数数据。
结论是这一块里任何摆法的能量都高出五角双锥不少。
第二块更棘手。
那里存在接近反极点的电子对。
模型把这一块继续切细。
中间五片各用一份严格凭证排除。
最靠近极点的一片，交给高精度凭证去压。
它给出的能量下界只比五角双锥低 2.3×10⁻¹⁶。
窗口很窄。
接着是收口的一步。
所有数值凭证都被舍入并转成精确整数与有理数。
整个证明就此脱离浮点误差。
也脱离了外部求解器的依赖。
从头到尾都建立在精确代数运算上。
验证结果摆在那里。
Lean 内核全量编译 599 秒通过，其中编译环节占 344 秒。
独立内核 nanoda 校验了 47854 个声明。
零错误。
负对照实验里，只改动数据中的一个整数，nanoda 立刻中止。
改动一个整数就报错。
这是形式化验证给出的可信度。
四、从会解题走向会做研究
过去说 AI 做数学，指的是它会解题。
给一道竞赛题，吐出一个答案。
现在被接管的是一整条研究链条，从找证明路线、并行试错，一直到机器验收。
这已经不是一次普通的 AI编程，而是一条研究链路的自动化。
差别就在这里。
人类数学家花了几十年没做成的事，十个模型用了一个通宵。
而且全程没有人类插手。
它们自己建群，自己讨论，自己分工，自己合并代码，自己通过验证。
它们不只是证明了一个百年猜想，还顺手证明了一件更大的事：AI 已经准备好和人类一起做数学了。
回到那道球面上的电子排布题。
它挂在那里 122 年。
被补上的这一刻，没有掌声也没有署名。
只有一份能一行行编译的证明文件。
对普通读者来说，这件事的意义不在一道题的胜负，而在它把研究的边界又往前推了一格。
它说明 AI工具 正在从帮我算走向替我做。
当一个模型能自己组队、自己试错，还能把结果交出去被人一行行检验，它离真正的科研伙伴就近了一步。
至于这条路能走多远，答案得由下一份证明来写。
Claude Code会员中转站 微信:douhanq
