OpenAI 公开前沿模型数学研究成果，发布 722 份手稿与 Lean 形式化证明

OpenAI 在其官方博客发布题为 Sharing AI progress in mathematics 的文章，公开了一批针对数学开放问题的新研究成果。这些结果来自公司内部的一个前沿模型，而非已对外发布的商用模型。

与以往只给出答案不同，OpenAI 这次同步公开了研究的原始材料。博客称，公司发布了 722 份数学手稿，并附上 Lean 证明形式化（formalization）以及相关研究细节，全部托管在 GitHub 上供外界查阅。

Lean 是一种交互式定理证明器，把数学证明写成机器可逐行检查的形式。把结论翻译成 Lean 代码，意味着证明的正确性可以被计算机验证，而不只依赖人工同行评审。围绕这批手稿的讨论，也主要集中在机器能否生成可验证证明这一点上。

值得注意的是，产出这些结果的模型并未对外发布。OpenAI 将其描述为内部前沿模型，这延续了前沿实验室先在小范围内验证模型能力、再决定是否公开的常见做法。

对数学界而言，这批材料同时具备两重价值：一是开放问题本身的结果，二是可供复现和二次研究的形式化代码。研究者可以在 GitHub 上直接检查证明流程，判断哪些环节成立、哪些仍需补强。

对 AI 行业而言，这件事的意义在于把模型会做题推进到模型能给出可被机器验证的推理。数学长期被视为检验模型推理能力的试金石，而形式化证明比自然语言解答更难含糊过关。

接下来值得观察的是，这批手稿会得到数学界的多少实质反馈，以及 OpenAI 是否会公开模型本身或更多技术细节。若形式化证明被广泛复现，相关方法也可能外溢到软件验证、芯片设计等需要严格推理的领域。