夜雨聆风2026年5月21日，《自然》（Nature）杂志刊发资深记者 Davide Castelvecchi 的长篇特稿，系统梳理了人工智能在纯数学领域取得的一系列突破性进展。报道指出，从没有数学专业背景的业余爱好者到顶尖数学家，越来越多的人开始借助大语言模型（LLM）攻克长期悬而未决的数学难题，这一趋势正引发整个数学界对自身未来走向的深刻反思。
上月，居住在英格兰西南部的 Liam Price 与剑桥大学本科生 Kevin Barreto 合作，利用 ChatGPT 成功解决了匈牙利数学家 Paul Erdős 于 1966年 提出的第1196号问题。该问题涉及"原始集"——即集合中任何一个整数都不能整除其他整数的整数集合，素数集是其典型代表。值得关注的是，此前尝试解决该问题的数学家大多将其转化为概率论语言来处理，而 ChatGPT 直接在问题的 原始表述框架 内给出了证明，其策略之新颖令专家们感到意外。
小知识：什么是 Erdős 问题？Paul Erdős 是20世纪最多产的数学家之一，一生中收集了超过1000个数学猜想与问题，并为解决它们悬赏不同金额。这些问题横跨数论、组合学、图论等多个分支，至今仍有大量未解。解决一个 Erdős 问题在数学界被视为重要成就。
加州大学洛杉矶分校数学家 Terence Tao 指出，ChatGPT 的解法虽然形式上停留在数论语言中，但 隐含地建立了数论与概率论之间的联系 。斯坦福大学数学家 Jared Duker Lichtman 则在社交媒体上将这一突破类比为国际象棋——仿佛 AI 发现了一种因"人类审美与惯例"而从未被考虑过的全新开局。OpenAI 数学家 Sébastien Bubeck 评论道："这太不可思议了。一年前人们还认为大语言模型可能永远无法超越训练数据的边界。"
小知识：大语言模型为何能做数学？大语言模型（如 GPT、Gemini、Claude）并非专门为数学设计，它们通过海量文本训练获得了模式识别与逻辑推理能力。在数学证明中，模型能够将不同子领域的技巧进行意想不到的组合，有时产生人类数学家未曾尝试过的证明路径。这种"涌现"能力正是当前研究的核心谜题。
然而，AI 数学能力的局限同样显著。目前模型生成的数学证明长度大多在 3至4页 以内。谷歌 DeepMind 超人推理团队负责人 Thang Luong 透露，内部测试的模型已能处理更长的证明，预计很快可达到10页，但要达到 100页 级别尚需时日。与此同时，AI 生成的"看似令人信服"的数学论文正在给期刊评审带来沉重负担。哈佛大学数学家 Lauren Williams 警告，多家数学期刊编辑已经遭遇了大量 AI 生成的低质量投稿——所谓"AI 垃圾"问题日益严峻。
为应对验证难题，研究者正探索多种技术路线。一种策略是将数学证明翻译为开源形式化语言 Lean ，利用计算机自动验证逻辑正确性。北京大学计算数学家 Bin Dong 及其合作者已在一个代数问题上成功演示了这一方法。加州初创公司 Math, Inc. 则利用自动翻译工具加速了 Fields 奖得主 Maryna Viazovska 的获奖工作的 Lean 形式化进程——这是首个被完整转化为 Lean 的高影响力数学成果。谷歌 DeepMind 还开发了名为 AlphaProof 的系统，能够直接在 Lean 中生成证明；同时，其多智能体验证系统 Aletheia 内置了专门的数学文本校验模块。
小知识：什么是 Lean 形式化验证？Lean 是一种开源的形式化编程语言，能够将数学定理与证明转化为计算机可严格检查的逻辑表达式。一旦证明被成功"翻译"为 Lean 代码并通过编译，就意味着其逻辑推导在数学上是正确的。不过，目前能被 Lean 覆盖的数学范围仍然有限，扩展工作需要大量人工参与。
2026年2月，数学界对 AI 进行了一次正式"考试"—— First Proof 基准测试。各子领域专家提交了只有自己知道答案的问题，向公众征集 AI 生成的解答。结果显示，几乎所有提交的解答都使用自然语言撰写，仅一份通过了 Lean 形式化验证，部分解答经人工审核确认正确，还有一些至今无法判定对错。该基准测试的第二轮将于 2026年6月 启动，届时将集中测试公开可用的 AI 模型。Williams 作为组织者之一表示："我们希望为数学家群体提供有价值的服务。"
展望未来，Luong 提出了一个雄心勃勃的目标：希望到 2030年 ，AI 与数学家能够联合赢得 Fields 奖——数学界的最高荣誉。多数研究者认为，短期内人类数学家仍将掌握主导权，尤其在"研究什么问题"这一核心判断上。OpenAI 数学家 Mark Sellke 指出："选择问题更多是一种判断力，这在一段时间内仍将由人类来做。"卡内基梅隆大学数学家 Jeremy Avigad 则强调，即便 AI 能力持续增长，数学的终极目标仍是 人类对数学现象的理解 ，而非机器单方面宣布"定理为真"。布朗大学数学家 Javier Gómez-Serrano 感慨道："事态发展之快，我甚至不敢想象五年后会怎样。"
Reference: https://doi.org/10.1038/d41586-026-01521-z
