计算机解决的难题：机器帮助攻克的著名数学问题（1976–2026）

1976年，伊利诺伊州的两位数学家宣布，他们证明了任何地图都只需四种颜色就能着色，而证明的一部分只能由计算机来检验。许多数学家深感不安：如果没有人能把它从头读到尾，这还算是证明吗？五十年后，问题反转了。2026年，AI系统找到了专家们几十年都没能找到的关键思路。本文按时间顺序讲述这段历史，并对每个著名问题准确说明机器到底做了什么，因为“由计算机解决”可能意味着完全不同的事情。

学生常常混淆的区别

计算机在证明中扮演的三种截然不同的角色

检验情形：由人把问题化归为一张很长但有限的清单，再由计算机逐项检验（四色定理、开普勒猜想）。
搜索证明：计算机自己找到论证（罗宾斯猜想，以及2026年的AI成果）。
验证证明：像Coq或Lean这样的证明助手，逐步确认一个证明的每一个逻辑步骤，无论证明是谁写的。

1976年：四种颜色，和一个没人能读完的证明

GCSE核心

这个问题简单到小学生都能懂：给地图着色，让相邻的国家颜色永远不同。最多可能需要几种颜色？弗朗西斯·格思里在1852年猜测是四种。很容易看出可能需要四种（见下图），但要证明四种颜色对任何可能的地图都“永远”够用，难倒了数学家整整124年。

图示：为什么可能需要四种颜色

由五个区域围成的环需要三种颜色；与这五个区域都相邻的中心需要第四种。难点在于证明没有任何地图会需要第五种。

肯尼斯·阿佩尔和沃尔夫冈·哈肯找到了一种方法，证明任何需要五种颜色的地图都必然包含将近两千种特殊构形之一，而且每一种构形都可以被“约化”掉。全部手工检验是不可能的，于是由计算机完成，用了一千多个小时的机时。定理被证明了，但这种方式改变了“证明”在实践中的含义。

疑虑是如何消除的：1996年出现了一个更短的计算机证明；2005年，乔治·贡蒂埃和本雅明·韦尔内在证明助手Coq中验证了整个论证。如今它是数学中验证最彻底的定理之一。

1996年：第一个由计算机自己找到的证明

本科拓展

罗宾斯猜想问的是：三条简短的规则，描述的是否与布尔代数——每块计算机芯片里的真/假逻辑——完全相同的代数？包括阿尔弗雷德·塔斯基在内的顶尖逻辑学家，六十年都没能解决它。1996年，威廉·麦丘恩的自动定理证明器EQP在大约八天里搜索各种可能的推理链，找到了一个证明。这与1976年有本质不同：没有人告诉计算机论证应该是什么样子。

1998–2014年：开普勒的橙子

1611年，约翰内斯·开普勒断言，水果商堆橙子的方式（每一层都放在下一层的凹处）是等大球体最密的堆积方式。它填满约74%的空间（精确地说是π/√18）。

图示：水果摊上的堆法

这种排列的密度：π / √18 ≈ 空间的74.05%

大家熟悉的金字塔式堆法。证明没有更巧妙的排列能做得更好，花了将近400年。

托马斯·黑尔斯与塞缪尔·弗格森一起，把这个问题转化为数千个优化问题，用计算机求解，并在1998年宣布证明。期刊审稿人说他们“有99%的把握”它是对的，却无法检查每一步计算。黑尔斯随后领导了Flyspeck项目，在证明助手软件中把一切重新验证一遍；项目于2014年完成。

2016年：200TB的证明

GCSE核心

这里有一个可以自己动手的谜题。把每个整数涂成红色或蓝色。你能做到让任何一组勾股数（满足 a² + b² = c² 的三个数，比如3、4、5）都不是同一种颜色吗？

动手试试：给1到40着色，不出现同色的勾股数组

点一个数，让它在蓝色和红色之间切换。目标：任何满足 a² + b² = c² 的三数组（如3、4、5）都不能是同一种颜色。冲突三数组中的数会带上深色外圈。

16个同色三数组：3–4–5, 5–12–13, 6–8–10, 7–24–25…

试试1到40。可以做到，而且一直到7,824都可以。

罗纳德·格雷厄姆曾悬赏100美元求解。2016年，马里恩·赫勒、奥利弗·库尔曼和维克多·马雷克在超级计算机Stampede上运行“SAT求解器”（一种解决庞大真/假逻辑谜题的软件）约两天。答案是：1到7,824的每个数都能安全着色，但1到7,825不行。证明“7,825个数的任何着色都行不通”的证明文件大小为200TB，《自然》杂志当时称之为史上最大的数学证明。同样的技术在2019年解决了凯勒猜想在七维空间中用立方体铺满空间的情形。

快速检测

布尔勾股数组问题的答案是7,825。这个数是什么意思？

2025–2026年：AI开始找到思路

研究生拓展

上面的一切，都是用计算机来检验，或在人设计的框架内搜索。从2025年起，基于大语言模型的系统开始自己提出数学思路，并与证明助手Lean结合，使结果可以由机器检验，而不只是被相信。

单位距离猜想（2026年5月）。1946年，保罗·埃尔德什问：在平面上放n个点，最多能有多少对点的距离恰好为1？他认为答案只比n增长得快一点点。OpenAI的一个内部模型利用代数数论的深刻工具，找到了一族无穷多的点集，比这个上限多出一个真正的n的幂次。包括菲尔兹奖得主蒂莫西·高尔斯和雅各布·齐默曼在内的九位顶尖数学家检验了它，并撰写了配套论文，威尔·索温则把增益明确地写了出来。吉尔·卡莱把它的重要性比作1976年的四色定理证明。

图示：数一数单位距离

19个点，42对距离恰好为1

像这样的格点图案会产生很多距离为1的点对。埃尔德什认为不可能做得好太多；2026年的构造做到了。

AlphaProof Nexus（2026年5月）。谷歌DeepMind让其结合了Gemini模型与Lean的智能体，去攻克埃尔德什问题数据库中的353个公开问题。它解决了9个，其中两个已悬而未决56年，并证明了整数序列在线百科全书（OEIS）中的44个猜想。每一个证明都能在Lean中编译通过。但请注意成功率：大约2.5%。

Astra（2026年8月）。OpenAI公布了其尚未发布的下一代模型的十项成果，包括首次构造出“非sofic群”（回答了米哈伊尔·格罗莫夫在1999年提出的问题）、三个埃尔德什问题，以及1978年以来对球体堆积一般上界的首次改进。每项成果都附有Lean证书。一项独立的人工审核没有在主要成果中发现经确认的实质性错误，但其中一项成果收到了专家提出的重大修改要求；截至撰稿时，期刊同行评审尚未完成。

学生常常混淆的区别

并非每个“AI解决了”的标题都属实

2025年10月，OpenAI员工发帖称GPT-5解决了十个“未解决”的埃尔德什问题。维护埃尔德什问题数据库的托马斯·布鲁姆解释说，他网站上的“未解决”只表示他本人不知道解答——模型其实是在旧论文里找到了已有的解答。这些帖子随后被删除。找到被遗忘的文献是有用的，但那不是解决问题。看到关于AI与数学的标题时，先问三个问题：有独立专家检验过吗？有机器检验过的（Lean）证明吗？这个问题真的未解决吗？

五十年，一条时间线

图示：证明中的机器五十年，1976–2026

197620002026

1976 — 四色定理
1994 — 费马大定理
1996 — 罗宾斯猜想
1998 — 开普勒猜想
2016 — 布尔勾股数组
2019 — 凯勒猜想（7维）
2025 — 三维挂谷问题
2026 — 格雷厄姆重排猜想
2026 — 埃尔德什单位距离（被推翻）
2026 — 非sofic群（Astra，已宣布）

手工计算机辅助计算机发现AI时代成果

颜色与专题页一致：绿色为手工证明，蓝色为计算机辅助，紫色为计算机发现，粉色为AI时代。即使在2026年，一个重大问题（格雷厄姆猜想）仍然是由人类解决的。

时间线

1976年阿佩尔和哈肯借助一千多个小时的计算机检验证明了四色定理——第一个著名的计算机辅助证明。
1996年威廉·麦丘恩的自动证明器EQP在大约八天后自己找到了罗宾斯猜想的证明。
1998年托马斯·黑尔斯宣布了开普勒猜想（球体堆积）的计算机辅助证明。
2005年贡蒂埃和韦尔内在证明助手Coq中验证了四色定理的完整证明。
2014年Flyspeck项目完成了开普勒猜想的完全机器验证证明。
2016年SAT求解器解决了布尔勾股数组问题：答案是7,825，证明大小200TB。
2019年凯勒猜想的7维情形由SAT求解解决——这是最后一个未解决的维度。
2025年10月关于GPT-5“解决”了十个埃尔德什问题的说法被撤回：这些解答早已存在于文献中。
2026年5月OpenAI的一个模型推翻了埃尔德什1946年的单位距离猜想；DeepMind的AlphaProof Nexus在Lean中解决了9个埃尔德什公开问题。
2026年8月OpenAI公布其未发布模型Astra的十项成果，附Lean证书，其中包括第一个非sofic群。

如果你正在学数学，这意味着什么

本文的每一项成果仍然依赖于人：必须有人准确地陈述问题，决定哪种方法值得一试，检查计算机证明的定理正是重要的那一个，并解释它为什么成立。这正是学校数学要求你“写出解题过程”时培养的能力，也是我们的文章AI真的会做数学吗？的主题。仍未解决的问题，以及这些已解决问题的逐张卡片列表，请见我们的未解数学之谜专题。

参考资料与延伸阅读

最后核实：2026年10月3日。AI领域的成果变化很快，最新情况请以上方来源为准。

常见问题

计算机辅助的证明是“真正的”证明吗？

是的：其逻辑和任何证明都一样，计算机只是执行那些对人来说步骤太多或太长的部分。真正的问题在于，如何确认计算机正确地完成了这些步骤。这正是四色定理和开普勒猜想的证明后来在证明助手中重新验证（2005年的Coq和2014年的Flyspeck项目）的原因——证明助手会机械地检查每一个逻辑步骤。

AI真的解决了未解的数学问题，还是只是炒作？

两种情况都有。真实的成果包括2026年5月对埃尔德什单位距离猜想的推翻（由九位撰写配套论文的顶尖数学家检验），以及DeepMind的AlphaProof Nexus在尝试的353个埃尔德什公开问题中解决了9个，并附有机器验证的Lean证明。但在2025年10月，GPT-5解决了十个埃尔德什问题的说法被证明只是重新找到了已发表的解答，相关帖子已被删除。状态核实日期：2026年10月3日。

Lean是什么？它为什么对AI做数学很重要？

Lean是一种“证明助手”：一种编程语言，用它写的证明精确到计算机可以检查每一步。如果AI用Lean写出证明并且编译通过，你就不必再信任AI本身——只需信任那个小巧且经过充分测试的检查程序，以及定理的陈述确实表达了你所想的意思。这就是为什么2026年大多数严肃的AI数学成果都附有Lean证明。

AI会取代数学家吗？

从目前的证据看不会。即使是2026年最强的系统，也只能解决它所尝试的公开问题中的一小部分（AlphaProof Nexus：所尝试的埃尔德什问题中约2.5%），而选择问题、检查陈述、解释结果并围绕它们构建理论的，仍然是人。变化很快的是：有多少搜索和检验工作可以交给机器。

读者评分与评价

从多个维度为这篇文章打分——您的评价既能帮助其他读者,也能帮助我们不断改进。

这篇文章对您有帮助吗?

告诉我们您的想法——可以是需要更正的地方、尚未解答的问题,或您希望我们接下来讲解的主题。

想直接沟通吗？ 在方便的时间预约免费视频通话：简短问题15分钟，其他问题30分钟。时间以您所在的时区显示。

预约通话

关于作者

Sudershan Soni

Mostak Services 的创始人兼首席导师——拥有硕士学位的数学、科学、计算机科学与 STEM 导师,拥有超过20年的职业经验,通过在线授课为全球从 11+ 和 GCSE 到 A-Level 及更高阶段的学生提供教学。

阅读完整履历