刚刚过去的一周，大概是纯数学与 AI 关系史上最戏剧性的一周：10 月 6 日，OpenAI 一次性公开了 372 项数学结果（共 722 份手稿文件），两天内引来数学家组织的公开抵制；同一天，菲尔兹奖得主陶哲轩在社交网络上提出了「Math 2.0」的路线主张；媒体随即发现，OpenAI 的解法「尚未达到数学界的标准」。这不是孤立事件，而是过去两年「AI 做数学」从奥赛奖牌一路冲进研究前沿之后，必然到来的一次总摊牌。
这篇文章梳理这条线：机器辅助证明已经走到哪一步，哪些成绩经得起核验，哪些争论在撕裂数学社区，以及接下来会怎样。
先说结论：机器证明的边界在哪里
把两年来的证据放在一起，当前边界大致可以画成三条。
能做的：竞赛级数学已被攻克——2025 年两家机构的系统在同届 IMO 上双双达到金牌级；对个别研究级开放问题，AI 能给出完整且经得起人工核验的解答，2026 年 5 月对 Erdős 单位距离猜想的反驳是标志性案例；在形式化验证一侧，把人类证明翻译成机器可查证明的效率在 2026 年已从「以年计」压缩到「以小时计」。
不能做的：未经核验的大批量「成果」不等于数学。10 月 6 日那批结果发布不到三天，OpenAI 自己已因缺陷撤回其中若干证明；陶哲轩反复强调，AI 加速的是证明的生产，而证明的核验、讲解与消化仍是人类瓶颈。他在 2026 年 8 月提交 ICM 2026 的报告《AI 时代的数学》中写下一句被广泛引用的话：一个没有任何人类能恰当解释的证明，即使通过了形式化验证，也应视为未完成。
没人能做的：知识的规范化（canonicalization）——判断哪个证明值得进入教科书、如何把它安放进已有理论——被陶哲轩称为「最不适合用 AI 优化、也最有价值」的环节。这一段今天仍完全属于人类，而且正是它，成了 10 月这场冲突的引爆点。
两年三级跳：从奥赛银牌到研究前沿
奖牌时刻
2024 年 7 月 25 日，Google DeepMind 宣布 AlphaProof 与 AlphaGeometry 2 联手解出 IMO 2024 六道题中的四道，拿到 28/42 分，达到银牌水平——距离金牌线 29 分只差一分。其中 AlphaProof 用强化学习在 Lean 形式空间里搜索证明，解出两道代数题和最难的那道数论题（609 名参赛选手中只有 5 人解出）；AlphaGeometry 2 在完成形式化后 19 秒内解出几何题。评分由 Timothy Gowers 等数学家按 IMO 规则完成，这套方法论后来于 2025 年 11 月发表在 Nature 上。
真正的转折在 2025 年 7 月。DeepMind 的 Gemini Deep Think 在 IMO 2025 上五题满分、35/42 分，达到金牌级——关键是它完全用自然语言作答，直接从官方题目出发，在 4.5 小时限时内完成，不再依赖 Lean 或数天运算，评分由 IMO 协调员按与人类选手相同的标准完成。同一个周末，OpenAI 也宣布其实验推理模型取得 35/42 的金牌级成绩，评分者是多位前奖牌得主，但因未经 IMO 官方确认、未按惯例等待核验就自行公布，OpenAI 受到 IMO 官方与 DeepMind 研究者的批评。这场口水战如今回看，只是预演。
下表汇总了这条主线上的代表成果：
| 系统 | 机构 | 公布时间 | 成果 | 验证方式 |
|---|---|---|---|---|
| AlphaProof + AlphaGeometry 2 | Google DeepMind | 2024-07 | IMO 2024 解出 4/6 题，28/42 分，达银牌级 | 数学家人工评分（IMO 规则） |
| Gemini Deep Think | Google DeepMind | 2025-07 | IMO 2025 五题满分，35/42，金牌级，纯自然语言 | IMO 协调员按学生标准评分 |
| OpenAI 实验推理模型 | OpenAI | 2025-07 | 同届 IMO 35/42，金牌级 | 前奖牌得主评分，未获 IMO 背书 |
| Aristotle | Harmonic | 2025-10 | IMO 2025 金牌级解题，并完成 Lean 形式化验证 | Lean 机器验证，附技术报告 |
| 未公开内部推理模型 | OpenAI | 2026-05 | 反驳 Erdős 单位距离猜想 | 数学家人工核验，配套论文发表 |
| 未公开内部模型 | OpenAI | 2026-09 | 声称解决 Navier–Stokes 千禧年问题，附 Lean 证明 | 社区核查中，Clay 未认可 |
timeline
title AI 做数学的三个加速年
2024-07 : AlphaProof 与 AlphaGeometry 2 达 IMO 银牌级
2025-07 : 两家系统先后宣布 IMO 金牌级成绩
2025-11 : AlphaProof 方法论发表于 Nature
2026-05 : OpenAI 模型反驳 Erdős 单位距离猜想
2026-08 : 陶哲轩发表 ICM 报告《AI 时代的数学》
2026-09 : OpenAI 声称给出 Navier–Stokes 解法
2026-10 : 372 项结果一次性发布，AHM 呼吁抵制
2026 年的三次冲击
第一次冲击在 5 月：单位距离问题。 这是 Erdős 1946 年提出的平面组合几何问题：平面上 n 个点之间最多能有多少对距离恰为 1 的点对。此前最好的构造来自缩放方格，量级约为 n^(1+c/log log n)，Erdős 本人猜测这已接近最优上界。OpenAI 在官方公告中宣布，一个未公开的通用推理模型在评估过程中构造出无穷多个反例：存在固定正数 δ，使无穷多个 n 可达到 n^(1+δ) 规模的单位距离对——猜想被推翻。数学上，模型的思路是把经典的高斯整数构造换成更一般的代数数域，并动用无限类域塔与 Golod–Shafarevich 理论控制分歧；后续由 Will Sawin 精化出显式常数 δ=0.014。Noga Alon 等数学家人工核验后发表了配套的 arXiv 论文，Gowers 称之为「AI 数学的里程碑」。这是一个子领域核心开放问题首次由 AI 自主解决（OpenAI 的说法），而且走的正是「AI 生产 + 人类核验」的理想分工。
第二次冲击在 9 月 8 日：Navier–Stokes。 OpenAI 宣布其模型给出千禧年大奖问题之一——Navier–Stokes 方程解的存在性与光滑性——的解法，附完整 writeup 与 Lean 形式化证明，同时声明不会去申领 Clay 数学促进会的一百万美元奖金。争议立刻从三个方向涌来：其一，优先权——坊间早有哈佛青年学者 Levent Alpöge 与纽约大学的 Tristan Buckmaster 接近解决此问题的传闻，OpenAI 承认工作受此「启发」但否认直接使用，称证明方法（尤其在 Euler 情形）有实质差异；其二，资格——Scientific American 的标题是「OpenAI 是不是解错了 Navier–Stokes 问题」，其证明是否符合 Clay 奖的认定条件取决于规则上的一个争议「漏洞」，Clay 始终未做任何认可；其三，程序——9 月，25 位顶级数学家（含多位菲尔兹奖得主）联署宣言《AI 在数学中的严重错位》，警告以基准驱动的批量产题解法与数学追求概念理解的目标严重错位。TechCrunch 当时用的标题是「OpenAI 与数学家的梁子只会越结越深」。
第三次冲击就在 10 月 6 日：批量轰炸。 OpenAI 公开一个代码仓库，内含 372 项结果、722 份手稿文件。批评在 48 小时内组织化：新近成立的「人类数学协会」（Association for Human Mathematics，AHM）于 10 月 7 日发表声明，其中的话迅速传遍社区——「一次发布 700 多份文件，展示的不是学术，而是力量。」AHM 的指控相当具体：OpenAI 自己召集的数学与 AI 顾问组（AGMAI）曾建议前沿实验室不要在内部模型上测试高难度数学问题，却被无视；数学家从未请求这些工作；声称此举「推进了数学」不成立。AHM 呼吁数学家停止与 OpenAI 合作。媒体的独立核查同样不留情面：TechCrunch 发现这批解法偏离了 OpenAI 此前咨询的数学家们定下的成文指南；The Atlantic 的评价是，这批证明比上一代 AI 文本明显清晰，但整体而言写得并不好。OpenAI 则已因缺陷撤回其中若干证明。
Lean：机器证明的「法庭」
理解这一切冲突，需要看清一个底层角色：形式化验证生态，核心是 Lean 定理证明器与其数学库 mathlib。
陶哲轩对 Lean 的定位极为清醒：它是形式化证明助手而非自动定理证明器——它验证人类已有的证明，本身并不擅长发现新证明。但它的价值在信任结构上：一份通过 Lean 检验的证明，其正确性不再依赖作者的声望与审稿人的勤勉。他的手笔之一是 2023 年牵头把 PFR 猜想（多项式 Freiman–Ruzsa 猜想）的证明在三周内由约二十位协作者完整形式化，被视为「工业化数学」的样板。
生态在 2026 年的进展是实打实的。Xena 项目统计，截至 2025 年 12 月，Erdős 问题网站约 240 道问题已有 Lean 形式化陈述、17 道有完整 Lean 证明；Harmonic 公司的 Aristotle 在 2025 年 10 月的技术报告里把 IMO 金牌级解题与 Lean 验证合成一条流水线；基准从 FormalMATH 的 5560 道题演进到面向研究生级数学的 FormalProofBench 与取材 arXiv 论文的 MathArena ArXivLean。陶哲轩观察到，自动形式化已把过去以年计的形式化工程压缩到以小时计。
但「Lean 证书」正在成为一个需要警惕的词。10 月这批结果中部分附带 Lean 证书，社区随即指出关键缝隙：机器只保证 Lean 里的命题为真，并不保证它和原始自然语言命题是同一句话——自动形式化这一步的忠实性本身可能出错。这正好呼应陶哲轩在《AI 时代的数学》里的告诫：验证只是流水线的一环，一份「没有任何人能解释」的证明应当视为未完成。他在文中举的数字同样值得记住：Erdős 问题数据库已经收到数十份 AI 生成的证明提交，其中许多人类根本无法核验；他的「第一证明」项目第二批十道全新研究题，到 2026 年 5 月已有七道被至少一个系统通过，单题成本仅数十到数百美元。
抵制与「数学 2.0」：数学界如何分裂
抵制派：先慢下来
AHM 是个新组织，宗旨是把数学作为一项人类志业来保护、让数学社区独立于公司利益。它的抵制呼吁得到了认真对待——arXiv 被海量 AI 生成投稿冲击「几乎不可用」的警告（New Scientist 报道）、8 月 arXiv 上主张全面反对 AI 的长文《AI 生成数学的危机》、9 月 25 人宣言，声浪是连续的。需要澄清一个流传甚广的误读：陶哲轩在自己的博客转发了 AHM 声明，但他本人并未表态支持抵制，除了编辑注记与一句「本文初稿为其他格式、经 AI 转换」的披露外没有个人评论——顺带一提，这条披露本身就是他 AI 重度使用者的注脚。
「数学 2.0」：换一套价值坐标
陶哲轩的立场，在 10 月 6 日的 Mathstodon 帖子里说得最完整：「Math 1.0」把溢价给了第一个解出开放问题的人，哪怕解法最初无人能懂；如今这个目标已被优化到不可持续，「Math 2.0」将需要弱化裸解题的角色，更整体地衡量数学进步——比如抬升讲解（exposition）的地位，也抬升社区建设与开辟新方向的地位。此前数小时他还在连续发帖警告：批量生产而不消化的解法，正在让领域失去讲座、合作与后续工作，数学正变得「不那么肥沃」。
这套主张的学理版就是 8 月提交的 ICM 报告《AI 时代的数学》。他先立下「工作假设」——AI 达到研究级数学能力是迟早的事，然后不去争论会不会，而是追问数学研究的价值到底是什么。答案是流水线的重构：生成、验证、讲解、发表、规范化五段中，AI 碾压第一段、擅长第二段、在讲解上记录「喜忧参半」——过度打磨的证明「易读而难学」；而规范化的价值反而因稀缺而上升，因为 AI 训练数据恰恰就是规范化的产物。既然期刊、优先权、奖项、招聘都是按「证明稀缺」设计的制度，它们在「证明过剩」时代必然失灵——这是古德哈特定律的教科书案例。他据此提出四条建议：披露工具使用、把社区重心从证明生成移向证明消化、确认作者的署名与责任归于人类、主动标注来源；还给出一条可操作的铁律——作者若不能就其结果做一场清晰的专家级报告，就不应发表。制度侧的落点是 6 月获国际数学联盟背书的《莱顿宣言》。
两派共享同一个事实判断（证明正在过剩），分歧在处方：抵制派要求先按停公司主导的批量发布，陶哲轩要求改造数学界自身的价值与基础设施。前者把 10 月 6 日视为越界，后者视为一次压力测试。
趋势判断（以下为推测）
其一，竞赛数学作为基准已经退役。IMO 金牌 2025 年到手，DeepMind 后续的 IMO-ProofBench 上 Deep Think 已刷到 90% 分段，前沿社区的评价轴正整体移向研究级基准。下一个「IMO 时刻」将出现在某本顶刊的常规问题上，而非奥赛。
其二，「发布即完成」与「核验后才算数」的拉锯会继续升级，且不会由争论解决，只会由事故解决。10 月 6 日之后，任何一家再搞批量发布，都会被放在同一套显微镜下；而 OpenAI 撤回自家证明的动作，说明「先发布后核验」连公司自己也在支付成本。下一个千禧年问题声明几乎必然出现（已有预测市场开盘赌年内出现第二例），但它被社区接受的速度，将取决于是否能配齐 Alon 式的人肉核验链条。
其三，形式化验证会成为发布标配，但争夺点移向忠实性。Lean 证书会越来越常见，围绕「自动形式化是否忠实翻译了原命题」的审查会成为新的审稿环节；谁能把「自然语言命题到形式陈述」的转写也做成可核验的，谁就掌握下一代的信任基础设施。
其四，数学社区的组织形态会被迫重构。披露规范、讲解优先的荣誉体系、给「消化者」记分的机制，方向已由莱顿宣言画出；剩下的问题是速度——公司发布节奏以周计，学术制度以年计，这个时间差正是目前一切摩擦的根源。
小结
回到开头的问题：AI 做数学研究走到哪一步了？它已经越过竞赛数学的天花板，在研究前沿拿下了第一个经人类核验的猜想反驳，也第一次展示了批量生产数学结果的能力；但它还没有学会（或者说还没有兴趣学会）数学最看重的那部分——把一个证明变成共同体的知识。10 月这一周的意义，不在 372 这个数字有多大，而在数学界第一次作为整体划出了红线：能被机器生成的证明越来越多，能被人类理解的证明才是数学。边界不在模型的能力上，而在我们打算为「理解」保留多少位置。
参考资料
- Mathematics in the age of AI（Terence Tao，arXiv:2608.16753）——ICM 2026 报告成文，「证明过剩」论与四条社区建议的原始出处。
- AHM Statement on OpenAI's October 6 Release（ahmath.org）——抵制声明原文，「展示的不是学术，而是力量」即出于此。
- AHM 声明的陶哲轩博客转载页（terrytao.wordpress.com）——可见陶哲轩本人的编辑注记与 AI 使用披露，判断其立场的一手材料。
- An OpenAI model has disproved a central conjecture in discrete geometry（OpenAI）——单位距离问题成果的官方一手报告，含方法与外部核验细节。
- AI achieves silver-medal standard at the IMO（Google DeepMind，2024-07-25）——AlphaProof/AlphaGeometry 2 成绩、评分方式与 Nature 发表信息的一手来源。
- Gemini Deep Think achieves gold-medal standard at the IMO 2025（Google DeepMind，2025-07-21）——金牌级成绩与自然语言作答细节的一手来源。
- Terence Tao 的 Mathstodon（2026-10-06 帖）——「Math 1.0/Math 2.0」提法的原始出处。
读者留言
COMMENTS 暂无还没有留言，来说第一句？