10个Claude通宵15h 攻克122年物理猜想

10个Claude通宵15h 攻克122年物理猜想 【时间】2026年9月30日（北京时间） 【地点】远程协作（Vals AI / Anthropic / 加州） 【人物】Vals AI 研究员 Hung Tran；10 个 Claude Sonnet 5.5 智能体；独立内核 nanoda 验证方 【事件详情】Vals AI 宣布，10 个 Claude Sonnet 5.5 智能体在「最大算力投入」模式下协作 15 小时，互发 1270 条消息，最终产出 17895 行 Lean 形式化代码，首次完成对汤姆逊问题 N=7 情形的严格数学证明——证明 7 个电子在球面上的最低能量排布正是「五角双锥」（赤道 5 个、南北极各 1 个，理论能量约 14.4529774142）。人类只给定 2 条 Lean 定理陈述和 9 个探索方向，全程不介入分工；其中一个智能体主动认领「集成者」角色，把通过验证的零件合并进单一 Solution.lean。验证流程包括 Lean 内核全量编译（599 秒通过、8928 个编译任务）、独立内核 nanoda 校验 47854 条声明零错误，以及负对照实验（仅改动一个整数即报错）。 【背景】汤姆逊问题由 J.J. 汤姆逊于 1904 年提出，是将 N 个电子放在球面上求最小库仑能的几何极值问题。过去 122 年里，N=2、3、4、6、12 由几何对称性证明，N=5 由数学家 Richard Schwartz 于 2013 年借助计算机证明，N=8 由 Kryvonos、Liehr、Taylor 于今年 9 月 18 日挂在 arXiv 并用 Lean 形式化。N=7 一直悬而未决：数值模拟一万次都指向「五角双锥」，但缺乏形式化闭环，无法排除「幽灵构型」。值得一提的是，就在 10 月 1 日之前，OpenAI、DeepMind 等机构在 Lean 形式化数学和「AI 自动研究」方向也在加速布局，但团队级别、跨问题门类的全自主验证案例尚属首次。 【影响】1）数学层面：把一个开放 122 年的物理-数学猜想写进 Lean 内核，为后续 N=9、N=10 及更高情形的链式证明提供方法样板；2）AI 能力层面：标志「AI 会解题」向「AI 会做研究」的关键跃迁——路线发现、并行试错、裁决、合并、机器验收，整条研究链条由 Agent 全程接管，无人类干预；3）形式化验证生态：把「数值证书 → 精确整数/有理数」的转换流程沉淀为可复现模板，nanoda 这类独立内核可成为机器学习结果可信度的硬约束；4）企业研发：Vals AI 凭此展示多智能体在长时间跨度、复杂符号任务上的协调能力，对自动化证明、芯片验证、密码学证明等场景具有直接商业价值。 【总结】这是「AI 自己做研究」的一个标志性时刻——10 个 Claude 不是在「答题」，而是用 15 小时的通宵会议，自主发现路线、互相裁决、合并代码，并通过双重内核验证，最终把一道悬了 122 年的物理猜想压成了 17895 行可机检的 Lean 代码。从「解奥赛题」到「主导整条研究链」，AI 形式化数学的能力曲线在这一夜出现了一个明显拐点。 【参考来源】 1. 36氪：刚刚，十个Claude 5.5攻克百年物理猜想 - https://www.36kr.com/p/4005646894157699 2. AGI Hunt（英文）：10 Claude Agents Solve 122-Year-Old Thomson Problem in 15 Hours - https://agihunt.info/en/e/1a0eb206dc00421d8c4cc7ffb89 3. AlphaSignal：Vals AI's Ten Claude Agents Formally Prove a Century-Old Math Problem - https://alphasignal.ai/news/vals-ai-s-ten-claude-agents-formally-prove-a-century-old-math-problem 4. TipRanks Blog：Vals AI Showcases Advanced AI-Driven Formal Proof Capabilities - https://blog.tipranks.com/vals-ai-showcases-advanced-ai-driven-formal-proof-capabilities 5. 新浪看点：刚刚，十个Claude 5.5攻克百年物理猜想 - https://k.sina.cn/article_5953190046_162d6789e06703ter0.html 6. AGI Hunt（中文）：10 个 Claude agent 15 小时用 Lean 证明最短路算法新上界 - https://agihunt.info/p/1a0cad08c64dca949b1aff5b3e5 7. 论文 / 仓库：github.com/huwngtran/thomson-n7-lean（Solution.lean + 论文 + 一键验证脚本）