数学这颗明珠被击穿了——但计算机证明本来就不是新鲜事

数学一直是人类智慧的最后堡垒。下棋？机器1997年就赢了。画图？2022年就行。写代码？去年就比你快了。但研究数学——那种需要洞察力、需要美的、需要跨越领域寻找到没人想到的连接的数学——一直是人独有的地盘。

现在这个地盘也被踩进来了。OpenAI的一个通用推理模型推翻了Erdős在1946年提出的单位距离猜想，一个挂了80年的开放问题¹。Fields奖得主Tim Gowers说”毫不犹豫推荐Annals of Mathematics接收”²。这回不是假的——去年11月Kevin Weil吹的”解决了10个Erdős问题”后来被证实只是重新发现已有文献，维护Erdős问题网站的Thomas Bloom直接说是”严重误导”³；这回Bloom自己联名写了配套论文²。

但这件事的意义不是”又一个领域被AI拿下了”这么简单。因为计算机证明，本来就不是新鲜事。

计算机证明50年前就有了

1976年，Appel和Haken用计算机证明了四色定理——任何地图只需要四种颜色就能让相邻区域不撞色⁴。整个数学界震了一下：证明用了计算机穷举了上千种情况，人根本没办法一行一行验证。

后来很多人不舒服。有人说这不算”真正的证明”，因为你没有办法读懂它。有人说机器只是做了人让它做的事，没有真正的数学洞察。

他们说得对——但四色定理至今没有被”纯人”证明出来。而过去50年，数学界已经接受了：计算机可以成为证明工具。Coq、Lean、Isabelle这些证明助手早就嵌入了数学工作流⁵。2026年1月以来，AI已经把15个Erdős问题从”未解”变成”已解”⁶。

所以问题从来不是”机器能不能证明数学”。机器早就能够证明了。

问题是：机器是帮你计算，还是替你思考？

这次不一样的部分

Erdős的单位距离问题很简单：平面上n个点，最多有几对点距离恰好是1？¹

人一直觉得答案是n的一点点倍——差不多就是线性增长。正方形网格给出2n对，Erdős自己的构造稍微好一点（n^(1+C/log log n)），但也就好那么一丁点¹。1984年Spencer、Szemerédi和Trotter给出了上界O(n^(4/3))⁷，42年没有人动过。

所有人都觉得线性增长差不多是对的。Erdős自己猜的也是u(n) ≤ n^(1+o(1))⁴。

表1：挂了80年 ¹⁷

年份	结果	谁
1946	最好的下界：n^(1+C/log log n)	Erdős本人
1984	最好的上界：O(n^(4/3))	Spencer, Szemerédi, Trotter
2026	推翻：u(n) ≥ n^(1+δ)，δ=0.014	OpenAI模型 + Will Sawin改进

模型是怎么做的？它去寻找了反例。

这听起来不值一提，但想想之前攻过这个问题的数学家都是怎么做的——他们试图证明猜想是对的。而模型的思维链（Chain of Thought）显示，它把大部分算力花在构造反例上²。它没被”大家都觉得这应该是对的”困住。它不知道这个社交共识，所以它尝试了人类集体排除的方向。

Gowers看到了这一点：“大部分思考在尝试构造反例，而不是试图证明。这说明模型有某种直觉，愿意尝试被社区视为长枪的路线。”²

这就是”vibe数学”——跟LLM来回对话、迭代地发展定理⁵。不是你给它一个命题它给你一个证明。是它来回来去尝试，试到寻找到路径为止。

代数数论从后门走进来

然后是真正让人意外的部分。

模型没有在组合几何里打转。它跳到了一个看起来完全不相干的领域——代数数论。它把Erdős用的Gaussian整数（a + bi）换成了更复杂的代数数域，用上了无限类域塔和Golod-Shafarevich理论¹²。

这些东西在代数数论里是基本功。但从没有人想过拿它们去解决平面点集的问题。

表2：人和AI看了不同的门 ¹²

	人	AI
在哪个领域搜索	组合几何	代数数论
用什么工具	组合论证	类域塔、Golod-Shafarevich
策略	证明猜想	构造反例
结果	没证明出来	n^(1+0.014)

普林斯顿的Will Sawin把δ明确到了0.014²。0.014看起来很小。但它不是”比线性快一点”——它是”有一个固定的指数优势”。在渐近分析里，这俩是本质区别。

Alon的评价直截了当：“AI做到的是大量优秀的研究者尝试过但没能做到的事。”²

Bloom写得更远：“AI正在帮助我们更充分地探索几个世纪以来建立的数学大教堂；还有什么未见过的奇观在等待着我们发现？”¹

但Gowers泼了冷水——也是实在话。

证明了，但不是那种证法

Gowers把这件事跟2005年Guth和Katz解决Erdős距离问题做了对比。Guth和Katz的证明引入了全新的工具——多项式切条法——打开了一整个方向，后来解决了好几个相关问题。

这次的构造没有做到这一点。它是从数论拉过来一座桥，但不是一种新的几何理论。它”没有引入强大的新几何工具，也没有揭示结构性的洞察”²。

Gowers的判断：反例靠搜索有可能寻找到，正面证明需要真正的理论构建。所以”也许我们现在看到的不是AI要超越人类数学家，而是某些问题类型上AI有明显优势——它有百科全书式知识，不用担心时间管理，能够负担尝试看来不太可能成立的事情”²。

这话其实是在说：AI擅长搜索，不擅长构建。

这跟”计算机证明”的历史一脉相承。1976年四色定理的证明就是搜索——穷举了上千种构形。只是这次搜索的不是构形的数量，而是跨领域的连接。

没有被Lean验证

一个值得注意的细节：这个证明没有被形式化验证。没有Lean，没有Coq，就是9个顶级数学家读了、确认了²。

四色定理后来被Coq形式化了（2005年，Georges Gonthier）。Erdős问题的很多AI解决方案也在Lean里被验证过⁵。但这次的证明是自然语言写的，人一个字一个字看的。

这到底算不算”计算机证明”？要看你定义的边界在哪。如果是”机器输出的东西人确认了”，那四色定理1976年就是计算机证明。如果是”机器在形式化系统里独立完成了从命题到QED的全链路”，那这次还不算。

但这次的证明做了一件四色定理没做的事：它寻找到了人类没有找到的路径。 四色定理是人想出策略、机器执行。这次是机器自己摸到了代数数论那扇门。

参考来源

结语

数学是人类智慧最后一块没有被机器碰过的硬骨头。现在被碰了。但回头看看——1976年四色定理就是计算机证明，Coq和Lean早就嵌在教学和科研里了。计算机证明不是新鲜事，AI解决Erdős问题也不是今天才开始的。

这次真正不同的地方：以前的计算机是帮你计算，这次是替你思考。模型寻找到了从代数数论到离散几何的那扇门——人没有找到，不是因为它太困难，是因为人被”大家都这么想”困住了。

但Gowers说了一句实在话：反例靠搜索可能寻找到，真正的理论构建搜索不来。它寻找到的是反例，不是新理论。

接下来几个月会有很多代数数论学者翻看离散几何里其他开放问题²。如果那扇门后面站着的是更多反例——好，那AI就是更快的搜索工具。如果门后面站着的是Guth和Katz式的新理论——那就真的不一样了。

Footnotes

1. OpenAI官方博客 — An OpenAI model has disproved a central conjecture in discrete geometry https://openai.com/index/model-disproves-discrete-geometry-conjecture/ ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷

2. Alon, Bloom, Gowers, Litt, Sawin, Shankar, Tsimerman, Wang, Wood — 配套论文 — 人可读版证明和专家评述 https://arxiv.org/abs/2605.20695 ↩ ↩² ↩³ ↩⁴ ↩⁵ ↩⁶ ↩⁷ ↩⁸ ↩⁹ ↩¹⁰ ↩¹¹ ↩¹²

3. TechCrunch — “这次是真的” — Kevin Weil之前的虚假声明和这次的真实验证 https://techcrunch.com/2026/05/20/openai-claims-it-solved-an-80-year-old-math-problem-for-real-this-time/ ↩

4. Gil Kalai — “Erdős单位距离问题被推翻！” — 把这次跟1976年四色定理对比 https://gilkalai.wordpress.com/2026/05/21/amazing-erdos-unit-distance-problem-was-disproved-it-was-achieved-by-ai/ ↩ ↩²

5. arXiv 2602.18918 — “Vibe-proving”：跟LLM来回对话发展定理 https://arxiv.org/abs/2602.18918 ↩ ↩² ↩³

6. CryptoBriefing — 2026年1月以来15个Erdős问题被解决，11个归功于AI https://cryptobriefing.com/openai-ai-solves-erdos-math-conjecture/ ↩

7. Spencer, Szemerédi, Trotter (1984) — 上界O(n^(4/3))，42年没有人动过 引用于配套论文 ↩ ↩²