Large models begin to "batch solve" mathematical problems

人工智能在数学领域的突破正在加速。自圣诞节以来，著名数学家保罗·埃尔德什遗留的 1000 多道未解难题中，已有 15 道从"未解决"状态转为"已解决"，其中 11 道明确标注 AI 模型参与了求解过程。这一进展标志着大语言模型在推进人类知识前沿方面展现出前所未有的能力。

据 TechCrunch 周四报道，OpenAI 最新发布的 GPT 5.2 模型在数学推理能力上实现显著提升。软件工程师、前量化研究员 Neel Somani 在测试中发现，该模型能够在 15 分钟内给出完整的数学证明，并通过形式化工具 Harmonic 验证无误。这一表现远超此前版本，使 AI 工具从辅助角色转向能够独立攻克高难度数学问题的新阶段。

菲尔兹奖得主陶哲轩在其 GitHub 页面上统计，AI 模型已在 8 道不同的埃尔德什问题上取得实质性自主进展，另有 6 例通过定位和扩展先前研究实现突破。尽管距离完全自主的数学研究仍有距离，但大模型在数学领域的作用已不容忽视。

这一进展对数学研究生态和 AI 应用市场均产生直接影响。形式化工具如微软研究院开发的开源证明助手 Lean，以及 Harmonic 公司的 Aristotle 等 AI 工具，正在被顶尖数学家和计算机科学教授广泛采用，预示着学术研究工作流程的深刻变革。

从意外发现到系统性突破

Somani 的发现始于一次常规测试。他将一道数学难题输入 ChatGPT，让模型思考 15 分钟后，返回了一个完整解答。该证明引用了勒让德公式、伯特兰假设和大卫之星定理等数学公理，最终找到了哈佛大学数学家 Noam Elkies 在 2013 年 Math Overflow 论坛上发布的类似问题的优雅解法。但 ChatGPT 的最终证明在关键方面与 Elkies 的工作有所不同，并给出了埃尔德什问题某个版本的更完整解答。

"我想建立一个基准，了解大语言模型何时能够有效解决开放数学问题，以及它们在哪些方面仍有困难，"Somani 表示。令人意外的是，使用最新模型后，这一前沿界限开始向前推进。

埃尔德什问题集包含超过 1000 个猜想，由这位匈牙利数学家提出并在线维护。这些问题在主题和难度上差异显著，已成为 AI 驱动数学研究的诱人目标。首批自主解决方案于去年 11 月由 Gemini 驱动的 AlphaEvolve 模型产生，但最近 GPT 5.2 在高级数学方面表现得更为出色。Somani 将其描述为"在数学推理方面比以前的版本更熟练"。

顶尖数学家的审慎评估

陶哲轩对这一进展持更为细致的看法。他在 Mastodon 上推测，AI 系统的可扩展性使其 “更适合系统性地应用于那些不为人知的埃尔德什问题的'长尾'，其中许多实际上有直接的解决方案”。

"因此，许多较简单的埃尔德什问题现在更有可能通过纯 AI 方法解决，而非人类或混合方式，"陶哲轩补充道。

这一评估揭示了 AI 在数学研究中的定位：并非取代人类数学家处理最前沿的复杂问题，而是高效处理大量中等难度、但因人力有限而长期未被关注的问题。这种分工可能重塑数学研究的资源配置。

形式化工具推动应用落地

另一个关键驱动因素是数学界近期向形式化的转变。形式化是一项劳动密集型任务，能使数学推理更易于验证和扩展。虽然形式化不必依赖 AI 或计算机，但新一代自动化工具大幅降低了工作难度。

微软研究院 2013 年开发的开源"证明助手"Lean 已在该领域广泛使用，而 Harmonic 公司的 Aristotle 等 AI 工具承诺将形式化工作的大部分自动化。

Harmonic 创始人 Tudor Achim 认为，埃尔德什问题解决数量的突然增加不如顶尖数学家开始认真对待这些工具更重要。“我更关心数学和计算机科学教授正在使用这些 AI 工具，” Achim 表示，“这些人需要保护自己的声誉，所以当他们说使用 Aristotle 或 ChatGPT 时，这是真实的证据。”

这一趋势表明，AI 工具已从实验阶段进入学术界的主流应用，可能为相关技术公司开辟新的商业机会，同时也对传统数学研究方法论提出挑战。