OpenAI 数学仓库：AI 证明、Lean 形式化与 4000 道题

一、背景：AI 生成的数学成果该怎么看

2026 年 10 月，OpenAI 在 GitHub 上公开了 openai/math 仓库。仓库里不是训练代码，也不是模型权重，而是由内部前沿模型生成的数学手稿和 Lean 形式化证明。OpenAI 的说法是，把模型在内部评估中产生的成果拿出来，让学术界共同消化。这一举动既被看作“AI 加速科学”的例证，也被质疑“把未经同行评议的结果公开”。

二、技术原理：Lean 形式化能做什么、不能做什么

仓库的核心技术栈是 Lean 4。Lean 是一种依赖类型理论（dependent type theory）的交互式定理证明语言，它可以把数学命题写成形式化代码，并让计算机检查证明的每一步是否合法。也就是说，只要 Lean 检查通过，证明在形式层面就是没有错误的。

但形式正确不等于数学上有洞见。Lean 只能验证“从 A 到 B 的推理是否严谨”，不能判断“这个定理是否重要”。一个形式正确的证明可能只是在原地打转，或者使用了已有结论的简单组合。因此，Lean 形式化的价值在于“保证不出错”，而不是“自动发现新数学”。

仓库里的手稿覆盖了谐波分析、复杂性理论、量子场论等领域。OpenAI 自述模型在评估中被提出了约 4000 个问题，仓库只放出了部分结果和形式化。换句话说，这是从大量模型输出中筛选出来的一个子集。

三、关键数据与仓库结构

从公开信息看，仓库主要包含以下内容：

• lean/ 目录：Lean 4 形式化证明。
• 数学手稿：以 PDF 或 Markdown 形式存放的模型输出。
• 推理摘要：OpenAI 公开了 10 份模型推理摘要，用于展示模型如何思考。
• 计算成本估算：以 ChatGPT Pro 使用量为单位，给出模型解题的大致成本。
• 尝试统计：记录了模型尝试问题的数量分布。

部分媒体报道称仓库包含约 722 篇数学手稿，但 OpenAI 官方并未在仓库 README 中明确这个数字，因此只能作为“据报道”的口径使用。

四、价值：它改变了什么

首先，它把 AI 生成结果的流程透明化了。过去，模型产出往往只在论文里呈现最终答案；现在，研究者可以看到原始手稿、推理过程和形式化代码。其次，它为学术界提供了一个新的“待审材料池”。数学家可以选择自己感兴趣的命题去验证，而不是被动等待发表。最后，它推动了“形式化数学”的大众化。越来越多的研究者可能会因为这套仓库接触 Lean，从而提升整个领域的形式化水平。

五、争议与风险

最大的争议在于学术署名和验证责任。OpenAI 声明不寻求学术荣誉，但这并没有解决“谁来为错误负责”的问题。如果某个被 Lean 检查通过的证明后来被数学家发现使用了不成立的前提，责任在 OpenAI、在模型、还是在验证者？

其次是可重复性问题。仓库中“由未具名的内部 OpenAI 模型”生成的结果，外人无法复现生成过程。这意味着研究者只能验证最终产物，无法判断模型是如何得到这个结果的。

第三是激励错位。形式化验证是一项耗时耗力的工作，但 OpenAI 的模式下，验证者的学术回报并不明确。长期下去，可能只有少数志愿者愿意投入。

六、结论与展望

openai/math 是一个实验性的基础设施。它展示了 AI 模型可以批量产出形式化数学内容，但也暴露了当前学术体系在接收这些内容时的制度空白。短期内，它最有价值的用途可能是作为 Lean 练习材料和研究线索。中期来看，如果 OpenAI 能公开更多生成细节和评估协议，它的可信度会大幅提升。长期来看，AI 生成成果想要被学术界接受，还需要解决署名、验证、激励和可重复性四个核心问题。否则，它更像是一个“数学结果批发市场”，而不是真正的科学共同体合作。