丘成桐弟子再立功，广义庞加莱猜想证明首次形式化验证

数学界刚刚传来一则重磅消息。

今年9月，AI成功完成了“庞加莱猜想”的形式化验证，当时已令学界震撼。

而如今，由Ayush Khaitan领衔的顶尖学术团队，携手NVIDIA Humanfia团队，终于将Thurston几何化猜想的完整证明在Lean中实现了形式化！

哈密尔顿-佩雷尔曼那份被誉为“世纪证明”的文献长达数百页，即便是顶尖人类学者也需要数年才能消化。

继今年9月攻克庞加莱猜想之后，这次在AI的助力下，这一经典证明终于被转化成了代码。

470万行代码，仅用了大约两周时间。

这不仅是数学史上的又一座里程碑，更标志着AI辅助高阶几何分析进入了“狂飙时代”。

AI辅助形式化数学，已经正式踏入了人类最深奥的高阶几何分析“无人区”。

惊叹！庞加莱被推广到完整几何化猜想

如果有人告诉你，有一支团队在两周内写出了470万行零错误的现代数学代码，你可能会觉得难以置信。

但这正是刚刚发生的事实。

近日，斯坦福大学数学助理教授Jared Duker Lichtman惊叹道：

这确实是一项令人惊叹的工作。

庞加莱证明被推广到了完整的几何化猜想，而这一切，全部在Lean中完成了！

发布成果的是普林斯顿数学与AI学者Ayush Khaitan。他在推文中介绍了这次超强的跨界阵容。

看看这份硬核的团队名单：

Bennett Chow（周培能）：丘成桐弟子、加州大学圣地亚哥分校数学系教授，Ricci流领域的绝对权威和泰斗级人物。

Ziyang Qin与Yuan Liao：项目形式化工作的绝对主导者。

Ayush Khaitan：普林斯顿大学学者，项目的核心推手。

NVIDIA Humanfia团队（Jui-Hui Chung & Ligeng Zhu）：代表全球最强AI算力巨头英伟达的前沿力量。

在这支超级团队的协作下，奇迹诞生了。

Ayush透露，该证明大约有470万行代码。

在Chow、Liao和Qin此前约200万行代码的工作基础上，新增的270万行代码在短短大约两周内就编写完成！

目前，这项伟大工程已全面开源在GitHub上。

https://github.com/qinz1yang/differential-geometry

降维打击：从“庞加莱”到“全几何化猜想”，他们究竟证明了什么？

为何让斯坦福数学家如此激动？

我们首先得知道Thurston几何化猜想到底难度几何。

大家都听说过**“庞加莱猜想”**。

它探讨的是：如果一个三维空间中所有的封闭曲线都能收缩成一点，那么这个空间是不是一定等价于一个三维球面？

2002年到2003年，俄罗斯数学鬼才格里戈里·佩雷尔曼横空出世，用三篇预印本论文证明了庞加莱猜想，随后拒领百万美元奖金，深藏功与名。

但庞加莱猜想其实只是一个宏大蓝图的“冰山一角”。这个蓝图，叫做“瑟斯顿几何化猜想”。

换句话说，庞加莱猜想是教你如何认出一个“圆球”，而瑟斯顿几何化猜想则是给整个三维宇宙列出了一张“元素周期表”。

它指出：任何三维流形，最终都可以被精确地切割成几块。更重要的是，每一块都必然属于8种标准几何结构中的一种！

当年，佩雷尔曼正是通过证明了瑟斯顿几何化猜想，从而“顺手”证明了庞加莱猜想。

他使用的绝招，叫作**“Ricci流与手术理论”**。

这就好比是用一个“几何熨斗”（Ricci流方程），把扭曲的空间熨平。遇到熨不平的死结（奇点），就做个“外科手术”把它剪掉、封口，然后继续熨。

这套理论极其深奥，即便是世界上最顶尖的几十位数学家，要完全验证佩雷尔曼的证明也花了两三年时间。

而今天，这群伟大学者和工程师，把这套人类智力巅峰的理论，原原本本地塞进了计算机的脑子里！

Thurston几何化猜想的完整Lean证明，意味着机器已经具备了处理高级微分几何、拓扑学和偏微分方程的能力。

机器正式杀入了高阶几何的“无人区”。

扒开GitHub代码库：这470万行代码到底写了什么？

如果你打开这个名为differential-geometry的GitHub仓库，你会感受到强烈的“硬核暴击”。

链接：https://github.com/qinz1yang/differential-geometry

这是一座用机器语言搭建的“现代微分几何数字长城”。

在Lean这个交互式定理证明器中，计算机不懂什么叫“显然可得”，它只认最底层的逻辑公理。为了让机器理解瑟斯顿几何化猜想，团队必须从零开始，在代码里定义整个宇宙的规则。

从仓库的技术细节来看，团队硬核填补了大量Lean官方数学库（Mathlib）中缺失的基础基建。

他们从底层重构了黎曼几何。

代码中定义了极其复杂的流形（Manifold）、切丛（Tangent Bundle）、张量场（Tensor Fields）以及黎曼度量（Riemannian Metrics）。

团队用严密的泛型编程，让机器终于“认识”了什么是弯曲的空间。

在传统的数学论文里，Ricci流不过就是一个偏微分方程。

但在GitHub的仓库中，团队需要用成千上万行代码，精确定义“时间依赖的度量演化”、“Ricci曲率张量的局部计算”以及极其复杂的偏微分方程解的存在性边界。

佩雷尔曼证明中最难的部分，当属**“手术理论”**。

如何在代码中实现对一个抽象空间的“剪裁”和“缝合”？

团队在代码库中引入了复杂的拓扑连通和几何分解算法，将几何上的奇点处理转化为计算机可以一步步运行、校验的逻辑树。

两周疯狂输出：NVIDIA入局，大模型接管“代码生产线”

最让人热血沸腾的，是这组数据：两周，新增近270万行代码，总计470万行。

在软件工程界，一个270万行的项目足以让一个几十人的资深开发团队连续加班一整年。

而在逻辑密度极高、每行代码都需要极长编译验证时间的Lean语言中，两周写完，纯靠人力是绝对不可能完成的！

他们是怎么做到的？

答案呼之欲出：NVIDIA Humanfia团队带来了大模型与自动化推理的“降维打击”。

英伟达不仅提供地表最强的算力，他们正在探索如何让AI直接辅助最前沿的基础科学研究。

虽然官方尚未公开所有AI生成的细节，但从短时间内暴增的代码量可以推断出这套“工业化”的证明流水线。

Chow、Liao、Qin等顶尖数学家负责绘制“战术地图”，将庞大的几何化猜想拆解为数以千计的引理和子目标。

NVIDIA团队利用LLM和自动化脚本，根据人类提供的上下文，疯狂生成海量的底层证明代码、补全繁琐的代数推演和边界条件穷举。

最后，所有的代码被送入Lean编译器进行无情的“逻辑质检”，不通过就打回重写，直到绿灯亮起。

这不仅是数学界的大事，更是AI进化史上的绝对焦点！

目前的大语言模型在复杂的长链条逻辑推理上依然存在“幻觉”，而解决大模型逻辑缺陷的终极武器，正是数学形式化。

如果AI能熟练生成Lean代码，去证明“瑟斯顿几何化猜想”这种人类智力巅峰的产物，那么距离AI自己“提出新猜想并给出证明”，真的只有一步之遥了。

为数学宇宙铺设高速公路，新纪元已然开启

Thurston几何化猜想的完整形式化，绝不仅仅是完成了一次高难度的“代码翻译”。它留给世界的，是一笔宝贵的数字财富。

通过GitHub上的differential-geometry项目，团队为全人类留下了一套经过“绝对真理验证”的微分几何代码库。

这意味着，以后全世界的数学家想在计算机里研究多维流形、黑洞的几何结构甚至时空演化时，直接调用他们写好的库就可以了！

这是前人栽树、后人乘凉的伟大工程。

从庞加莱在一百多年前写下那个著名的猜想，到瑟斯顿描绘出三维宇宙的宏大蓝图。

从佩雷尔曼在圣彼得堡的公寓里演算，到今天Ayush Khaitan、秦子洋、廖源、周培能等学者联合英伟达，用470万行代码让机器彻底“顿悟”……

人类对真理的追求，就像一场接力赛。

AI并没有抢走数学家的饭碗，而是给了他们一套探索宇宙的“星舰”。

人类破解难题的脚步，将爆发出前所未有的加速度。

参考资料： https://x.com/ayushkhaitan343/status/2108654050203840528?s=20 本文来自微信公众号“新智元”，作者：大卫 Aeneas，36氪经授权发布。