AI首次完整验证庞加莱猜想 4人小队470万行Lean

时间：2026年9月27日凌晨3时38分（美东时间），对应北京时间9月27日15时38分 地点：美国加州大学圣迭戈分校（UCSD）数学系 Lean 形式化数学项目，叠加 GitHub 开源社区 Lean-mathlib 与全球数学家协作网络 人物：丘成桐（菲尔兹奖得主、清华大学与中科院晨兴数学中心教授）；Ben Chow（UCSD 数学教授，1986 年丘成桐普林斯顿博士生，几何与 Ricci 流专家）；秦梓扬 Ziyang Qin（康奈尔今年 5 月本科毕业，仓库 11,000+ 次提交中 7,477 次挂其名下）；廖源 Yuan Liao（UCSD 博士生）；Ayush Khaitan（普林斯顿，9 月加入冲刺） 事件详情：在 Lean 证明助手与 GitHub 公开仓库内，Ben Chow 四人小团队以"AI Agent 顶会"形式指挥 ChatGPT Astra、Claude Fable 5.1、OpenAI Codex 等大模型，把 2002-2003 年俄罗斯数学家 Perelman 关于庞加莱猜想的证明完整形式化为约 470 万行 Lean 代码。其中约 270 万行是最后两周冲刺时由 AI 完成。系统分四层协作：人类选定义、定命题；Claude Fable 作为"领队"守住数学路线；后台调度 Agent 拆活、派活、验收；一群临时 Agent 写完一段就退；Claude 交叉互验后提交 Lean 内核检查。最终成品 0 处"sorry"占位、全部通过 Lean 类型检查与机器审计。 背景：1904 年法国数学家亨利·庞加莱提出"任何紧致、单连通、无边界的三维拓扑流形与三维球面同胚"的猜想；2002-2003 年 Perelman 在 arXiv 连发三篇论文用 Ricci 流方法给出关键证明，但具体步骤只写结论，2006 年才被 Hamilton、Tian 等数学家写成几百页详细版本。2025 年秋，丘成桐悬赏 10 万元人民币征集对 Poincaré 猜想的完整形式化验证；同年 Ben Chow 与弟子办起 Lean 线上学习班，并花 7 个月先把约 200 万行分析、微分几何、黎曼几何基础数学写进 Mathlib。 影响：这是千禧年七大数学难题之一首次被机器完整验证、AI 在冲刺阶段贡献 60% 以上的代码，证明"AI Agent + 人类数学家"已从实验走向千克级数学证明的工业生产。斯坦福数学家 Jared Duker Lichtman 连发两条感叹号评论；丘成桐宣布将奖励团队；Anthropic、OpenAI 等公司已悄悄布局"AI 数学家"研发。 总结：一老一少、四位数学家 + 一群 24 小时连轴转的 AI，把悬而未决近百年的庞加莱猜想写成 470 万行 Lean 代码并由机器打分——这是千禧年难题首次被 AI 完整形式化验证，AI 协手数学跨过临界点。 参考来源： - https://www.huxiu.com/article/4894253.html - https://finance.sina.cn/stock/jdts/2026-09-28/detail-initkarh2961862.d.html - https://m.sohu.com/a/1081733408_122066679 - https://36kr.com/p/4002565371056257 - https://news.pedaily.cn/202609/569689.shtml - https://hub.baai.ac.cn/view/57747 - https://github.com/qinz1yang/differential-geometry