Sharing AI progress in mathematics
OpenAI publishes new results on open problems in mathematics from an internal frontier model and shares Lean proof formalizations and research details on GitHub.
Marked important, but published more than 30 days ago, so it moved down to this band.
On this page12 sections
The full write-up and the editors' notes are in Chinese; the summary above is from the original announcement.
Record
The signal
#发生了什么
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 小时一个结果的算力，说明这还不是普通用户能复现的能力，而是内部模型在大算力下的产出。
Why now
Why it matters
#这是迄今规模最大的一次模型数学成果公开，而且附带了能机器核验的那一部分。它同时给出了一个读这类新闻的标尺：只有 42% 有形式化证明，第二天就撤回了 3 篇。
Background
Technical context
#Lean 是一种定理证明器：用它写下的证明可以由计算机逐步检查，不依赖人去读。形式化覆盖率低，意味着其余结果仍要靠数学家审阅。千禧年难题是克雷研究所列出的七个问题，解决部分情形与解决原问题不是一回事。
Audience
Who should care
#Next
Learning path
#- 先读本站 9 月 8 日的纳维-斯托克斯信号，看上一次类似成果的争议在哪里
- 读本站菲尔兹奖得主 Gowers 的信号，了解数学家认为模型强在哪、弱在哪
- 打开 openai/math 仓库，任选一个有 Lean 证明的结果，看它到底证了什么
- 读《人在回路的审查》，想清楚没有形式化的那 58% 该由谁、怎样审
Network
Where it sits in the network
#How this signal connects to neighbouring technologies, skills and background knowledge. Follow any link to keep exploring.
Further thought
Follow-up questions
#- 300 篇有 Lean 证明的结果里，有多少是新结论，有多少是已知结论的新证明？
- 撤回的 3 篇是怎么被发现的？是人读出来的，还是形式化时暴露的？
- 如果你的领域也有形式化工具，模型产出的结果有多少能被机器检查？
Publication record
Featured in
#The briefings that carried this signal, newest first; the last row is the weekly review of its week. The tag is the section it ran in.
技术简报 - 2026-10-08
Immediate attentionWeekly review · Oct 5 – Oct 11
Worth tracking
Sources