（来源：新智元）
新智元报道
球面上的7个电子，竟难住了人类数百年。
就在今天，10个Claude Sonnet 5.5，通宵15个小时，互发1270条消息，写出17895行Lean代码。
结果，把一道悬了122年的物理数学难题——汤姆逊问题N=7，直接完成证明了！
没有人类介入，没有预设分工。
十个Claude 5.5自己建群、自己吵架、自己选算法、自己合并代码。
最恐怖的是，这份证明通过了Lean内核和独立内核nanoda的双重验证。改一个整数，nanoda立刻报错。
这一刻，标志着AI不只是会解题了。AI开始自己做研究了。
「七星连珠」之谜
困扰物理界百年
1904年，发现电子的J.J.汤姆逊，提出了著名的「葡萄干布丁」原子模型，想弄清电子在原子里怎么排布。
模型后来被卢瑟福推翻了，但留下的这道题活了下来，名字就叫「汤姆逊问题」。
这个问题，听起来巨简单——
把N个电子扔到一个球面上，彼此排斥，怎么站，总能量最低？
注意，是总能量最低。只把某两个电子拉远，可能会把其他几个挤到一起。
过去的122年里，被严格证完的只有寥寥几个：
2、3、4、6、12个点，靠几何对称性解决；
5个点，拖到2013年，数学家Richard Schwartz借助计算机才证完；
8个点，就在今年9月18日，由Kryvonos、Liehr、Taylor三位数学家挂上arXiv，并用Lean做了形式化。
而7，夹在中间，一直空着。
数十年来，世界各地的超级计算机跑了无数次数值模拟，所有结果都指向同一个优美的直觉构型——「五角双锥」（Pentagonal Bipyramid）：
赤道上均匀分布5个电子，南北两极各钉死1个，理论能量值约等于14.4529774142
数值模拟能跑出一万次这个数字，但模拟不是证明。
只要没有逻辑上的绝对闭环，就永远无法排除在某处极其晦涩的微小折角里，藏着一个能量更低的「幽灵构型」。
百年来，人类始终拿不出对N=7的完备、严密数学形式化证明。
直到来自Vals AI的Hung Tran，把这个任务交给了由10个Claude组成的虚拟实验室。
10个Claude 5.5组队
通宵15h开会
这场实验里，人类先把任务边界钉牢。
他们把10个Claude Sonnet 5.5智能体，全部调到「最大算力投入」状态，扔进一个交互看板和Lean证明环境里，目标只有一个：
证明「五角双锥」是7个电子在球面上的最低能量排布。
没有给它们具体步骤。只给了两个固定的Lean定理陈述，以及九个可能的探索方向。
接下来15个小时，全交给它们。1270条技术讨论消息。
有的Claude试一条路走不通，把失败贴上来；有的接着改；有的发现两条路其实能合并。
后来，其中一个Claude主动认领了「集成者」的角色，把各路验证通过的零件，一块块塞进同一个文件Solution.lean。
硬规矩只有一条：没过检查器的，一律不算。
必须能从零复现编译、必须和题面一字不差地对上、不许偷偷加公理。
最终，得到了一份17,895行Lean形式化证明。
改一个整数，就报错
这份证明的核心策略，极其精巧。
它按任意两个电子之间最小内积m的值，把整个连续构型空间切成几个区域，逐个击破。
区域一：m ≥ -0.90
这个区域里，没有任何一对电子「接近反极点」。
Claude用了一个5次三点半定规划边界，配合内核可直接检验的精确整数数据，证明该区域内任何构型的能量都高于五角双锥至少3×10⁻⁴。
区域二：m < -0.90
这个区域更棘手，存在接近反极点的电子对。智能体把它继续细分：
这是一个极其狭窄的窗口。
它把潜在的「竞争者」全部压缩到五角双锥的极窄邻域内。
然后，Claude用区间算术刚性论证和精确二阶局部极小值定理，彻底锁定唯一性。
最狠的一步来了：所有数值凭证，全部被舍入并转换为精确整数与有理数。
这意味着整个证明脱离了浮点误差，脱离了外部求解器依赖，完全建立在精确代数运算之上。验证结果：
改一个整数就报错。这是形式化验证最硬核的可信度证明。
数学AI，开始「做研究」了
过去说AI做数学，指的是它「会解题」：给一道奥赛题，吐出一个答案。
现在，一整条研究链条正在被Agent接管：找证明路线、并行试错、裁决哪条路值得走、把代码合进一个文件、最后交给机器验收。
数学AI，正在从「会解题」，走向「会做研究」。
人类数学家花了几十年没做到的事，10个AI只用了一个通宵。
而且，它们全程没有人类插手。它们自己建群，自己讨论，自己分工，自己合并代码，自己通过验证。
刚刚，10个Claude通宵15小时做了一件事。
它们不只是证明了一个百年猜想。它们证明了一件事：
AI已经准备好，和人类一起做数学了。
参考资料：
https://x.com/ValsAI/status/2104757086462914888?s=20
https://www.vals.ai/blogs/thomson-n7-lean-proof
https://github.com/huwngtran/thomson-n7-lean
编辑：桃子
