过去，数学难题像一座座长在时间里的山。一个猜想在那里放上八十年，几代人从不同方向攀爬，某个天才偶尔找到一条新路。现在，山脚下忽然开来了一支机器施工队：数十个、数百个乃至上万个智能体同时搜索、互相传递线索，再让证明助手逐行检查。
短短几个月，新闻密得让数学家都来不及消化。AI不再只是拿奥数金牌，它开始伸手摘研究数学里那些多年无人拿下的果子。真正反常识的地方并不是机器会算，而是它似乎找到了把灵感工业化的办法。
一场突然加速的收割
2025年7月，Google DeepMind的Gemini Deep Think在国际数学奥林匹克竞赛中得到35分，达到金牌标准。那仍然是人类事先精心设计、有标准评分体系的竞赛题。一年之后，战线已经越过考场。2026年5月，OpenAI公布一项结果：内部模型推翻了围绕平面单位距离问题、延续近80年的一个主流猜想——方格类构型基本已经最优。这个问题最早由数学家保罗·埃尔德什在1946年提出，问的是平面上放置若干点时，能够形成多少对距离恰好为1的点。它的表述简单得像一道中学题，背后却压着数十年的组合几何研究。OpenAI称证明已经由外部数学家核查，菲尔兹奖得主Tim Gowers评价，如果作者是人类，他会毫不犹豫建议顶级期刊接收。
8月，Anthropic让Claude挑战黎曼猜想。它没有解决这个1859年提出、悬赏百万美元的难题，却意外推进了一个相关结果：把满足黎曼猜想条件的ζ函数零点比例下界，从41.6%提高到67.2%。Anthropic的两名数学家检查了结果，外部专家也做了审阅，并给出了可由Lean核验的形式化版本。这里必须踩住刹车：67.2%不是100%，更不是黎曼猜想已被攻克。它说明AI在一次失败的远征中，顺手开辟了一条此前没有的支路。9月，Claude又用了11天，把怀尔斯对费马大定理的证明转成了第一份端到端、可由计算机检查的Lean证明。它写下1300万行代码，完成数万个中间定理。费马大定理早在1995年就已得到人类证明，所以这不是AI重新解开费马大定理，而是机器完成了一项原本预计需要多年协作的形式化工程。它收割的不是定理本身，而是证明中那些人类习惯略去、机器却必须一格不漏补齐的逻辑细节。
更具冲击力的消息来自9月8日。OpenAI宣称，一个尚未公开的内部模型给出了纳维—斯托克斯千禧难题的解答：平滑流体也可能在有限时间内发展出奇点。公司披露，约一万个智能体并发工作，88小时形成结果，又用17小时完成Lean形式化。处理这一问题的智能体发送了270万条消息，消耗约1300亿输出token。这个结论仍要经过数学共同体的长期审查，不能仅凭公司公告就写进教科书。但这种组织方式已经足够惊人：过去只有少数顶尖数学家能够承受的搜索，现在被拆成了可并行、可复制、可追加算力的计算过程。
为什么偏偏是数学
数学为AI提供了一种其他领域很难拥有的东西：相对清晰的奖惩信号。
一篇小说好不好，没有一台机器能够给出绝对答案，一项社会政策是否有效，要等待真实世界运行多年，一个药物分子能否治病，还要经过实验、动物研究和临床试验。形式化数学不同。候选证明被写入Lean之后，证明助手能够逐步检查逻辑链条：成立就是成立，某一步类型不匹配就是不通过。DeepSeek-Prover的研究已经展示了这种路径，直接把Lean的核验反馈作为强化学习信号，让模型在一次次失败中调整证明策略。这形成了一个异常强劲的循环。模型生成候选思路，验证器筛掉错误，保留下来的轨迹回流训练。更多算力允许更多分支同时探索，更好的模型又能产生更有希望的分支。人类数学家、公开论文和数学数据库提供地形图，AI公司提供算力与组织系统，Lean一类证明助手充当不会疲倦的质检员。单个模型偶尔灵光一闪不是最可怕的变量，真正改变速度的是整条生产线开始闭环。
这也解释了为什么数学成绩不能直接推导出AI已经像人一样理解世界。形式化证明的边界极清楚，现实世界却充满目标冲突、隐含价值和无法穷尽的后果。一台机器能证明某个命题，不等于它知道这个命题为什么重要，能在给定规则内找到路径，也不等于它能替人类决定该往哪里走。把数学突破直接外推成全能智能，与把一次考试高分当成完整人格一样草率。
数学家真正焦虑的，不只是失业
最近，一张据称来自2026年菲尔兹奖得主邓煜的朋友圈截图被广泛转发。由于目前能够查到的是二手转载，不能把它当成正式采访逐字背书。截图中的态度却很值得讨论，数学界弥漫着浮躁不安，但AI迭代的时间尺度远短于人类社会，不妨等这一波前沿过去，看清新的生态。他好奇AI能否从回答偏微分方程的存在性，一路走到奇点的测度、维数、拓扑性质乃至完全分类，如果AGI真能解决这一整棵问题树，自己见证神迹之后，大不了回家写百合小说。这句玩笑里的松弛，恰好点出了做题和做数学的区别。题目已经被写在纸上时，任务是寻找答案，数学家更稀缺的能力，是从模糊现象里看见一个值得问的问题，创造定义，判断哪条道路会长出新的理论。AI现在疯狂采摘的，是人类已经挂上标签的果实。它什么时候能够自己选择土地、培育新品种，仍是另一道没有标准答案的问题。
陶哲轩等25位菲尔兹奖得主在9月11日发表的公开声明，把担忧说得更尖锐。他们承认大模型的数学能力已显著提高，却认为AI公司把著名难题当成能力基准，与数学共同体追求概念理解和洞见的目标严重错位。一个猜想在数学史上的价值，不只在最终被标记为真或假，还在求解过程中长出的概念、方法、讨论和学生。若机器高速批量生产结论，人类来不及整理方法、确认归属、把结果写进可以传承的知识体系，证明过剩反而可能制造理解稀缺。这里还有一个不容易被看见的阶层变化。过去，年轻数学家可以靠解决一个好问题进入共同体，未来，最强模型和最大算力掌握在少数公司手中，开放问题可能先被当作产品演示的矿区。学术声望、研究机会和解释权会不会随算力一起集中？当机器几天内给出一份长到无人能读完、却能通过形式核验的证明，谁来获得署名，谁承担审稿劳动，谁有资格决定它是否值得进入数学史？这已经不是单纯的技术竞赛，而是知识生产制度在重新分配权力。
从“数学神迹”跳到“人类末日”，中间还隔着什么
就在数学突破密集出现的同一周，前OpenAI、Anthropic研究员Jacob Coxon宣布辞职。他指责两家公司竞相奔向能够自我改进的超级智能，是在拿我们的生命赌博，并称业内一些开发者真诚地担心AI可能在本十年结束前威胁所有人。Anthropic对齐研究负责人Evan Hubinger随后给出的个人估计，是未来十年发生这类灾难的概率超过10%。TechCrunch对两人言论的报道媒体很容易把它压缩成一句“AI工程师说AI会杀死人类”。更准确的表达是，AI研究人员对未来风险给出了高度不确定、无法用频率统计验证的主观概率，并警告能力竞争正在快于安全治理。这不是预言，也不是数学突破自动推出的结论。会证明定理的系统与能够长期自主规划、入侵现实基础设施、获取资源并抵抗关停的系统之间，还隔着一长串能力条件。
数学新闻真正提供的证据只有一条，却已经足够重要：我们曾经低估过能力跨越发生的速度，也低估了“模型＋工具＋海量并行智能体”这种组织形式。纳维—斯托克斯方程不会因为AI算得更快就伤害人类。危险来自另一个反馈环，公司竞争带来更大投入，突破带来更多资本和政策支持，更强模型又加速下一轮竞争，而安全验证、学术规范和公共治理只能以人的速度追赶。邓煜选择用玩笑对抗焦虑，Coxon选择离开实验室发出警告，25位菲尔兹奖得主选择联合声明。三种反应看似相反，其实都在追问同一件事：当答案的生产速度超过人类理解、吸收和治理的速度，我们究竟该用什么来定义进步？
数学也许是最早显露这道裂缝的领域，因为它能给机器一个干净的判分器。可人类社会没有Lean，没有一个按钮能验证更强的智能是否带来更好的文明。如果有一天，难题真的不再稀缺，我们最需要保护的，恐怕不是人类比机器多会做几道题的尊严，而是提出问题、解释意义并决定把力量用向何处的权利。
- Google DeepMind，2025年IMO金牌水平报告。
- OpenAI，平面单位距离猜想、纳维—斯托克斯问题原始公告。
- Anthropic，黎曼ζ函数相关进展、费马大定理形式化报告。
- Xin等，DeepSeek-Prover-V1.5，ICLR 2025。
- 陶哲轩等25位菲尔兹奖得主，《A Severe Misalignment of AI in Mathematics》。
- 美联社，Jacob Coxon辞职与AI风险警告报道。