OpenAI 发布内部前沿模型数学研究成果，并公开 Lean 形式化证明
OpenAI 把「AI 做数学」摆上了台面
OpenAI 近日发布了一批由内部前沿模型生成的数学成果，针对的是数学领域中的开放问题。与以往只公布结论不同，这次 OpenAI 选择把论文、证明细节和研究过程一并放到 GitHub 仓库中，并附上 Lean 形式化证明，让计算机可以逐行验证推理是否正确。
对于长期关注 AI for Science 的人来说，这一动作的意义不只是「模型又解了几道题」，而是披露方式本身正在成为议题。
不只是给答案，还要给「怎么来的」
OpenAI 在公告中特别提到，他们与普林斯顿高等研究院（IAS）的数学与人工智能咨询委员会进行了沟通，参考了该独立小组的公开建议，才确定这次的发布规范。仓库中不仅有结果本身，还包含：
- 10 份模型推理过程摘要，展示模型如何逼近问题；
- 以 ChatGPT Pro 使用量折算的算力估算；
- 尝试过的问题数量等统计数据。
其中一个值得注意的数字是：平均每个结果消耗的算力，大约相当于 ChatGPT Pro 思考三个小时。这为外界理解「AI 做数学」的成本提供了一个可参照的锚点。
Lean 形式化：让证明可被机器检查
此次发布的另一重点是 Lean 形式化。Lean 是一门专门用于数学证明的编程语言，证明写完后可由计算机自动核验，减少人工审稿中可能出现的疏漏。OpenAI 表示，仓库中的形式化证明会随着后续工作持续补充。
这实际上回应了数学界对 AI 生成证明的一大疑虑：结论看起来对，但推理链条是否严密？ 形式化验证虽然不能替代数学直觉和审美，但至少提供了一条可复核的技术路径。
从「发结果」到「建机制」
OpenAI 还宣布将资助一系列研讨会、会议和特别项目，围绕如何理解 AI 产出的重大数学结果展开讨论，并承诺未来会继续改进论文的引用规范、数学表述和呈现方式。
更值得关注的是最后一句：OpenAI 表示正在负责任地发布产生这些结果的模型。这意味着当前公开的只是研究成果，而模型本身尚未对外开放。对于数学界和 AI 研究者而言，这既是一个信号——能力已经存在，也是一个悬念——何时能用上、以什么形式用上，仍是未知数。
AI 与数学的交叉正在从「能不能做」转向「做了之后怎么办」：如何验证、如何署名、如何引用、如何让社区真正受益。OpenAI 这次的 GitHub 发布，更像是一次面向学术界的流程试探，而非单纯的能力展示。
