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

来源：平行智能

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 Erdős在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 辅助撰写，内容经人工审核后发布。

阅读最新前沿科技趋势报告，请访问21世纪关键技术研究院的“未来知识库”

未来知识库是 “21世纪关键技术研究院”建 立的在线知识库平台，收藏的资料范围包括人工智能、脑科学、互联网、超级智能，数智大脑、能源、军事、经济、人类风险等等领域的前沿进展与未来趋势。目前拥有超过8000篇重要资料。每周更新不少于100篇世界范围最新研究资料。 欢迎扫描二维码或访问https://wx.zsxq.com/group/454854145828进入。

截止到2月28日 ”未来知识库”精选的百部前沿科技趋势报告

（加入未来知识库，全部资料免费阅读和下载）