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