数学中的 AI 指能证明定理、解决奥赛题和研究级问题并检验证明的人工智能系统。形式化语言 Lean 在其中起着关键作用：用它写成的证明由计算机检验，因此不必信任模型本身，也能检验 AI 的结果。
三年间，这一领域从奥赛银牌水平（2024 年）走到了数百篇带有新结果的手稿（2026 年）。12 这让数学家们既兴奋又不安：陶哲轩说“证明充裕的时代”正在到来，而国际数学联盟则支持了一份宣言，主张数学应当始终是人的事业。34
历史
- 14.12.2023Google DeepMind 在 Nature 上发表 FunSearch 系统：语言模型配合自动检验，找到了新的大型 cap set 构造，优于此前已知的结果。5 ¶ cza2rk877
- 25.07.2024DeepMind 的 AlphaProof 和 AlphaGeometry 2 系统解出国际数学奥林匹克六道题中的四道，得 28 分，达到银牌水平；其中一道题用时几分钟，其余最长用了三天。AlphaProof 把预训练语言模型与 AlphaZero 的强化学习算法结合起来，用 Lean 证明命题。1 ¶ cpmp95wjd
- 14.05.2025DeepMind 的 AlphaEvolve 找到一种只需 48 次标量乘法就能完成 4×4 复数矩阵乘法的方法，优于 1969 年的施特拉森算法。在 50 多个开放问题上，该系统约 75% 的情况下复现了已知最优解，20% 的情况下改进了它们。6 ¶ cz2yux3ij
- 19.07.2025OpenAI 宣布，其实验性推理模型在奥赛中取得了金牌水平的成绩。7 ¶ ccp7fkcq7
- 21.07.2025DeepMind 的 Gemini Deep Think 正式获得奥赛金牌：六道题中完整解出五道，42 分中得 35 分，在 4.5 小时的比赛时限内完成；结果由奥赛协调员按照评判学生答卷的同一标准正式评分并确认。8 ¶ c4xkfkcjr
- 08.09.2026OpenAI 称，其内部模型证明了纳维–斯托克斯方程（带外力）可能出现奇点，在 88 小时内动用了约 10 000 个智能体；证明已在 Lean 中形式化。9 ¶ cfknhmsr6
- 2026年10月8日《科学》刊发 DeepMind 关于 AlphaProof Nexus 智能体的论文：它自主解决了 353 个未解埃尔德什问题中的 9 个，证明了整数数列线上大全（OEIS）492 个猜想中的 44 个，所有证明都经 Lean 验证。同期，数学家 Jeremy Avigad 和 Matthew Ballard 发表评论《用于数学研究的 AI 已经到来》。10 ¶ ckdzaxmkz
工作原理
有两种思路。第一种是模型以程序或构造的形式搜索解，再由自动评估器检查它们是否优于已知结果：FunSearch 和 AlphaEvolve 就是这样工作的。第二种是模型用形式化语言 Lean 写出证明，由计算机检验：AlphaProof 以及 Math Inc 公司的 Gauss 项目都是这样。Gauss 用三周时间形式化了素数分布定理的强形式，约 25 000 行 Lean 代码，这项任务是陶哲轩和亚历克斯·康托罗维奇（Alex Kontorovich）在 2024 年 1 月提出的。11 ¶ c6575vwd8
数据
| 研究 | 测量内容 | 结果 |
|---|---|---|
| Epoch AI，FrontierMath，07.11.202412 | 研究级数学水平的全新难题 | 最好的模型只解出不到 2% 的题目 ¶ cc9ttcnpr |
| OpenAI，06.10.20262 | 发布在 GitHub 上的内部模型成果；公司自己的评估 | 372 个组共 719 篇手稿，涉及约 4000 个提出的问题；平均每个结果约需 ChatGPT Pro 在思考模式下工作三小时；其中三篇手稿因符号错误很快被撤回 ¶ cghjnybxm |
两年间，AI 从研究级问题上的“不到 2%”和奥赛银牌，走到了数百篇带有新结果的手稿。可检验性是数学区别于其他领域的主要之处：Lean 中的证明由计算机检验，因此 AI 在这里的速度受限的不是对模型的信任，而是人类理解和吸收这些结果的能力。需要说明：部分说法来自公司的内部评估，而 OpenAI 最引人注目的成果出自一个外界无法检验的模型。 ¶ c8xxc87et
批评
2025 年 10 月，研究人员宣布借助 GPT-5 找到了 10 道被列为未解的埃尔德什问题的解。erdosproblems.com 数据库的维护者托马斯·布卢姆（Thomas Bloom）称这种说法是“严重的歪曲”：GPT-5 找到的是已经发表、载有解答的论文，只是他本人此前不知道；“未解”状态仅仅意味着他不知道有这样的论文。他说，模型检索文献的能力“本身就已经足够有用、足够令人印象深刻，没必要把它说成它并不是的东西！”13 ¶ cydu4nn57
OpenAI 的成果发布后，The Verge 采访了三十多位数学家；巴尔托什·纳斯克任茨基（Bartosz Naskręcki）说，这“可能导致学术文化的大规模崩塌”。14 ¶ c6fm7zxay
《科学美国人》2026年10月13日报道：数学家们研读 OpenAI 长达 166 页的纳维-斯托克斯方程证明后发现，其中外力的构造方式与西班牙数学家 Diego Córdoba 和 Luis Martínez-Zoroa 的路线完全不同——而在发布时，公司自己曾“明确且反复地”表示证明沿用了这条路线。15 ¶ cdpxcquac
蒂莫西·高尔斯说，他对数学中的 AI 最大的担忧是“数学文化可能遭到摧毁”，也就是那些不仅存在于文献中、也存在于数学家头脑里的知识和经验。16 ¶ czth2y863
发展
2026年6月2日，关于人工智能与数学的《莱顿宣言》发布，国际数学联盟表示支持：功劳和责任仍属于数学界的人类，不应归于自动化系统。4 ¶ cxrzjmjxp
陶哲轩主张不要再盲目追求解题：他认为，在证明充裕的时代，这种做法已经开始损害数学的长远健康。3
信号
- 科学 / 杰克·克拉克: “AI 正在变得有创造力——无论是在数学上还是在 AI 研究本身，因此完全的递归自我改进如今更可能在 2027 年而不是 2028 年成为可能”Anthropic 联合创始人，在其通讯 Import AI 中谈一项衡量模型研究品味的基准；今年 5 月，他估计到 2028 年底模型能自主训练出自己继任者的概率为 60%
- 科学 / 陶哲轩: “我们正进入数学的证明丰裕时代”在加州理工学院的“Math 2.0”讲座中谈 AI 对数学的影响
- 科学 / 雨果·迪米尼尔-科潘: “OpenAI 一次发布数百份 AI 证明是“巨大的冲击”：对数学家来说，“已经是第二天了”；其中一个问题让他觉得像背着一个人跑马拉松，那人在最后 100 米跳下来，抢先冲过终点”法国数学家、2022 年菲尔兹奖得主，在瑞士广播电台 RTS 节目中谈及 OpenAI 公开数百篇 AI 证明手稿一事——其中 16 篇涉及他所在领域的问题
- 科学 / 蒂莫西·高尔斯: “证明 LLM 证明不了的东西”菲尔兹奖得主谈 ChatGPT 一小时内完成博士水平的研究
参见
参考资料
-
AI achieves silver-medal standard solving International Mathematical Olympiad problems — Google DeepMind, 25.07.2024. deepmind.google ↩ ↩2
-
openai/math — OpenAI, GitHub, 06.10.2026. github.com ↩ ↩2
-
Math 2.0 — Terence Tao, 10.10.2026. terrytao.wordpress.com ↩ ↩2
-
Leiden Declaration on Artificial Intelligence and Mathematics — 02.06.2026. leidendeclaration.ai ↩ ↩2
-
B. Romera-Paredes et al. Mathematical discoveries from program search with large language models — Nature, 14.12.2023. nature.com ↩
-
AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms — Google DeepMind, 14.05.2025. deepmind.google ↩
-
Alexander Wei: «our latest @OpenAI experimental reasoning LLM has achieved … gold medal-level performance» — X, 19.07.2025. x.com ↩
-
Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad — Google DeepMind, 21.07.2025. deepmind.google ↩
-
On the Navier–Stokes Millennium Prize Problem — OpenAI, 08.09.2026. openai.com ↩
-
Tsoukalas et al. Advancing mathematics research with AI-driven formal proof search — Science, 08.10.2026. doi.org ↩
-
Introducing Gauss, an agent for autoformalization — Math, Inc. math.inc ↩
-
E. Glazer et al. FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI — arXiv, 07.11.2024. arxiv.org ↩
-
Thomas Bloom: «this is a dramatic misrepresentation» — X, 17.10.2025. x.com ↩
-
‘Pure insanity’: Mathematicians will need years to make sense of OpenAI’s latest drop — The Verge, 09.10.2026. theverge.com ↩
-
OpenAI’s blockbuster Navier-Stokes proof isn’t what we thought it was — Scientific American, 13.10.2026. scientificamerican.com ↩
-
Thoughts about the Leiden Declaration — Timothy Gowers, 26.07.2026. gowers.wordpress.com ↩