10 个 Claude 攻破 Thomson 百年难题

时间：2026年9月29日（美国西部时间） 地点：美国（线上虚拟实验室，由 Vals AI 主导） 人物：Vals AI 研究员 Hung Tran（项目主导者）；Anthropic Claude Sonnet 5.5（10 个智能体组成的虚拟研究团队） 事件详情：AI 评测公司 Vals AI 的研究员 Hung Tran 在2026年9月把10个 Claude Sonnet 5.5 智能体调到最大算力、扔进交互看板和 Lean 形式化证明环境，目标是在无人持续干预的前提下，用15小时解决自1904年起悬而未决的 Thomson 问题的 N=7 情形——证明"五角双锥"是7个电子在球面上的最低能量排布。10个智能体在15小时内交换1270条技术讨论消息、自主认领"集成者"角色并把通过 Lean 检查器的零件整合到 Solution.lean，最终交付了一份17895行的形式化证明。Lean 内核全量编译耗时599秒完成8928个编译任务，独立第三方内核 nanoda 进一步核验47854个声明无误；任何对该证明任一处的整数篡改都会立刻导致编译失败。 背景：Thomson 问题自 J.J. Thomson 在1904年为理解原子内部电子排布而提出，是数学物理中最经典的离散几何问题之一，长期以来只有少数小 N 情形有严格证明。本次突破建立在2026年9月由 Kryvonos、Liehr、Taylor 与 Tooby-Smith、Zughaid 等人给出的 N=8 与 Lean 形式化方法基础上；Vals AI 把"AI 找证明路线 → 并行探索 → 自动合并 → 通过形式化验收"完整研究链条作为评估大模型在严肃科研任务中的能力上限，并已在今年早些时候完成 a16z 领投的4000万美元 A 轮融资，估值4亿美元。该实验的诚实免责声明同步出现在 GitHub 仓库首页：声明未经人工校对、尚未同行评审。 影响：这是 AI 从"会解题"迈向"会做研究"的标志性案例。研究链条（路线发现、并行试错、裁决、代码合并、机器验收）首次实现端到端无人值守。Thomson 问题的形式化证明为数学物理中的高维离散几何问题提供新范式：把数值凭证转换成可验证的整数与有理数、脱离浮点误差依赖，将使后续物理与材料科学中的几何优化问题受益。值得注意的是，这并非 AI 提出全新物理定律，而是基于人类已有的方法扩展到未被证明的角落。 总结：10个 Claude Sonnet 5.5 智能体用15小时、1270条消息、17895行 Lean 代码、5层验证，把 Thomson 问题的 N=7 情形从1904年悬而未决的百年猜想变成了机器可核验的完整证明，标志着 AI 正式进入"会做研究"的新阶段。 参考来源： 1. 36氪：https://36kr.com/p/4005646894157699 2. AGI Hunt（英文）：https://agihunt.info/en/e/1a0eb206dc00421d8c4cc7ffb89 3. AlphaSignal：https://alphasignal.ai/news/vals-ai-s-ten-claude-agents-formally-prove-a-century-old-math-problem 4. Startup Fortune：https://startupfortune.com/ten-claude-agents-wrote-a-17895-line-proof-for-a-1904-physics-problem 5. 今日头条：https://www.toutiao.com/article/7691161847004725801/