周末的一次测试中，软件工程师、前量化研究员兼创业公司创始人 Neel Somani 在检验 OpenAI 新模型的数学能力时，发现了一个出乎意料的结果。他将一道开放数学问题粘贴进 ChatGPT，设置“思考”约 15 分钟后返回，看到的是一份完整的证明。Somani 随后对该证明进行评估，并借助名为 Harmonic 的工具完成形式化验证，结果显示证明正确无误。

Somani表示，他的初衷是想了解大型语言模型（LLM）在解决开放数学问题时的“有效起点”以及其薄弱环节。但在使用最新模型时，他认为这一前沿方向已经出现突破迹象。

在这次尝试中，ChatGPT 展示出的推理链条同样引人关注。Somani称，该模型能够流畅调用多种数学公理和结果，包括勒让德公式、贝特朗猜想以及“大卫之星定理”等。最终，模型在推理过程中找到了哈佛数学家 Noam Elkies 于 2013 年在 Math Overflow 上的一篇帖子，其中给出了一个类似问题的优雅解法。不过，ChatGPT 给出的最终证明在若干关键点上与 Elkies 的处理方式并不相同，并对传奇数学家保罗·埃尔德什提出的某一版本问题给出了更为完整的解决方案。埃尔德什提出的大量未解难题，近年来正逐步成为人工智能系统的试验场。

类似案例并非孤例。多种人工智能工具已在数学研究中被广泛使用，从以形式化为导向的 LLM（如 Harmonic 的 Aristotle），到用于文献检索和综述的工具（如 OpenAI 的 Deep Research）。Somani提到，自 GPT 5.2 发布以来——他称该版本“在数学推理方面据传比之前版本更为娴熟”——被解决的问题数量明显增加，难以忽视。这一现象也引发了关于大型语言模型是否正在推动人类知识边界的新讨论。

Somani 目前重点关注的是“埃尔德什问题集”——一个在线维护的题库，收录了匈牙利数学家保罗·埃尔德什提出的 1000 余个猜想。这些问题在主题和难度上差异巨大，被视为人工智能参与数学研究的理想试验对象。首批由人工智能自主给出的解决方案出现在去年 11 月，当时一个由 Gemini 驱动、名为 AlphaEvolve 的模型给出了解答。近期，Somani 和其他研究者则观察到，GPT 5.2 在处理高阶数学问题方面表现突出。

根据公开信息，自去年圣诞节以来，埃尔德什问题网站上已有 15 个问题的状态从“开放”变为“已解决”，其中 11 个解答明确提及人工智能模型参与其中。

在数学界，相关进展也受到顶尖学者关注。数学家陶哲轩在其 GitHub 页面上对这些成果进行了更为细致的归类。他统计称，目前已有 8 个案例中，人工智能模型在埃尔德什问题上取得了“实质性自主进展”；另有 6 个案例则主要依靠模型定位并利用既有研究成果取得突破。陶哲轩认为，距离完全无需人类干预的“全自动”数学研究仍有相当距离，但大型模型已经在其中扮演了重要角色。

陶哲轩在社交平台 Mastodon 上推测，人工智能系统的可扩展性，使其“更适合系统性地应用于那些晦涩的埃尔德什长尾问题，其中许多实际上有直接的解决方案”。他进一步表示，因此许多相对简单的埃尔德什问题，如今“更有可能通过纯人工智能方法解决，而不是依赖人类或人机混合方式”。

推动这一趋势的另一个重要因素，是数学界近年来对“形式化”的重视。形式化旨在将数学证明转化为可由计算机严格检查的形式，这一过程传统上耗时耗力，但有助于提高推理的可验证性和可扩展性。形式化本身并不必然依赖人工智能或计算机，但新一代自动化工具显著降低了相关门槛。

由微软研究院在 2013 年推出的开源“证明助手” Lean，已在数学界被广泛用于证明的形式化工作。而以 Harmonic 的 Aristotle 为代表的人工智能工具，则宣称可以自动化完成其中的大部分步骤。

在 Harmonic 创始人 Tudor Achim 看来，相比埃尔德什问题解决数量的突然上升，更值得关注的是世界顶尖数学家开始认真使用这些工具。他表示，自己“更在意的是数学和计算机科学教授们正在使用这些工具”。Achim指出，这些学者需要维护自身声誉，“所以当他们公开表示使用 Aristotle 或 ChatGPT 时，这本身就是一种有分量的证据”。