四人团队借助AI将庞加莱猜想证明形式化，470万行代码全部通过Lean内核检查

9月28日，由加州大学圣迭戈分校教授Ben Chow带队，Ziyang Qin、Yuan Liao、Ayush Khaitan组成的四人团队宣布，已用证明助手Lean完成庞加莱猜想证明的完整形式化验证。整个证明共约470万行代码，全部通过Lean内核检查，没有一处使用sorry占位。

庞加莱猜想是1904年提出的千禧年难题之一，由佩雷尔曼在2002年底至2003年以Ricci流等工具证明。此次形式化工作将Hamilton与佩雷尔曼的证明从头到尾写入Lean，直接和间接引用的代码共14197个文件、约402万行。团队表示，最后两周约270万行代码是在ChatGPT、Claude等AI辅助下完成的。

Ben Chow是丘成桐在普林斯顿大学的博士弟子，长期研究Ricci流。2025年秋天他开始组织Lean线上学习班，并与Ziyang Qin、Yuan Liao先用七个月写出约200万行基础代码；2026年9月，普林斯顿的Ayush Khaitan加入，共同完成最后冲刺。据Khaitan介绍，主力AI为ChatGPT Astra，部分难啃章节由Claude Fable完成；人类成员负责选定义、定命题，确认Lean里证出的内容正是数学家想证明的结论。

在依赖链中，佩雷尔曼三篇论文对应约66万行代码，典范邻域定理相关证明约272万行，约占依赖链的三分之二。最终，庞加莱猜想被写成23行文件中的定理：任何紧致、单连通、无边界的3维拓扑流形都与三维球面同胚。