根据软件工程师和前量化研究员进行的测试，OpenAI 的最新模型在解决高级数学问题方面表现出了意想不到的能力 尼尔·索马尼。 Somani 观察到该模型在处理 ChatGPT 中的问题 15 分钟后生成了完整的解决方案，随后使用 Harmonic 工具形式化了证明，确认了其准确性。他表示，他的目标是为大型语言模型（LLM）解决开放数学问题的能力建立基线。该模型的思想链引用了数学公理，包括勒让德公式、伯特兰公设和大卫之星定理。它找到了哈佛大学数学家 Noam Elkies 在 2013 年发表的 Math Overflow 帖子，该帖子提供了类似问题的解决方案，但 ChatGPT 的最终证明有所不同，并为数学家 Paul Erdős 提出的问题版本提供了更完整的解决方案。自 GPT 5.2 发布以来，Somani 称其“据称比之前的版本在数学推理方面更加熟练”，越来越多的已解决问题引发了人们对法学硕士提升人类知识能力的质疑。 Somani 专注于 Erdős 问题，这是在线维护的 1000 多个猜想的集合，这些猜想的主题和难度各不相同。 11 月份，由 Gemini 驱动的模型 AlphaEvolve 出现了针对这些问题的第一个自主解决方案。最近，Somani 和其他人发现 GPT 5.2 擅长高级数学。自 12 月以来，Erdős 网站上的 15 个问题已从“开放”转变为“已解决”，其中 11 个解决方案归功于人工智能模型。数学家陶哲轩在他的 GitHub 页面指出了人工智能模型取得有意义的自主进展的八个问题以及涉及定位和建立先前研究的六个案例。陶在 Mastodon 上推测，人工智能系统的可扩展性使它们“更适合系统地应用于晦涩的 Erdős 问题的‘长尾’，其中许多问题实际上都有简单的解决方案”，并补充说，“许多更简单的 Erdős 问题现在更有可能通过纯粹基于人工智能的方法来解决，而不是通过人类或混合手段来解决。”这一进步的驱动力是向形式化的转变，这是一个验证和扩展数学推理的劳动密集型过程。虽然不需要人工智能，但新的自动化工具简化了这一过程。微软研究院于 2013 年开发的开源证明助手 Lean 已广泛用于形式化证明，而 Harmonic 的 Aristotle 等人工智能工具旨在实现大部分工作的自动化。 Harmonic 创始人 Tudor Achim 表示，数学家和计算机科学教授与人工智能工具的接触比解决 Erdő 问题的数量更重要。阿希姆说：“这些人有声誉需要保护，所以当他们说他们使用亚里士多德或他们使用 ChatGPT 时，这是真正的证据。”
