10个Claude通宵15小时，证明122年物理数学难题

球面上的7个电子，难住了人类数百年。今天，10个Claude Sonnet 5.5通宵15小时，互发1270条消息，写出17895行Lean代码，完成了汤姆逊问题N=7的证明。没有人类介入，没有预设分工，10个Claude自己建群、讨论、选算法、合并代码。证明通过了Lean内核和独立内核nanoda的双重验证，改一个整数，nanoda立刻报错。

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。但模拟不是证明，无法排除某处隐藏着能量更低的“幽灵构型”。

Vals AI的Hung Tran把任务交给10个Claude组成的虚拟实验室。人类只给定任务边界：两个固定Lean定理陈述和九个探索方向，智能体全部调到最大算力投入。15小时内，1270条技术讨论消息，有的试错贴出失败，有的改进，有的发现路径可合并。一个Claude主动认领“集成者”，把验证通过的零件塞进Solution.lean。硬规矩只有一条：没过检查器的不算，必须从零复现编译、与题面一字不差、不许偷加公理。

最终得到17895行Lean形式化证明。核心策略是按任意两个电子间最小内积m的值，把连续构型空间切成区域逐个击破。区域一m≥-0.90，用5次三点半定规划边界配合精确整数数据，证明能量高于五角双锥至少3×10⁻⁴。区域二m<-0.90，继续细分：[-0.99,-0.90]的五个切片各用严格三点凭证排除，高出最优能量约2.6×10⁻⁶；极冠区域m≤-0.99由高精度凭证约束，能量下界只比五角双锥低2.3×10⁻¹⁶，把潜在竞争者压缩到极窄邻域。随后用区间算术刚性论证和精确二阶局部极小值定理锁定唯一性。所有数值凭证全部舍入转换为精确整数与有理数，脱离浮点误差和外部求解器依赖。

验证结果：Lean内核全量编译599秒通过，lake build耗时344秒，完成8928个编译任务；独立内核nanoda校验47854个声明，零错误；负对照实验中，仅改动证明数据里的一个整数，nanoda立刻报错中止。

过去说AI做数学，指的是“会解题”。现在，一整条研究链条正在被Agent接管：找证明路线、并行试错、裁决哪条路值得走、把代码合进一个文件、交给机器验收。数学AI正从“会解题”走向“会做研究”。人类数学家花几十年没做到的事，10个AI只用了一个通宵，全程没有人类插手。它们不只证明了一个百年猜想，也证明了一件事：AI已经准备好，和人类一起做数学了。