AI正在摧毁数学吗-工具替代还是辅助

数学这门学科,长期以来被认为是「人类纯粹理性最高形式」的堡垒。AI 在下棋、围棋、翻译、写作上一路推进,但数学——尤其是数学研究——始终被认为门槛很高。直到最近两年,AI 正在系统性改变这件事。

从 2024 年 DeepMind 的 AlphaProof 与 AlphaGeometry 2 达到 IMO 银牌,到 2025 年 Gemini Deep Think 达到金牌,再到 2025 年 5 月 AI 自主推翻一个研究近 80 年的 Erdős 几何猜想,以及最近 9 月公布的纳维-斯托克斯方程解答,AI 在数学领域的推进速度已经远超外界预期。

把过去两年的关键节点串起来,会发现 AI 介入数学的速度是一条明显的上坡曲线。

2024 年,AlphaProof 和 AlphaGeometry 2 在国际数学奥林匹克赛(IMO)上达到银牌水平。一年之后,Gemini Deep Think 已经在同一项赛事上达到金牌标准。

2025 年 5 月,AI 自主推翻了一个研究近 80 年的 Erdős 几何猜想。这个案例值得专门说一下——传统的几何猜想通常需要多年、多位数学家的反复验证;能在短时间内完成这一过程,意味着 AI 在「提出并验证新结论」这条路径上,已经有实质能力。

2025 年 8 月,一次性公布十项数学与理论计算机科学成果,其中包含解决或推进多个长期开放问题。

到了 9 月,纳维-斯托克斯方程——千禧年难题之一、悬赏 100 万美元、困扰数学界近一个世纪——进入了 AI 的射程。一支团队动用了大约一万个 AI 代理同时展开搜索,88 小时后找到关键解法,随后又用 17 小时完成 Lean 形式化验证。

纽约大学数学家把这一刻称为数学的「深蓝-卡斯帕罗夫时刻」。

从「证明稀缺」到「证明过剩」

数学的瓶颈正在被重新定义。

菲尔兹奖得主陶哲轩把数学研究拆成三个环节:生成(提出新证明)、验证(确认证明成立)、消化(把新证明纳入知识体系、解释其意义)。AI 让生成与形式化验证越来越快,但人类理解与纳入知识体系的速度跟不上。

换句话说,数学可能正从「证明稀缺」进入「证明过剩」。当 AI 可以短时间内生成大量可验证的证明,真正的稀缺资源反而变成了「谁能解释这些证明意味着什么」「谁能把它纳入人类的知识地图」。

Lean 这类形式化验证工具,能验证逻辑是否成立,却不能判断证明是否优美、是否揭示了新结构。这件事,目前还只能由人来完成。

「好问题」可能变成不可再生资源

AI 的速度可能逆转数学共同体几百年的开放传统。

过去的数学研究有一个不成文的默契:研究者在公开尚未成熟的方向时并不担心,因为好问题往往需要多年解决,公开讨论能吸引更多人一起推进。一个想法刚露头,往往要花几年才能走通。

但在 AI 时代,这种情况可能会变。如果一个想法刚公开,大公司就能立刻投入数千个代理把它「打穿」,最理性的个人选择可能变成保密。

陶哲轩公开警告过这种激励可能逆转几个世纪以来的开放科学传统。损失的不是某一个证明,而是新思想形成的生态。

数学研究可能变成算力比拼

更进一步,数学研究可能像量化交易一样,从人与人的智力比拼,变成组织、模型与计算资源的比拼。

量化交易发展到一定阶段,比拼的不再是交易员的聪明程度,而是算法、数据、算力和基础设施。未来一部分数学研究也可能出现类似结构:好的问题一旦公开,若证明空间可被大规模机器搜索,资源最充足的机构就有能力最快把它「打穿」。

9 月 11 日,陶哲轩与另外 24 位菲尔兹奖得主联合声明,公开警告 AI 公司以攻克著名难题来展示模型能力的做法,与数学共同体的目标存在「严重错位」。

这种声明,本身就是 AI 对数学冲击的实质性信号——数学共同体开始明确表态,担忧 AI 介入的方式改变了数学研究本身的性质。

真正值得追问的问题

把视角从数学家的「饭碗」转向更日常的问题,会得到一组更值得长期思考的命题。

导航让人失去城市空间感,计算器和搜索引擎改变了记忆与计算,生成式 AI 开始替人写信、读材料、做方案、编程和思考。每一次工具的升级,都顺手带走一点我们原本以为属于人类的能力。

陶哲轩有一个比喻:过去研究难题像徒步远行,一路留下路标与地图,AI 更像坐直升机直接降落在终点。科研的回报,很大一部分来自过程本身;若过程被压缩成几小时,人类可能第一次拥有大量自己并未经历「发现过程」的知识。

值得追问的不是「哪个学科 AI 攻不下来」,而是「哪些事情即使机器做得更快更好,我们仍希望自己去做」。

我看到的两个关键转变

仔细看这组进展,有两个关键转变值得标记。

第一个转变是「数学的瓶颈在移动」。过去是「想法稀缺,验证稀缺」;现在是「想法可以批量生成,验证可以批量完成,瓶颈移到解释、纳入、教学」。这道瓶颈的移动,会让数学教育的重点也跟着移动——死记硬背和技巧训练会更不重要,而「理解证明、解释证明、纳入框架」会更重要。

第二个转变是「数学的资源门槛在抬升」。过去,一个聪明的数学家凭一己之力可以推进一个方向;现在,资源充足的机构能用大规模机器搜索在短时间内打穿一个证明空间。这意味着数学研究的「公平性」可能在改变,资源会进一步集中到头部机构。

反面观点:不必过度解读

也有一些冷静的提醒。

第一,这些进展里的很多案例,距离「正式攻克」还有几个步骤。纳维-斯托克斯方程目前只是 OpenAI 给出的一个解答,还没有经过数学共同体的全面评议,严格来说还没被正式攻克。

第二,Lean 形式化验证工具只能验证逻辑是否成立,无法判断证明的「价值」——这一点目前是 AI 的硬伤,也是数学共同体的护城河。一个「有价值」的数学证明,必须能被纳入人类的知识体系,这件事目前还只能由人来完成。

第三,数学共同体的回应很关键。菲尔兹奖得主联合声明这类动作,本身就是数学共同体在主动调整边界——他们不是反对 AI,而是在呼吁 AI 介入的方式要与数学研究的目标对齐。

a5 关键素材

• • 2024 AlphaProof + AlphaGeometry 2 达到 IMO 银牌
• • 2025 Gemini Deep Think 达到 IMO 金牌
• • 2025 年 5 月 AI 自主推翻研究近 80 年的 Erdős 几何猜想
• • 2025 年 8 月一次性公布十项数学与理论计算机科学成果
• • 9 月纳维-斯托克斯方程由约 10000 个 AI 代理、88 小时搜索、17 小时 Lean 验证
• • 纽约大学数学家称之为数学的「深蓝-卡斯帕罗夫时刻」
• • 陶哲轩把数学研究拆成生成、验证、消化三环节
• • 数学正从「证明稀缺」进入「证明过剩」
• • 9 月 11 日 25 位菲尔兹奖得主联合声明警告 AI 公司解题比拼
• • 关键问题:哪些事即使机器做得更快更好,我们仍希望自己去做