4000个数学问题、372个结果家族、722篇手稿——OpenAI正在展示一种新的可能：人工智能不只是帮助人类解数学题，而开始尝试参与数学研究。

近日，OpenAI发布了最新的数学研究进展，并在GitHub上公开了一批由其内部前沿模型探索产生的数学成果。

这次公布的数字颇为惊人：OpenAI表示，他们让AI针对约4000个开放数学问题进行探索，最终整理出372个数学结果家族、722篇数学手稿。部分成果还进一步使用Lean进行了形式化验证。

不过，这并不意味着“AI解决了722个数学难题”。真正值得关注的，是背后正在发生的变化。

从“做题”到“做研究”

过去几年，人工智能在数学领域的表现不断提升。

最初，它主要解决计算题和竞赛题；随后开始证明复杂定理，并在IMO等高难度数学任务中取得突破。

但“解题”和“科研”仍然存在很大区别。

一道数学题通常已经知道问题是什么，只需要找到答案。

而真正的数学研究则是：

发现问题 → 提出猜想 → 寻找思路 → 建立证明 → 验证结果。

这一次，OpenAI尝试让AI面对的正是大量尚未解决的开放问题。

也就是说，AI不再只是回答：

“这道题怎么做？”

而开始尝试回答：

“这里有没有一个人类还没有发现的数学结果？”

这或许才是此次发布最值得关注的地方。

4000个问题，为什么最终只有372个“结果家族”？

这里也需要特别澄清。

OpenAI公布的722篇手稿，并不等于722项重大数学突破。

这些手稿包含不同的证明、推论和相关结果，OpenAI最终将它们归纳为372个“结果家族”。

而且，这些结果处于不同的验证阶段。

部分结果已经使用Lean进行了形式化验证，但并不是全部。

因此，更准确的理解应该是：

OpenAI公开了一批由AI探索产生的数学研究成果，其中一些已经获得机器形式化验证，还有一些仍然需要数学界进一步检查和评价。

这与“AI已经独立解决数百个重大数学难题”显然是两回事。

Lean：给AI数学证明装上一把“验算尺”

这次发布中，一个特别值得关注的关键词是Lean。

Lean是一种形式化数学系统，可以让计算机逐步检查一个数学证明是否符合严格的逻辑规则。

传统数学论文中经常出现：

“显然……”

“容易得到……”

“由此可知……”

这些对于数学家而言通常没有问题，但对于AI来说，却可能隐藏着逻辑漏洞。

而如果一个证明能够被Lean完整形式化，那么计算机就可以逐步检查它。

于是，一条新的AI数学研究路线逐渐形成：

AI提出想法

↓

AI寻找证明

↓

AI写出数学结果

↓

AI将证明形式化为Lean

↓

计算机验证证明

这实际上解决了AI做数学时最令人担心的问题之一：

AI说得很漂亮，但到底对不对？

AI正在变成一个“数学研究团队”

OpenAI此次还有一个非常值得注意的地方，就是计算规模。

面对一个数学问题，人类数学家可能需要几天、几个月甚至几年寻找思路。

AI则可以采取完全不同的方式：

让大量Agent同时探索不同方向。

有的尝试代数方法，有的尝试几何方法，有的寻找反例，有的修改已有定理，有的负责检查证明，最后再把不同路线汇总起来。

这意味着，未来的数学研究可能出现一种全新的工作模式：

一个数学家提出研究方向，成百上千个AI Agent负责并行探索。

数学家的角色，也可能逐渐从“亲自完成每一步证明”，转向：

提出重要问题、判断研究方向、筛选AI产生的结果，并理解这些结果意味着什么。

这不仅仅是数学领域的事情

为什么OpenAI如此重视数学？

因为数学是检验AI“真正推理能力”的一个极好领域。

数学研究需要：

• 长时间推理；
• 多步骤规划；
• 抽象概念理解；
• 自我纠错；
• 工具调用；
• 程序编写；
• 结果验证；
• 发现新的规律。

因此，一个能够自主探索数学问题的AI，未来并不一定只会“做数学”。

它可能进一步进入：

物理、化学、生物学、材料科学和医学研究。

例如在生命科学中，未来完全可能出现这样的科研流程：

AI阅读海量论文

↓

发现已有研究中的矛盾和空白

↓

提出新的科学假说

↓

设计计算和实验方案

↓

分析实验数据

↓

寻找新的机制

↓

形成论文

↓

交给人类科学家和实验进行验证

如果这一过程最终能够稳定运行，那么AI带来的变化就不再只是“提高科研效率”，而可能是：

改变科学发现本身的生产方式。

但现在还不能说“AI已经成为数学家”

这次成果令人兴奋，但同样需要保持冷静。

第一，722篇手稿不等于722项重大突破。

第二，部分结果尚未完成完整的形式化验证。

第三，一个数学结果即使正确，也未必具有重要的数学意义。

数学研究不仅需要证明一个命题，更重要的是判断：

什么问题值得研究？

这个结果为什么重要？

它是否打开了一个新的研究方向？

这些能力目前仍然很难完全交给AI。

因此，现在更准确的说法不是：

“AI已经取代数学家。”

而是：

AI正在从数学工具，逐渐成为数学研究的参与者。

从“AI解题”到“AI发现”

如果把近几年AI数学的发展放在一起看，会发现一条非常清晰的路线：

AI做数学题

↓

AI证明数学定理

↓

AI解决开放问题

↓

AI提出新的数学结果

↓

AI利用Lean进行形式化验证

↓

AI参与数学研究

这条路线最值得关注的，并不是某一个具体的数学定理。

真正值得关注的是：

人工智能第一次开始大规模尝试进入“知识生产”的环节。

过去，计算机主要负责计算。

后来，AI开始负责分析。

现在，AI正在尝试发现。

如果未来人类能够确认这些AI产生的结果中，持续出现真正重要、原创并能够推动数学发展的成果，那么我们面对的就不仅仅是一次模型升级。

而可能是：

科学研究方式的一次改变。

4000个问题只是开始。

372个结果家族也许只是早期样本。

真正值得期待的问题是：

下一次，人类会不会发现一个数学领域的重要新定理，是AI首先想到的？

如果答案最终是“会”，那么“AI科学家”就不再只是一个科幻概念，而可能成为未来科研体系中的一种新角色。

https://github.com/openai/math/tree/main