《纽约时报》万字长文：两年与五天，一份被 AI 截胡的数学证明

luyuanhong

《纽约时报》万字长文：两年与五天，一份被 AI 截胡的数学证明

原创  悟尔新（PURE） 平行智能  2026 年 6 月 9 日 23:37  广东

2024 年，年轻的数学家 Sidharth Hariharan 在洛桑见到了菲尔兹奖得主 Maryna Viazovska 。两人随后启动了一个极具野心的项目：将 Viazovska 在 2016 年证明的“8 维球体填充定理”，用 Lean 定理证明器完整地形式化。

所谓“形式化”，简而言之，就是把数学论文中的每一个推理步骤，翻译成计算机可以逐行验证的逻辑代码。这是一项极其耗费心血的工程——论文中看似简短的一行推理，往往需要后台写出几百行代码来填补逻辑跳跃。

Hariharan 的团队花了整整两年时间搭建框架、撰写蓝图、定义新概念。直到 2025 年底，他们估计还需要至少六个月才能攻克 8 维的情况。

然而，加州初创公司 Math , Inc. 带着其开发的 AI 形式化工具—— Gauss ，毫无征兆地介入了。

Gauss 仅用 5 天时间，就自动完成了 8 维证明剩余的所有内容。紧接着，它又用时两周，直接从 Viazovska 的原始论文出发，自动形式化了更复杂的 24 维情况，最终产出了超过 20 万行代码。

Hariharan 的团队被彻底抢跑了。尽管他们是该项目的主要贡献者——搭建了蓝图框架、定义了球体填充和模形式在 Lean 中的基础概念，为整个项目铺平了道路。但 Gauss 确实用降维打击的速度，在人类打好的地基上疯狂收割。

两年前项目启动时，还没有人预料到 AI 能以这种方式介入。这就是 6 月 8 日《纽约时报》长篇报道的核心故事。但记者 Gregory Barber 真正想追问的，是一个更为沉重的问题。



AI 在数学领域的进化速度正在超出所有人的想象。

2025 年，AI 在国际数学奥林匹克（IMO）上斩获金牌。就在五月底，OpenAI 宣布一个通用推理模型解决了“平面单位距离问题”——这是由 Paul Erdos 在 1946 年提出、困扰了数学界近 80 年的著名开放问题。菲尔兹奖得主 Tim Gowers 对此惊叹：“这是 AI 数学的里程碑。”

面对技术海啸，学术界开始筑起防波堤。6 月 2 日，由 16 位数学家起草、国际数学联盟背书的《莱顿宣言》正式发布。宣言严肃警告： AI 正在威胁数学的核心价值，包括证明的可靠性、作者归属、透明性以及学者的自主判断。

菲尔兹奖得主 Peter Scholze 在签署宣言时的发言掷地有声：“数学研究的目标是人类对数学的理解。数学只能在一个由人类数学家组成的共同体中繁荣。就像我不希望我的孩子被 AI 教育一样，我思考数学时不使用 AI ，也尽量不读 AI 生成的文本。”

但真正让整个数学界感到彻骨寒意的，并不是 AI 攻克了顶级难题。这类菲尔兹奖级别的璀璨成果终究是罕见的。

真正让年轻数学家彻夜难眠的，是 AI 正在迅速吞噬那些“中间地带”的项目。

在传统的学术界，年轻研究者的职业路径清晰可见：花两到五年时间攻克一个具体的开放问题，凭借这篇论文在细分领域内建立学术声誉，进而获得教职。

形式化项目同样遵循这一逻辑。将一个已知定理完整形式化，需要研究者深刻理解其全部细节并翻译成计算机语言。这极度考验耐心、细致与深度理解力，恰好是年轻学者向招聘委员会展示自身学术潜力的最佳舞台。

现在， AI 可以用几天时间完成原本需要耗费数年的工作。

如果一个博士三年级的学生，正准备投入两年青春去形式化某个重要定理，他不得不面对一个残酷的现实：走到一半时，某个 AI 工具可能已经敲完了最后一行代码。

更直接的威胁来自现实的学术评价体系。如果资助机构和招聘委员会开始认为“形式化是 AI 可以批量生产的产物”，那么这类项目在评估体系中的价值就会瞬间归零。年轻数学家将失去一块至关重要的训练场。

这绝非危言耸听。Math , Inc. 的一名员工透露，公司在球体填充项目上投入了超过 10 万美元的计算成本。对不差钱的 AI 巨头而言这只是九牛一毛，但对个人研究者来说，这可能是整个博士生涯都无法企及的资源。



面对被抢跑的结局，Hariharan 本人展现出了超乎寻常的平静：“ AI 是颠覆性的。”如今，他的团队正在反向使用 AI 工具来优化 Math , Inc. 生成的代码，使其更具可读性与可维护性。

在他看来，人类与 AI 的关系目前并非简单的“取代”，而是 AI 正在重新定义“什么叫数学家的产出”。

过去，学者的产出是“我独立证明了一个定理”；未来的产出则可能是“我设计了一个原创框架，AI 在框架内完成细节填充，而我负责验证、组织和解释结果”。

类似的范式转移已经在药物研发领域上演：AI 批量提出候选分子，人类科学家则凭借直觉与经验，判断哪些分子值得投入临床试验。判断力、品味以及对问题意义的评估，依然是人类独有的领地。

然而，不可忽视的痛点在于：当一个年轻数学家花了两年时间搭建框架、训练自己、建立直觉，AI 却抢在终点前摘走了果实。这失去的不仅是时间，更是一块通往未来的职业阶梯。

这块阶梯断裂之后，下一个台阶究竟在哪里？目前，整个学术界依然给不出答案。



本文由  AI  辅助撰写，内容经人工审核后发布。

平行智能

重生888@

所谓“声明”，是既得利益者，想保住其霸权地位！只有顺应时代，让人与机器相互作用，推动数学事业的高质量发展！