OpenAI 公开 AI 做数学的结果，附 Lean 证明

数学论文最难骗人的地方在于，证明摆在那里，同行可以一行一行看。现在 OpenAI 把一批由模型产出的数学结果交了出来，还附带计算机能直接验的 Lean 版本。

一、发生了什么

10 月 6 日，OpenAI 发布《Sharing AI progress in mathematics》，10 月 15 日做了更新。文章说，公司把一批由内部前沿模型得到的新数学结果放到了公开的 GitHub 仓库，同时公开三类过程信息：10 份模型推理摘要、按 ChatGPT Pro 用量估算的算力消耗、尝试过的题目数量统计。

算力口径值得一提。OpenAI 说，平均每个结果消耗的计算量，大致相当于 ChatGPT Pro 连续思考三个小时。这个说法比"某个跑分涨了多少"更能让人判断成本。

发布方式不是自己拍板。OpenAI 说它咨询了普林斯顿高等研究院的"数学与人工智能顾问组"（AGMAI），并依据该小组 9 月 29 日的公开建议来安排披露方式。配套动作是钱：OpenAI 向西蒙斯基金会的一项新计划出资 500 万美元，该计划总规模 1500 万美元，用来支持数学家审核、理解并在 AI 结果上继续工作，包括工作坊和会议。

文章没有给出具体定理名称，也没有列任何基准测试分数。这一点很关键——它说明发布重点是"结果本身可被检查"，而不是"我们又拿了个第一"。

二、跟你有什么关系

做研究的人。 多了一类需要处理的稿件：不是人写的，但证明能过机器检查。审稿流程里迟早要加一问——这个结论是模型给的，谁负责核对？

学数学的学生。 Lean 形式化会变成一项实用技能。能读懂、能改写形式化证明的人，比只会用聊天框问答案的人更容易参与这类工作。

普通读者。 看到"AI 解决了某数学难题"这种标题时，先找三样东西：原始仓库、形式化证明、同行评议。三样缺两样，就先当成进展报告，别当成结论。

三、怎么判断

1. 先看有没有可运行的证明。Lean 能编译通过，至少排除了低级错误；编译不过，剩下的话都不用谈。
2. 再看问题本身有没有被重新表述。模型常常"解决"的是一个被简化过的版本，原问题还在。
3. 查算力成本。三个小时的 Pro 思考换一个结果，意味着这类产出目前还不能批量复制。
4. 看谁做了审核。有数学家独立复核，和只有模型自评，性质完全不同。
5. 留意引用与署名规范。OpenAI 自己说要改进论文修订和引用协议，说明这块此前并不成熟。

四、三个别信的说法

"AI 已经能独立做数学研究了。" 更准确的说法是：模型能在人类给出的方向上产出候选结果，再由形式化工具和人类检查。提出猜想、判断什么问题值得做、发现证明里的关键一步，这些仍然高度依赖人。

"有 Lean 证明就等于数学界认可。" 形式化只保证"从公理到结论的推导没有漏洞"，不保证这个东西重要、新颖，也不保证它回答的是原来那个问题。机器验证是必要条件，不是充分条件。

"OpenAI 顺手解决了纳维-斯托克斯问题。" 那是同一站点上另一篇 9 月 8 日的文章，标题用的是"提出一个解法"。这类标题在传播中很容易被压缩成"解决了"。看到时，回到原文看一眼动词。

五、一句话结论

这一批成果真正的价值不是"AI 会做数学了"，而是"AI 的数学产出第一次变得可以被逐行检查"。

信息来源

• OpenAI：Sharing AI progress in mathematics（2026 年 10 月 6 日发布，10 月 15 日更新）

功能与价格以官方公告为准。本文写于 2026 年 10 月 18 日。