OpenAI公开722份AI数学手稿：机器给出的证明，由谁来验证

2026年10月25日讯 10月6日，OpenAI在GitHub上公开了一批由其内部前沿模型生成的数学研究成果，共722份手稿，按主要结果和相关论证、推论或替代证明归为372个结果族，其中不少证明附有Lean语言的形式化版本。据报道，平均每个结果大约用了相当于三小时的ChatGPT Pro思考时间。由于生成这些成果的模型尚未对外发布，外界暂时无法复现生成过程，它们的正确性和新颖性需要领域专家独立验证。

这件事为什么引起数学界关注？

数学是对正确性要求最严格的学科之一。一个证明只要有一处漏洞，整个结论就站不住。过去AI在数学上的成绩多体现在竞赛题上，而这一次公开的是研究级别的结果，并且数量很大。数量大带来一个现实问题：谁来逐一审查？传统的同行评审依赖少数专家投入大量时间，面对几百份手稿，审查能力本身就成了瓶颈。

这也是人们屡屡提到形式化证明的原因。这些用Lean等证明助手写成的证明，可以被计算机一步步地检查，减轻人工负担。但形式化并不能回答这个结果是重要的还是无关紧要的，是前人没有做过的还是重复劳动，这些都需要懂行的人来判断。

证明的每一步都要经得起检查，无论出自谁手（插画）

对普通研究生有什么启发？

大多数研究生不做前沿数学，但这件事也告诉我们一个道理：AI生成的东西，必须有办法验证。对使用AI编写代码的同学而言，验证即利用原始数据重新计算关键数值；对使用AI整理文献资料的同学而言，验证即逐条查阅原文进行核对；对使用AI推导公式的学生而言，验证即自行推导或采用其他方法进行交叉验证。

这也是PaperOK科研助手在设计上强调“过程可查、结果可复现”的原因。智能体在本机直接调用Python或R环境运行代码，每一步做了什么都能展开查看，脚本可以保存下来复现。官网案例中，一次方法章节写作任务输出了19个编号公式和7张表，全文165处公式都是Word原生公式，还另派代理独立复算了208个数值。复算本身就是一种验证。

结论可信，靠的是可以追溯的引用和可以复现的计算（插画）

验证的责任在谁？

无论工具多强，结果的责任都在使用它的研究者身上。OpenAI也表示会继续补充形式化内容，并资助围绕AI生成成果的研讨活动，这本身说明，成果要被学界接受，必须经过独立的检验。对学生来说，在论文中使用AI生成的推导、代码或数据分析时，如实说明使用方式和验证过程，既是学术规范的要求，也是对自己研究质量的保障。

常见问题

问：Lean是什么？

Lean是一个交互式定理证明和编程工具，允许将数学证明编码为计算机可以逐步验证的形式。

问：用AI推导的公式能直接写进论文吗？

不建议直接使用。应自行推导验证或使用数值方法交叉验证，并按学校或期刊的要求说明AI使用情况。