丘成桐弟子团队携手 NVIDIA，完成瑟斯顿几何化猜想 Lean 形式化验证

近日，由斯坦福大学学者 Ayush Khaitan 带领的顶尖学术团队联合 NVIDIA Humanfia 团队，成功完成了 Thurston 几何化猜想的完整 Lean 形式化验证。这一成就标志着 AI 辅助数学研究正式深入高阶几何分析的深层领域。该项目总代码量达 470 万行，其中新增的 270 万行代码由团队在约两周时间内编写完成。相比之下，证明核心人物之一 Bennett Chow（周培能）此前已完成约 200 万行的基础工作，而 AI 与自动化推理技术在短时间内完成了巨大的编码增量。项目团队成员包括加州大学圣地亚哥分校教授 Bennett Chow、普林斯顿学者 Ayush Khaitan 以及 NVIDIA 工程师 Jui-Hui Chung 和 Ligeng Zhu。斯坦福数学助理教授 Jared Duker Lichtman 对该成果给予了高度评价，认为这是将庞加莱猜想证明推广至完整几何化猜想的惊叹之作。Thurston 几何化猜想被视为比庞加莱猜想更为宏大的蓝图，旨在将任意三维流形分割为属于八种标准几何结构之一的部分。佩雷尔曼曾通过 Ricci 流与手术理论在 2003 年证明该猜想并间接解决了庞加莱猜想，此次验证则是将该理论的整个逻辑链条形式化地嵌入计算机系统。团队在 GitHub 上开源了名为 differential-geometry 的代码库，地址为 https://github.com/qinz1yang/differential-geometry。该项目重构了黎曼几何基础，定义了流形、切丛、张量场及黎曼度量等复杂概念，并将 Ricci 流方程与手术理论转化为可被 Lean 编译器验证的逻辑树。此次合作展示了 AI 在长链条逻辑推理中的潜力，通过大模型生成底层证明代码并经由 Lean 进行严格质检，实现了从人类绘制战术地图到机器执行繁琐代数推演的工业化流水线。这不仅是数学界的里程碑，也为 AI 未来自主提出并证明新猜想奠定了技术基础。目前，所有成果已全面开源，标志着数学形式化验证迈入新时代。这一项目证明了 AI 在微分几何、拓扑学和偏微分方程等人类智力巅峰领域的处理能力正在飞速发展，为探索宇宙三维结构提供了全新的数字工具与视角。