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」频道最新
- 同一 SQL 分析任务，Sonnet 比 Haiku 贵约 12 倍 — sh_reya · 2026-11-16
- Rust 时间库 Jiff 发布 1.0,uv、Cargo 等已在生产环境采用 — charliermarsh · 2026-11-16
- Agent 检测到 Mac 电量仅 3%,主动暂停任务提醒充电 — adonis_singh · 2026-11-16
- 开源 ComfyUI 插件 Plenio 2.0：18 秒点歌到出歌的本地派对系统 — Vivid_Promise1700 · 2026-11-16
- AI 时代编程语言将分三类:自然语言、高性能代码与中间态规范 — dbreunig · 2026-11-16
- 把编辑部修改意见变成 AI 检查项,四大模型摘要得分提升 25+ 分 — danshipper · 2026-11-16