7.9
深览指数
科技虎嗅·新智元··AI 生成
丘成桐弟子带AI狂写470万行，庞加莱猜想证明首次被机器完整验证
一个四人团队（领衔者为丘成桐弟子、UCSD教授Ben Chow）使用数学证明助手Lean，将庞加莱猜想的完整证明形式化为约470万行代码，并通过了Lean内核的自动检验。其中约270万行是在最后两周借助ChatGPT、Claude等AI助手完成的。文章详细拆解了代码分布——佩雷尔曼的原论文仅占六分之一，其余均为填补隐含前提的基础数学——并披露了团队设计的AI协作架构（领队-调度-临时智能体）。这一成果的核心意义不在于证明了新定理，而在于展示了「AI辅助+形式化验证」如何将人类数学家从繁琐的证明书写中解放出来，转向更高层的判断工作。适合对AI在科学/数学研究中的实质应用、形式化验证、以及长期数学难题攻克感兴趣的深度读者。原文 ↗
核心观点
- ▍庞加莱猜想的完整证明已被四人团队借助AI助手全部形式化为470万行Lean代码，并通过了机器内核的自动验证，这是首个千禧年难题的完整机器验证版本。
- 01代码总约470万行，其中约270万行是在最后两周由ChatGPT Astra、Claude Fable等AI助手协助完成。
- 02佩雷尔曼三篇原始论文对应的代码仅约66万行，占总代码量的六分之一；其余六分之五为佩雷尔曼默认读者已知的基础数学（分析学约109万行，微分几何约77万行）。
- 03团队设计了三层AI架构：最上层的「领队」AI（守数学路线）、后台长期运行的「调度」智能体（拆活、派活、验收）、以及临时退出的「执行」智能体（写证明、挑错）。
- 04核心定理「典范邻域定理」占用了272万行代码，是整个依赖链的三分之二。
- 05团队采用先搭结构骨架、再用「sorry」占位后陆续填充的策略，而非逐节线性推进，将原本预估6-10周的工作压缩至不到一周完成。
- 06所有402万行代码最终服务于一个23行的文件，该文件包含了庞加莱猜想的正式定理表述。
- 07跨接拓扑与光滑版的「Moise定理」代码达46万行，比手术部分多出一倍。
反方 / 局限
- — 文章未主动讨论该成果的数学圈争议（例如形式化证明是否等同于「理解了」证明，以及Lean内核本身的正确性假设），也未提及其他形式化工具（如Coq、Isabelle）的对比或局限。
庞加莱猜想Ricci流LeanBen ChowZiyang Qin丘成桐格里戈里·佩雷尔曼Ayush KhaitanClaude FableChatGPT AstraMoise定理Mathlib加州大学圣地亚哥分校 (UCSD)典范邻域定理
16 分钟 · 4 卡片 · 6 资料
读原文 →