庞加莱猜想被写成470万行Lean代码，AI两周赶出270万行
新智元 · wechat · 2026-09-28
丘成桐弟子、UCSD教授 Ben Chow 带队，与刚本科毕业的 Ziyang Qin 等四人合作，用证明助手 Lean 把 Hamilton 与佩雷尔曼的庞加莱猜想证明完整形式化，共约470万行代码并通过 Lean 内核检查、无一处 sorry，其中约270万行是最后两周借助 ChatGPT Astra 与 Claude Fable 赶工完成的。
分析显示佩雷尔曼三篇论文对应的代码仅约66万行、占比六分之一，其余是论文默认读者已懂的基础数学：分析学约109万行、微分几何约77万行；单是典范邻域定理就用了272万行。团队采用「AI管AI」的多智能体工作流：Claude 领队守数学路线并验收，调度智能体拆活派活，临时智能体写证明，还曾让 Claude 把拓扑章节拆成并行任务线交给 OpenAI Codex 执行，人类负责审定命题。作者认为这预示数学家精力将从写证明转向判断该证什么、并审查 AI 的产出。
所属事件:庞加莱猜想证明完成 Lean 形式化，代码达 470 万行(3 条相关)→
「研究」频道最新
- 4.5MB 无 Transformer 语言模型 MICA 分家:Ember 与 Flame 评测进展 — Silver_Employ2617 · 2026-09-28
- Anthropic 可解释性研究梳理：Claude 有可报告的「全局工作区」表征 — ctjlewis · 2026-09-28
- Yoav Goldberg 质疑:新模型发布两周 arXiv 已涌现 29 篇论文 — yoavgo · 2026-09-28
- 数据效率被视为人类最后优势,但海量喂料仍是最便宜路径 — himanshustwts · 2026-09-28
- 北大与谷歌提出 Harness-Zero:把 Agent 框架蒸馏进模型权重 — AxSaucedo · 2026-09-28
- MultiFlow 用耦合流匹配预测单细胞多组学扰动响应 — burny_tech · 2026-09-28