470万行代码、两周写完：Thurston几何化猜想被完整形式化了，这次有英伟达入局

九月底，AI 形式化验证「庞加莱猜想」的消息还没凉透，这周又有更大动静。普林斯顿学者 Ayush Khaitan 牵头，联合 NVIDIA Humanfia 团队（Jui-Hui Chung、Ligeng Zhu），以及丘成桐弟子、加州大学圣地亚哥分校数学系教授 Bennett Chow（周培能），把 Thurston 几何化猜想在 Lean 里完整形式化了。整个证明大约 470 万行代码，新写的部分约 270 万行，官方说法是"两周左右"搞定。斯坦福数学助理教授 Jared Duker Lichtman 的评价是"确实令人惊叹的工作"。

先弄明白它到底证明了什么——它不是简单地把庞加莱猜想重做了一遍。

庞加莱猜想说的是：三维空间里所有封闭曲线都能缩成一点，那这个空间是不是等价于三维球面。佩雷尔曼在 2002 到 2003 年用三篇预印本证明了它，随后拒领百万美元奖金。但庞加莱只是更大蓝图的一角，那个蓝图叫 Thurston 几何化猜想——它给整个三维宇宙列了一张"元素周期表"：任何三维流形都能被精确切分成几块，每一块必然属于 8 种标准几何结构中的一种。佩雷尔曼当年正是通过证明 Thurston，才"顺手"证明了庞加莱。

他的工具是 Ricci 流与手术理论。说白了，就是把扭曲的空间放一个"几何熨斗"上去熨平，遇到熨不平的奇点，做一次"外科手术"剪掉封口再继续。这套东西有多深？哪怕是世界上最顶尖的几十位数学家，要完全核验佩雷尔曼的证明也花了整整两三年。现在这堆东西被塞进计算机、变成一行行代码，含金量不难想见。

翻开 GitHub 仓库 differential-geometry（github.com/qinz1yang/differential-geometry），能直接感到什么叫硬核。Lean 这个交互式定理证明器不认"显然可得"，只认最底层的逻辑公理。要让机器理解 Thurston，团队得从零定义整个宇宙的规则，填补了大量 Lean 官方数学库 Mathlib 缺失的基建，从底层重构黎曼几何——流形、切丛、张量场、黎曼度量，全都要用泛型编程严密定义。论文里 Ricci 流不过一行偏微分方程，到了代码里就是成千上万行：时间依赖的度量演化、Ricci 曲率张量的局部计算、偏微分方程解的存在性边界。最难的手术理论部分，团队把奇点处理拆成拓扑连通和几何分解算法，让"剪裁缝合"变成计算机能一步步运行校验的逻辑树。

最有讨论价值的，还是两周 270 万行到底怎么写完的。一个 270 万行的项目，搁在软件工程里，足够让几十人的资深团队加班一整年；而在每行代码都要经受长编译验证时间的 Lean 里，纯人力几乎不可能。答案指向 NVIDIA 的算力和大模型接过的代码生产线。不过得说清楚，官方至今没有公开所有 AI 生成的细节，对这条"工业化证明流水线"的描述，更多是从代码量暴增反推出来的——数学家负责拆解出引理和子目标，NVIDIA 团队用 LLM 和自动化脚本生成底层证明代码、补全代数推演和边界条件穷举，最后全部送进 Lean 编译器做"逻辑质检"，不通过就打回重写。

这里想泼一点冷水，倒不是怀疑成果本身，而是别把它理解成"AI 自己会做数学了"。现在的大模型在长链条逻辑推理上依然有幻觉，数学形式化恰好是暴露和约束这种缺陷的窗口。能生成通过 Lean 校验的证明代码，说明 AI 在"被人类圈定的推理轨道"上能把活干得很扎实，但距离它自己提出新猜想并给出证明，还隔着一条鸿沟。材料里那句话其实点到了要害：这更像是一套经过绝对真理验证的微分几何代码库，以后要在计算机里研究多维流形、黑洞几何结构、时空演化的人，可以直接调库了。

所以这件事的价值，我倾向看成是给数学界铺了一段高速公路，而不是某家公司的能力秀。它在 GitHub 上全面开源，等于把一个人类智力巅峰的证明浓缩成可复用、可核验的数字资产。至于它会不会真的让 AI 进入高阶几何的"无人区"、催生新的猜想，那是下一棒的事，现在断言还太早。先把这几百万行代码跑通、让同行能复现，本身就足够让人兴奋了。

参考资料：Ayush Khaitan 推文（https://x.com/ayushkhaitan343/status/2108654050203840528）、GitHub 仓库（https://github.com/qinz1yang/differential-geometry）