OpenAI 公开 719 篇数学结果：四成有 Lean 证明，第二天就撤回三篇
OpenAI 10 月 6 日在 GitHub 公开 openai/math：一个未发布的内部模型针对约 4000 个问题写出的 719 篇稿件，平均每个结果约 3 小时思考算力。其中 300 篇有 Lean 形式化证明，约占 42%；OpenAI 自己说其余的可能有问题。仓库记录显示，第二天就因符号错误撤回 3 篇、修订 14 篇。
编辑标为重要，发布已满 30 天，从立即关注降到这一档。
本页目录12 节
记录
信号正文
#发生了什么
10 月 6 日 OpenAI 发布「Sharing AI progress in mathematics」，材料放在 GitHub 仓库 openai/math：一个尚未发布的内部前沿模型在开放数学问题上的结果，连同 Lean 形式化证明与部分推理摘要。OpenAI 官网页面对抓取返回 403，本条的数字来自仓库的 README、history.md 与 lean 目录说明。
规模与可核验的部分
- 约 4000 个问题交给内部模型，产出 719 篇稿件，分为 372 个家族
- 平均每个结果约用了 ChatGPT Pro 档 3 小时的思考算力
- 300 篇（约 42%）的主结果有 Lean 形式化证明，按仓库说明可以用 Comparator 校验
- OpenAI 明说：没有形式化的结果「可能有问题」
也就是说，近六成的结果目前只能靠人读。可核验的那四成，才是这批材料最可靠的部分。
例外与亮点
仓库列出两项不按标准流程处理的结果：黎曼 ζ 函数在 Re(s) > 11/12 上的无零点区域（文稿经过人工编辑），以及 CM 阿贝尔簇上的 Hodge 猜想。另有 10 个家族公开了删节的推理摘要，包括 π 的无理性指数、Mahler 猜想、特征 2 下 Kaplansky 直接有限性等。
量子位称这批结果涉及「又三个千禧年难题」，但仓库里能看到的标题都是部分情形或特殊情形，例如 CM 阿贝尔簇上的 Hodge 猜想、从低 Selmer 余秩出发的 BSD。本站不采用这一说法。
第二天就开始更正
仓库的更正记录显示，10 月 7 日因一个符号错误撤回了 3 篇稿件，其中包括《K3 曲面乘积的有理 Hodge 猜想》，另有 14 篇被修订。这说明两件事：公开材料确实在被检查，而没有形式化证明的结果需要按「待核验」对待。
同一周，据量子位报道，包括陶哲轩在内的 25 位菲尔兹奖得主联名批评把数学当作 AI 基准。
对读者意味着什么
- 读这类成果时，先分清哪些有机器可检的证明、哪些没有。这批材料自己就给出了比例：42% 对 58%。
- 「解决某某猜想」的标题要回到仓库看具体是哪个情形。
- 3 小时一个结果的算力，说明这还不是普通用户能复现的能力，而是内部模型在大算力下的产出。
为什么是现在
为什么重要
#这是迄今规模最大的一次模型数学成果公开，而且附带了能机器核验的那一部分。它同时给出了一个读这类新闻的标尺：只有 42% 有形式化证明，第二天就撤回了 3 篇。
背景
技术背景
#Lean 是一种定理证明器：用它写下的证明可以由计算机逐步检查，不依赖人去读。形式化覆盖率低，意味着其余结果仍要靠数学家审阅。千禧年难题是克雷研究所列出的七个问题，解决部分情形与解决原问题不是一回事。
关注人群
谁该关注
#下一步
学习路径
#- 先读本站 9 月 8 日的纳维-斯托克斯信号，看上一次类似成果的争议在哪里
- 读本站菲尔兹奖得主 Gowers 的信号，了解数学家认为模型强在哪、弱在哪
- 打开 openai/math 仓库，任选一个有 Lean 证明的结果，看它到底证了什么
- 读《人在回路的审查》，想清楚没有形式化的那 58% 该由谁、怎样审
关系网络
在技术网络中的位置
#当前技术与相邻技术、技能和背景知识的连接，点击节点可继续探索。
延伸思考
后续问题
#- 300 篇有 Lean 证明的结果里，有多少是新结论，有多少是已知结论的新证明？
- 撤回的 3 篇是怎么被发现的？是人读出来的，还是形式化时暴露的？
- 如果你的领域也有形式化工具，模型产出的结果有多少能被机器检查？
发布记录
收录于
#收录这条信号的技术简报，新的在前；最后一行是它那一周的周回顾。标签是它在那一期所在的栏目。
来源参考