仅仅五年前，语言模型能解决多步骤数学题还近乎一件新奇事。如今，问题已经不只是它能否完成练习，而是：当它也能产出研究成果时，会发生什么？
这个变化的意义远超任何基准排行榜。几个世纪以来，新证明一直是一种稀缺产物：它可能耗费数月、数十年，甚至一整个职业生涯。论文发表、学术声誉、人才培养以及很大一部分数学文化，都是围绕这种困难建立起来的。
如果证明生产开始能够通过计算规模化，稀缺并不会消失，只会转移。
从习题到开放问题
近年的发展解释了这场讨论为何变化得如此迅速。
OpenAI 在 2021 年发布 GSM8K，正是因为当时的大模型仍会系统性地答错需要多步推理的小学数学题。一年后，Google 的 Minerva 在中学、大学和定量科学的技术题目上取得了明显进展。
2023 年，FunSearch 把程序生成模型和自动评估器结合起来。它为 cap set problem 找到了新的构造，也为 bin packing 找到了更好的启发式方法。关键变化在于：系统生成的候选方案可以被检验，并在超越已知最佳结果时被保留下来。
2024 年，AlphaGeometry 在一组历史奥数几何题上接近人类金牌选手的平均水平。同年，AlphaProof 与 AlphaGeometry 2 解出了国际数学奥林匹克六道题中的四道，获得 42 分中的 28 分，达到银牌水平。
2025 年 7 月，高级版 Gemini Deep Think 达到金牌水平：解出五道题、获得 35 分，并在 4.5 小时限制内直接用自然语言写出证明。竞赛这道象征性门槛已经跨过，但仍有一个令人安心的区别：奥赛不是研究。
2026 年，证据的性质发生变化
First Proof 直接测试了这条边界。项目收集了十个来自真实研究过程的问题；作者知道答案，但从未公开发表。四套系统在受控条件下作答，由 30 位专家评审。
十个问题中有七个至少得到了一份被评为基本无误或只需小幅修改的解答。报告也记录了典型缺陷：系统常常详细展开常规步骤，却快速略过最困难的环节；有些引用也并不支持对应主张。
这比一句“AI 已经会做数学”更有价值。它既显示了小样本中的真实能力，也揭示了貌似可信的文本在接受专家评审时暴露的问题。
同年 5 月，OpenAI 发布了一个由内部模型生成的反例，推翻了 Erdős 关于平面单位距离的一项猜想。外部数学家检查了证明，并撰写配套论文进行解释和定位。
8 月，OpenAI 公布了内部 Astra 系统在几何、编码理论、群论、复杂性、密码学和组合数学等领域的十项结果。该公司称，数学论证由模型生成，人类与模型共同整理成论文，随后模型又把每项论证形式化为 Lean 证书。结果已经公开并可检查，但它们的长期意义应由数学共同体判断，而不是由公司的发布稿决定。
几天后，Anthropic 公布了另一项醒目进展。实验版 Claude 尝试攻克黎曼猜想，但没有成功。不过在过程中，它给出了一个论证，把与临界线上 zeta 零点比例有关的下界从 41.6% 提高到 67.2%。
这并不意味着黎曼猜想“解决了 67%”。Anthropic 明确表示，不认为这项技术会导向猜想的证明。公司内部两名数学家验证了工作，外部专家进行了审阅，并且已有 Lean 形式化版本。这是相关问题上的进展，而不是主猜想的一部分答案。
验证证明不等于理解证明
数学相较其他科学有一项特殊优势。模型提出的新分子仍然需要实验室验证；数学证明则可以被翻译成形式化对象，由一个很小的软件内核逐步检查。Lean 不需要相信公司声誉，也不需要相信作者直觉。
但形式化验证只回答一个有限问题：结论是否通过有效推理，从编码后的公理与定义中推出？它不会告诉我们形式化陈述是否忠实表达了原问题，也不会说明证明是否带来解释，更不会判断结果是否值得关注。
一份十万行的证明可以完全正确，却仍然无法被不理解其核心思想的共同体使用。把它改写成流畅文字也不够。过度润色的解释可能会隐藏选择、失败尝试和关键联系，而这些恰恰是人真正学会一个论证的途径。
从证明稀缺到证明消化不良
Terence Tao 把风险描述为从证明稀缺走向证明过剩。如果假设 AI 将完成相当一部分研究任务，就会出现一串新的瓶颈：
- 生成候选证明；
- 验证它是否正确；
- 解释到他人能够理解；
- 让共同体评估并使用它；
- 把它整合进理论、课程和教科书。
自动化第一步不会自动化后续步骤，反而可能淹没它们。证明积累的速度可能超过我们评审、阅读以及将其转化为共享知识的速度。
这个问题早于 AI 就已存在。高度专业化、超长论文和同行评审压力，早已让一部分文献难以消化。大规模生成只会放大这种不匹配。
真正有价值的也许从来不只是定理
解决问题只是数学活动的一部分。选择好问题、建立定义、发现联系、培养判断、教学，以及维持一个能够传递隐性知识的共同体，同样重要。
过去，这些活动通常彼此相关。要写出困难的证明，往往必须深刻理解问题；在过程中还会产生新技术、新直觉和新问题。因此，“证明一个结果”可以粗略代表许多其他贡献。
AI 可能打破这种相关性。如果生成证明只需几分钟，而理解它为何成立需要几个月，那么最终产出就不再足以衡量工作的价值。
这会迫使我们面对更难的问题：
- 当生成、筛选、验证和解释由不同主体完成时，荣誉应归于谁？
- 如果把学习者形成数学思维所必经的艰难步骤自动化，我们该如何培养数学家？
- 当文献增长快于人类阅读能力时，如何决定优先级？
- 一套理论能否在形式上完全正确，却没有任何人理解其整体？
- 即便某项活动可以自动化，哪些部分仍应保留为人的活动？
答案既不是拒绝所有自动化，也不是接受任何通过验证器的东西。我们需要让生成、验证、署名与解释彼此分离，并且全程可见。
AI 不会让数学变得无趣。它只是让我们无法继续把生产证明和建立理解混为一谈。如果证明不再是最困难的部分，我们或许会发现：真正的价值一直也包括知道该证明什么、为什么重要，以及如何让别人理解。
资料来源
- OpenAI：GSM8K
- Google Research：Minerva
- Google DeepMind：FunSearch
- Google DeepMind：AlphaProof 与 AlphaGeometry 2 在 2024 年 IMO 的表现
- Google DeepMind：Gemini Deep Think 在 2025 年 IMO 的表现
- First Proof：第二批测试报告
- OpenAI：单位距离猜想的反例
- OpenAI：数学与理论计算机科学的十项进展
- Anthropic：与黎曼 zeta 函数有关的进展
- Terence Tao：Mathematics in the age of AI
