庞加莱猜想被机器完整验证了：470 万行代码，一个 22 岁本科生提交了 68%，佩雷尔曼的心血只占六分之一
AI飞行客 庞加莱猜想被机器完整验证了：470 万行代码，一个 22 岁本科生提交了 68%，佩雷尔曼的心血只占六分之一
人类数学史上最著名的难题之一，刚刚被整个写成了代码。
不是被”证明”——佩雷尔曼 2003 年就证明了。而是被完整形式化、逐行验证、零 sorry。
一个四人小团队，用 Lean 4 把 Hamilton 和佩雷尔曼的证明从头写到了尾，总共约 470 万行代码。最后一行：
`theorem poincare_conjecture : ∀ M : manifold3, compact M → simply_connected M → ∂M = ∅ → M ≃ₕ S³`
通过了 Lean 内核的终极校验。没有 sorry，没有 admit，没有”待后续补全”。
先说清楚这件事为什么难
1904 年，庞加莱问了一个问题：如果一个封闭三维空间里，任何闭合绳圈都能缩成一点，它是不是一定等价于三维球面？
佩雷尔曼的答案是”是”。方法很暴力——用 Ricci 流当熨斗把空间”烫平”。但哑铃状空间会在细腰处”啪”地断裂，产生无穷曲率奇点。他的破局点是一把数学手术刀：在断裂前 0.0001 秒，精准切开”颈部”，扔掉病灶，缝上两个标准球帽，再继续熨烫。
2006 年，数学界花了好几年同行审查，才敢说”没毛病”。佩雷尔曼甚至因为拒绝领菲尔兹奖而成了传奇。
而这次，说”没毛病”的不是同行，是机器的内核。 写证明的主力也不是人，是 AI。
一老一少 + 一群 AI
这支团队的构成，是 2026 年最硬核的人机协作样板。
Ben Chow（曹怀东），71 岁，研究 Ricci 流几十年的老教授，丘成桐的弟子。他不是来挂名的——他把自己当 Lean 新生，从 `#check nat.add_comm` 开始一行行敲代码。
Ziyang Qin，22 岁，康奈尔 2025 届本科毕业生，博士都还没入学。他以 7477 次提交（占总提交量 68%） 成为整个代码库的”心跳引擎”。
Ayush Khaitan（普林斯顿拓扑）负责 Moise 定理的 PL 武器库，并公开了所有 AI 调度协议。Yuan Liao（UCSD 博士生）啃最难的 Ricci 流短期存在性模块，曾为一行引理调试了 17 个版本。
他们没雇程序员，没招博士后。他们训练了一批”用完即焚”的临时 AI 智能体——写完一个引理就自我销毁，绝不污染知识图谱。
人类只做三件事：选定义、定命题、拍板”这正是我们要证的那个东西”。
最震撼的数字：佩雷尔曼只占六分之一
研究者把整个仓库下载下来，顺着最终的庞加莱定理，把它直接和间接引用的代码全部找了出来。
真正用到的有 14197 个代码文件、约 402 万行，最长的一条引用链串起了 353 个文件。
其中，佩雷尔曼三篇论文对应的代码加起来约 66 万行——只占六分之一。
剩下的六分之五是什么？是佩雷尔曼在论文里默认”读者早就懂了”的基础数学。 分析学约 109 万行，微分几何约 77 万行。
论文写得越简略，Lean 里要补的代码就越多。第三篇论文平均每页对应 1.4 万行代码。里面只用了一句话提到的”曲线缩短流”——让一根曲线一边缩短一边变圆——到了 Lean 里就写了 7.6 万行。
这是这次事件里最值得咂摸的细节。
一个反 hype 的判断：这不是”AI 会做数学了”
看到这里，很多人会直接得出”AI 攻破千禧年难题”的结论。
Stop。这个结论是错的。
佩雷尔曼的证明是对的，这件事 2003 年就确定了。这次完成的是形式化验证——把人类写的、大量依赖”不言自明”的高层数学，翻译成机器能逐行检查的代码。
这更接近于一座桥，而不是一项发现。
AI 在这里扮演的角色，是把六分之五的”默认共识”显式写出来。佩雷尔曼默认读者懂的基础分析、基础微分几何，AI 帮他补成了 300 多万行可验证的代码。这件事人类当然也能做，只是需要几十年——就像费马大定理、就像有限单群分类，每一个大型形式化工程都是一代人甚至几代人的工作量。
所以真正被改变的，不是”AI 会做数学”，而是”数学界终于有了一个能承接超大规模知识的容器”。
为什么这件事比”AI 会算题”重要得多
我上一轮写过 Claude 攻克杨-米尔斯九圈振幅，那是一个”AI 在一个定义良好的空间里填数独”的故事——规则清晰、验证明确、AI 天然擅长。
庞加莱猜想这事完全不同。它的意义在于：
当一项证明庞大到任何个人都无法从头复核时，人类第一次有了可靠的管理方式——把”人类判断 + AI 大规模推导 + 形式系统验证”三者绑在一起。
清华丘成桐团队做的 FormaTheoria 是同一个方向的另一个案例。他们用 7 个月完成了数学家 15 人花 6 年才做完的 Feit-Thompson 定理形式化，产出 99.4 万行代码、850 余个文件，最长依赖链 458 层。
丘成桐团队周源的话说得很准：”人类负责确定值得研究的问题并作出关键判断，AI 承担大规模搜索与推导，形式系统则确保每一个被接受的步骤都可以被重新检验。”
这三者结合的方式，或许将成为人类管理超大规模数学知识的一条全新路径。
给所有”知识工作者”的一个信号
如果你不是数学家，这件事对你也有一个直接的启示。
过去几年大家都在讨论”AI 会不会取代我”。庞加莱猜想这个案例给出的答案是另一个方向的：最先被 AI 改变的，不是那些”有明确答案的工作”，而是那些”人类内部靠默契和默认共识运转的工作”。
佩雷尔曼的论文之所以需要补 400 万行代码，恰恰因为数学界长期依赖一种隐性契约——”这些基础的东西大家都懂，不用写出来”。这种隐性契约是效率的来源，也是知识传承的裂缝。
AI 擅长做什么？把隐性变显性，把共识变代码，把”你懂我懂”变成”机器也能检查”。
这对任何行业都成立。你公司里那些”老员工才知道的规矩”、”大家都心照不宣的流程”、那些从没写进文档的默认操作——它们就是等着被形式化的 400 万行代码。
AI 去找它们，只是时间问题。