上周末，软件工程师、前量化研究员兼初创公司创始人尼尔·索马尼在测试OpenAI新模型数学能力时有了意外发现。他将问题粘贴至ChatGPT并让模型思考15分钟，返回后得到了完整解答。经评估证明过程并使用Harmonic工具进行形式化验证，结果完全正确。
“我好奇想确立一个基线，看看大型语言模型在解决开放数学问题时的有效能力与困境所在，”索马尼表示。令人惊讶的是，使用最新模型，前沿能力已开始有所推进。
ChatGPT的思维链表现尤为突出，接连列出勒让德公式、伯特兰假设及大卫之星定理等数学公理。最终，该模型找到一篇2013年Math Overflow帖子，其中哈佛数学家诺姆·埃尔基斯对类似问题给出了优雅解法。但ChatGPT的最终证明与埃尔基斯的工作存在重要差异，为传奇数学家保罗·埃尔德什提出的问题版本提供了更完整的解答。埃尔德什大量未解问题集合已成为检验人工智能能力的试验场。
对于机器智能持怀疑态度者而言，这是一个令人惊讶的结果，且并非孤例。AI工具已在数学领域变得无处不在，从以形式化为导向的大型语言模型（如Harmonic的Aristotle）到文献综述工具（如OpenAI的深度研究）。随着GPT 5.2发布——索马尼称其“在数学推理能力上据传闻优于前代版本”——已解决问题数量激增变得难以忽视，这引发了关于大型语言模型能否推动人类知识前沿的新疑问。
索马尼正在研究由匈牙利数学家提出、在线维护的超1000个埃尔德什猜想。这些问题主题和难度差异显著，是AI驱动数学研究的诱人目标。首批自主解决方案于11月出现，来自Gemini驱动的AlphaEvolve模型；而近期索马尼等人发现，GPT 5.2在处理高等数学方面表现得极为娴熟。
自圣诞节以来，埃尔德什网站已有15个问题从“开放”转为“已解决”，其中11个解决方案明确将AI模型列为参与过程的一部分。
备受尊敬的数学家陶哲轩对此进展持有更为细致的看法。他在GitHub页面上统计了八个AI模型取得有意义自主进展的问题，另有六个案例是通过定位并基于先前研究取得的。尽管距离AI系统无需人类干预即可进行数学运算尚有长路要走，但大型模型显然扮演着重要角色。
在Mastodon上，陶哲轩推测AI系统的可扩展性使其“更适合被系统地应用于那些晦涩难懂的埃尔德什问题的‘长尾’部分，其中许多问题实际上有简单的解法。”
“因此，如今这些较简单的埃尔德什问题更有可能通过纯AI方法而非人类或混合手段来解决，”陶哲轩补充道。
另一推动力是近期向形式化方向的转变。这项劳动密集型任务使数学推理更易验证和扩展。虽然形式化不依赖AI或计算机，但新一代自动化工具大幅降低了门槛。微软研究院2013年开发的开源“证明助手”Lean现已广泛用于形式化证明，而Harmonic公司的Aristotle等AI工具承诺自动化形式化工作中的大部分内容。
对于Harmonic创始人Tudor Achim而言，已解决的埃尔德什问题数量增加固然可喜，但更重要的是世界顶级数学家开始认真对待这些工具。“我更关心的是数学和计算机科学教授们正在使用AI工具，”Achim表示，“这些人有声誉需要维护，当他们公开使用Aristotle或ChatGPT时，这就是真实的证据。”