OpenAI 一次放出 722 篇数学手稿，含 Lean 形式化证明
发布日期：2026-10-09
事件概述
10 月 6 日，OpenAI 公开一批数学研究成果：722 份手稿，归并为 372 个成果族，全部由一个尚未发布的内部模型产出。这是继此前多次单点数学公告之后，第一次以批量仓库的形式放出。
仓库为其中部分结果附上了可被计算机检验的 Lean 形式化证明；官方同时明确警告，未经形式化的工作可能包含错误，各项成果仍处于不同的验证阶段。
核心要点
- 可机检证明的价值：形式化证明可以被独立机器验证，把「AI 说它证出来了」变成「任何人都能跑一遍确认」
- 验证是分层的：已形式化、未形式化、待核验三档并存，不能把整包当作同等可信
- 从演示到提交：科研产出从单点演示走向可被独立核验的大批量提交，检验标准同步升级
- 开放对象：仓库面向独立研究者开放核验，公开反馈将决定后续正式发布节奏
行业意义
AI 做科研的公信力之争，正在从「晒结果」转向「给检验工具」：谁能被独立核验，谁的成果才算数。