AI模型开始攻克高难度数学问题

软件工程师、前量化研究员兼创业公司创始人Neel Somani在周末测试OpenAI新模型的数学能力时，有了意外发现。他将数学问题粘贴到ChatGPT中，让它思考15分钟后，回来时发现了一个完整的解答。他使用名为Harmonic的工具评估并形式化了这个证明，结果全部正确。

"我想确定一个基准线，了解大语言模型何时能够有效解决开放性数学问题，以及它们在哪些地方存在困难，"Somani说。令人惊讶的是，使用最新模型时，这个前沿界限开始向前推进。

ChatGPT的思维链条更加令人印象深刻，它熟练运用勒让德公式、贝特兰定理和大卫之星定理等数学公理。最终，该模型找到了一篇2013年的Math Overflow帖子，哈佛数学家Noam Elkies在其中给出了类似问题的优雅解答。但ChatGPT的最终证明在重要方面不同于Elkies的工作，并对传奇数学家保罗·厄尔德什提出的问题版本给出了更完整的解答。厄尔德什留下的大量未解问题已经成为AI的试验场。

对于任何对机器智能持怀疑态度的人来说，这是一个令人惊讶的结果，而且这并非唯一案例。AI工具在数学领域已经变得无处不在，从专注形式化的大语言模型如Harmonic的Aristotle，到文献综述工具如OpenAI的深度研究。但自GPT 5.2发布以来——Somani形容其"在数学推理方面明显比以往版本更熟练"——已解决问题的庞大数量变得难以忽视，这引发了关于大语言模型推进人类知识前沿能力的新问题。

Somani研究的是厄尔德什问题集，这是由这位匈牙利数学家提出的1000多个猜想的在线合集。这些问题已成为AI驱动数学研究的诱人目标，在主题和难度上都存在显著差异。第一批自主解答出现在11月，来自名为AlphaEvolve的Gemini驱动模型，但最近，Somani和其他人发现GPT 5.2在高级数学方面表现出色。

自圣诞节以来，厄尔德什网站上已有15个问题从"开放"状态转为"已解决"，其中11个解答明确指出AI模型参与了求解过程。

备受尊敬的数学家陶哲轩在其GitHub页面上对这一进展持更加细致的看法，他统计了8个不同的问题，AI模型在厄尔德什问题上取得了有意义的自主进展，另有6个案例通过定位和基于先前研究取得了进展。AI系统距离无需人工干预进行数学计算还有很长的路要走，但显然大语言模型可以发挥重要作用。

陶哲轩在Mastodon上推测，AI系统的可扩展性使其"更适合系统性地应用于那些鲜为人知的厄尔德什问题的'长尾'，其中许多实际上有直接的解答。"

"因此，许多较简单的厄尔德什问题现在更可能通过纯AI方法解决，而不是通过人工或混合方式，"陶哲轩继续说道。

另一个推动因素是最近向形式化的转变，这是一项劳动密集型任务，使数学推理更容易验证和扩展。形式化不需要使用AI甚至计算机，但一批新的自动化工具使这一过程变得容易得多。2013年在微软研究院开发的开源"证明助手"Lean，已在该领域得到广泛应用作为形式化证明的方法，而像Harmonic的Aristotle这样的AI工具承诺将大部分形式化工作自动化。

对于Harmonic创始人Tudor Achim来说，厄尔德什问题解答数量的突然增加不如世界上最伟大的数学家开始认真对待这些工具重要。"我更关心数学和计算机科学教授正在使用[AI工具]这一事实，"Achim说。"这些人有声誉需要保护，所以当他们说使用Aristotle或ChatGPT时，这是真实的证据。"

Q&A

Q1：GPT 5.2在数学问题求解方面有什么突破？

A：GPT 5.2在数学推理方面比以往版本更熟练，能够独立解决高难度数学问题。软件工程师Somani测试发现，该模型能够在15分钟内给出完整的数学证明，甚至解决了传奇数学家保罗·厄尔德什提出的问题，并给出比以往更完整的解答。

Q2：AI在厄尔德什问题上取得了哪些成果？

A：自圣诞节以来，厄尔德什网站上已有15个问题从"开放"状态转为"已解决"，其中11个解答明确指出AI模型参与了求解过程。数学家陶哲轩统计显示，AI模型在8个不同问题上取得了有意义的自主进展，另有6个案例通过定位先前研究取得了进展。

Q3：什么是数学形式化？AI如何改变这一过程？

A：形式化是一项使数学推理更容易验证和扩展的劳动密集型任务。开源"证明助手"Lean已在数学领域广泛应用于形式化证明，而像Harmonic的Aristotle这样的AI工具承诺将大部分形式化工作自动化，使这一过程变得更加容易。