AI正在疯狂收割数学难题！黎曼猜想、孪生素数、哥德巴赫猜想……这次轮到数学家丢饭碗了

图片仅作示意

撰文｜王昱

审校｜陶兆巍、子鱼

2026年7月23日，邓煜、约翰·帕顿（John Pardon）、雅各布·齐默曼（Jacob Tsimerman）和王虹获得2026年菲尔兹奖。这个原本曲高和寡的数学奖项，因为邓煜和王虹获得了大量关注。

但除此之外，这届菲尔兹奖还有一项值得注意的线索。刚刚获得数学最高荣誉的雅各布·齐默曼却公开说：“我认为两年之内，AI做数学会比数学家更好。”并且在获奖当天宣布将加入OpenAI。

网上很快就流传起了一种判断，这届菲尔兹奖，也许是最后一届获奖成果主要依靠人类完成的菲尔兹奖。这当然只是对未来的猜测。菲尔兹奖每四年颁发一次，但最近的进展，似乎正在告诉我们，也许根本不需要等那么久。

数学收割机

过去几年，新闻中AI的数学能力一直在稳步前进，从AI在高考数学上取得了怎样的成绩，AI如何完成几何证明题，大学生用AI作弊数学作业，一直到AI达到国际数学奥赛金牌水准。

直到最近一两个月，AI似乎终于真正触达了人类的能力边界，和AI一起出现的数学名词也带上了历史的厚重感。

费马大定理、黎曼猜想、孪生素数猜想、哥德巴赫猜想……

AI在这些著名数学命题及其相关问题上取得了不同类型的进展：有的是发现新结果，有的是把人类早已完成的证明变成机器可以核验的形式。随着新一代Claude和GPT模型接连公布成果，数学研究的节奏也在加快。

8月10日，Anthropic公布了一项由尚未发布的研究版Claude发现的结果：一名员工原本想让Claude证明黎曼猜想。Claude没能完成证明，但据Anthropic公布的结果，它把已知能够证明位于临界线上的黎曼ζ函数非平凡零点的渐近比例下界，从约41.6%提高到67.2%。Claude同时还给出了Lean形式化（formalization）证明。

9月初，OpenAI公开了GPT-6 Astra在有界素数间隔问题上的新成果。这个问题与孪生素数猜想密切相关。孪生素数猜想认为存在无穷多对相差2的素数。2013年，张益唐证明存在无穷多对间隔小于7000万的素数；此后上界降到246，今年8月31日又被Julia Stadlmann改进为240。OpenAI的新论文则给出186的界限，即存在无穷多对间隔不超过186的相邻素数。这仍未解决要求间隔为2的孪生素数猜想。北大数学学院2007级校友、宾大教授苏炜杰随后介绍了这项工作。相关论文和Lean代码已公开。但代码仓库明确说明，形式化部分仍依赖三个尚未在Lean中证明的外部输入假设，不能据此称整份证明已经完成机器核验。

OpenAI关于有界素数间隔的新论文。图片来源：OpenAI

9月4日，Anthropic宣布，Claude在约11天内大体自主地用Lean完成了费马大定理的首个完整计算机核验证明。17世纪，数学家费马曾在书的页边写下：“我发现了一个绝妙的证明，但这个页边太窄，写不下。”让这个命题成为了数学史上最著名的一个“坑”。直到20世纪90年代，安德鲁·怀尔斯等数学家才完整证明了费马大定理。这一次，Claude沿着已有的人类证明路线，完成了此前尚未完成的完整形式化。

在大公司之外，也有人在推进形式化工作。9月5日，知乎用户子鱼在一篇文章中表示，自己使用GPT-5.6/6搭配Hermes Agent完成了部分解决哥德巴赫猜想的陈景润定理，即通常所说的“1+2”的形式化，并认为这“大概率是历史上第一个1+2的形式化证明”。在此基础上，子鱼正在进一步形式化今年六月份的一篇将陈景润定理推进到“1+1.9”的文章，并表示“这将会验证哥德巴赫猜想六十年以来的最重要突破。”

这只是最近1个月的进展，实际上，从今年5月开始，AI在数学上的突破就层出不穷，Erdős单位距离猜想、构造非sofic群、大素数间隔问题……类似的例子根本列不完。

自动化验证

在这些进展中，“形式化”和“Lean”这两个词反复出现，它们是核验AI数学成果的重要工具。

大语言模型（LLM）可能产生幻觉，给出看似可信、实际上错误的信息。它会根据上下文预测后续token，但这种生成机制本身不保证逻辑正确性。AI可以自动输出各种“奇思妙想”，但这些“奇思妙想”究竟是否值得相信，仍需要独立验证。

AI编程就是一个很好的例子。LLM会输出“看起来还不错”的代码，但LLM本身并不能保证代码的正确性。编译器可以检查语法、类型等错误，测试和运行反馈还能帮助发现部分逻辑问题。许多检查可以由计算机自动完成，让AI能够反复修改代码，这为AI编程提供了快速试错的条件。

而Lean，就是属于数学的“编程语言”。2013年，Leonardo de Moura在微软研究院启动Lean项目，2014年发布第一个正式公开版本。它既是一门函数式编程语言，也是一个交互式定理证明器。Lean语言能把普通数学论文中的定义、公理、引理、每一步逻辑推导、定理都变成机器能读懂的对象。而把用人类语言写下的数学，改写成计算机可以逐条理解、逐步检查的过程，就被称为形式化。

图片来源：Lean

数学定理被形式化后，AI数学就突然变得和AI编程非常类似。

数学研究的一大限制，是专家能用于理解和核查复杂证明的精力有限。今天的数学已经发展得非常深入，一篇涉及重大突破的论文，即使对相关领域的专家也可能很难读。如果证明被完整形式化，逐步检查逻辑推导的工作就可以

交给计算机。但人类仍需确认：形式化的命题是否准确表达了原问题，证明有没有依赖额外的未经证明的假设，以及结果究竟有什么数学意义。

OpenAI、Anthropic等前沿AI公司以及许多独立的数学工作者正在探索“AI提出证明—机器验证—自动修正”的工作流程，批量制造数学突破。大模型开始与Lean等形式化证明系统结合，给数学研究带来了一场名副其实的范式转变。

人类的数学？

作为人类智慧的顶点，数学家自己当然察觉到了这样的趋势。比如顶级数学家陶哲轩，他对AI的评价一直在变化。

2024年，他评价AI像一个“平庸但不完全无能的研究生”。

2026年3月，他表示AI已经“ready for primetime”，在实际数学研究里，开始“节省的时间多于浪费的时间”。他会让AI查文献、写代码、试计算、筛掉失败方向。

与此同时，他也在提醒：如果只追求解出题目，人类可能失去研究过程中更有价值的东西。

最近，陶哲轩在知识媒体Big Think的访谈中，把数学研究比作一次徒步旅行：研究者为了寻找远处的瀑布，需要不断探路、迷路、画地图，途中还可能发现新的景观；而AI则像一架直升机，可以直接把人送到瀑布旁，再把人接回来。这样当然更快，但人类也可能因此不知道如何抵达那里，更不会注意到沿途那些意外的发现。而后面这两点，反而才更可能是数学研究本身的意义。

目的地只是这段旅程价值的一部分。一路发现的那些工具、概念、技巧、失败原因，往往才成为下一代数学的基础。

9月3日，陶哲轩在Mathstodon发了一组长帖。他拿长期悬而未决的三维不可压缩纳维–斯托克斯方程的整体正则性问题（Navier–Stokes问题，也叫N-S问题）举例，设想了这样一种情形：一个拥有巨大算力的AI系统在内部反复尝试，最终解决这个问题，并给出机器可以核验的证明。

图片来源：Mathstodon

问题在于，如果整个探索过程都留在AI公司的内部，人类最后只看到那个最终答案，那么数学上最有价值的部分——哪些路线失败了、为什么失败、由此暴露出了什么新的流体结构——可能全部丢失。在这种极端情况下，技术上一个著名开放问题被解决了，但“几乎没有给数学增加相应的价值”。

可怕的是，陶哲轩只是用纳维–斯托克斯问题举例，网上很快就开始流传“陶哲轩是不是已经看过Claude解决纳维–斯托克斯的证明”。陶哲轩9月5日专门澄清，这只是一个假设性场景，他不知道纳维–斯托克斯目前有任何重大新进展。但这也说明，就算AI攻克了纳维–斯托克斯问题，大家也不会感到十分意外。

过去，人们曾用“爱因斯坦测试”来想象AI真正成为科学家的门槛：只给AI爱因斯坦在20世纪初能够获得的信息，看看它能否在不知道答案的情况下，独立提出广义相对论。Google DeepMind的Demis Hassabis在访谈中也用过这样的思想实验，来讨论AI是否具备开创性的科学创造力。它并不是一项已经建立的标准化测试，而是提出了一个更高的要求：AI不仅要会回答已有的问题，还要完成前人从未完成过的智力跃迁。

然而到了2026年，这个曾经显得颇为遥远的设想，似乎已经露出了现实的轮廓。AI当然还没有成为下一个爱因斯坦，但至少在数学领域，它已经不只是复述、计算和证明人类给出的结论，而是开始独立发现反例、改进数学界保持多年的纪录，甚至在尝试一个未解猜想失败时，顺手带回一个此前未知的新结果。我们过去用“AI能不能作出真正的科学发现”衡量未来；现在，这个问题正在一点点变成现实。现实的进步，似乎比我们的预想还要更快一些。