10个Claude通宵15小时,1.8万行Lean证明122年汤姆逊难题
新智元 · wechat · 2026-09-30
ValsAI 的 Hung Tran 让 10 个 Claude Sonnet 5.5 智能体在最大算力投入下,只给了两个 Lean 定理陈述和九个探索方向,自主完成了悬置 122 年的汤姆逊问题 N=7(7 个电子在球面上的最低能量排布为五角双锥)的形式化证明。
- 全程无人类介入:15 小时内互发 1270 条消息,自行试错、分工,其中一个智能体主动认领「集成者」角色合并代码
- 产出 17,895 行 Lean 证明:按电子对最小内积 m 划分构型空间逐区域击破,所有数值凭证舍入为精确整数与有理数,彻底消除浮点误差
- 验证过硬:Lean 内核全量编译 599 秒通过;独立内核 nanoda 校验 47,854 个声明零错误;改动任一整数即报错
背景:汤姆逊问题源自 1904 年 J.J. 汤姆逊的原子模型,此前严格证明的只有 N=2、3、4、5、6、12 等少数情形。此次实验标志着 AI 从「会解题」走向自主开展研究:自己找路线、并行试错、裁决、合并、通过机器验收。
所属事件:10 个 Claude 智能体 15 小时证出百年 Thomson 难题(3 条相关)→
「编程与Agent」频道最新
- 语音平台一线实测:GPT-Live-1 对话自然,Gemini 3.8 Live 工具调用不卡顿 — VladimirSamukov · 2026-10-01
- 语音+代理式电脑操作被指是未来交互,Clicky 团队加速推进 — thealexbanks · 2026-10-01
- antirez:新手别靠读 AI 代码成长,该手写解释器和游戏 — antirez · 2026-10-01
- 扛不住 AI 生成 PR 洪水，Rust 编译器 swc 停收外部贡献 — DanielLockyer · 2026-10-01
- DeepSeek harness 0.2 发布:桌面版上线,Agent 权限修复与异步问答落地 — WebAssemblyMan · 2026-10-01
- Obsidian 插件把知识库变成 MCP 技能目录，省下数万 token — dSebastien · 2026-10-01