深度 | OpenAI 甩出 722 篇数学论文，但黎曼猜想并没有被证明
OpenAI 这次放出的东西，规模大到让「读」这件事本身成了问题：722 篇手稿、372 个成果族、横跨 17 个数学方向，全部塞进github.com/openai/math一个仓库。但翻完最受关注的那几篇，你会发现一个更值得说的事：被喊得最响的「黎曼、霍奇、BSD 全上阵」，一个都没被真正证明。
上图：github.com/openai/math 仓库页面截图，2026-10-08 —— 本文所有篇数与编号均可在此仓库核对（图注日期为抓取日，仓库内容以访问时为准）。
中文媒体的标题先给这件事定了调。量子位写「黎曼霍奇BSD全上阵」，新智元跟着起哄，还有一家直接写成「准黎曼猜想已被证明」。机器之心、今日头条、投中网这三家则老实得多，标题里老老实实写着「准黎曼猜想」。这一个「准」字的差别，就是整场风波的全部。
那个「准」字，才是关键
先说被传得最神的那条。OpenAI 声称证明了：黎曼 zeta 函数和所有狄利克雷 L 函数，在 Re(s) > 7/8 的右半平面里没有零点，编号 F003，据说已经用 Lean 4 形式化；另有一篇独立证明给了更弱的 Re(s) > 11/12 版本，顺带排除了 Landau–Siegel 零点，那篇经过人工编辑重写。
而黎曼猜想要的是 Re(s) > 1/2，整条临界带。7/8 离 1/2 隔着好大一段，最难啃的区域一点没碰。所以这条结果即便全对，也只是朝黎曼猜想迈了一步。罗格斯大学的 Alex Kontorovich 在 X 上那句「如果是人做的，这就是即时菲尔兹奖」，恰恰是从反面说明问题：这个「准」字里藏着的份量，全压在一条弱化版上。
BSD 是「条件版」。F002 声称对 Selmer 群余秩 0 或 1 的椭圆曲线证明了完整的 leading-term 公式，连 Tate–Shafarevich 群有限性都包进去了；F006 则声称证明了二次扭曲下的 Goldfeld 猜想。两者一拼，覆盖的是「每个有理椭圆曲线里密度为一的那批二次扭曲」，不是任意椭圆曲线，所以完整 BSD 依旧开着，而且这两篇都没形式化。
霍奇更直接：OpenAI 证的是 CM 阿贝尔簇和 K3 曲面乘积上的有理霍奇猜想，F032，未形式化。CM 阿贝尔簇是一类对称性极高的特殊对象，离「任意光滑射影簇」的完整霍奇猜想，隔得还很远。上图：三大「全上阵」的猜想，实际证到的都是更窄、更弱的版本。
反倒是一些名气小得多的结果更值得信。机器之心和 36氪挑出的「最重 30 道名题」里，有 L=RL=BPL、唯一博弈猜想、有理数域上的希尔伯特第十问题，还有「π 的无理性测度等于 2」「卡塔兰常数是无理数」这种小而硬、且已经 Lean 形式化的结论。它们的话题性远不如黎曼霍奇，但形式化完整、容易核对，可信度反而最高。
722 篇是怎么来的，又怎么算「合格」
这批手稿都出自一个没发布、没名字的内部模型。它被投喂了约 4000 个开放问题，平均每个保留下来的结果花约 3 小时 ChatGPT Pro 级别的「思考」算力。产出之后，OpenAI 给它们的「合格证」分了档：仓库里的formalization.yaml列了 162 篇主结果经过 Lean 形式化，按成果族算约六成附了 Lean 说明页。
但几个最抓眼球的，恰好都不在形式化名单里：BSD 的 F002/F006、CM 霍奇的 F032、4D 挂谷的 F074、希尔伯特第十问题的 F004。OpenAI 自己也承认，未形式化的结果「可能包含错误」，只能算「声称」。
这里有个容易被忽略的边界：Lean 只证明「我证的那个命题成立」，不证明「那个命题就是你嘴里那个著名猜想」。机器核对的是推理内部一致，核对不了命题和原开放问题是不是一回事，这步还是得人来。所以「Lean 通过」不等于「问题解决」，尤其当模型可能把命题悄悄改弱的时候。
至于独立验证，答案是零：722 篇没有一篇经过正式同行评审，仓库关了 Issues、PR 只对协作者开放，外部没有公开质疑的入口。数学界被要求接住的，是一份七百多篇、大半未经机器校验、全部未经人工评审的「声称包」。
上图：从「声称」到「定理」，中间隔着一整条还没走完的验证链。
数学界为什么没有欢呼，只有联名信
一个月前的那桩前科，把这次的信任提前透支了。9 月 8 日，OpenAI 宣布内部模型「解决」了 Navier–Stokes 千禧年难题，约一万个智能体跑了 88 小时，结果被指出只解决了带外力的版本；克雷数学研究所没发奖，OpenAI 自己还拒领了那 100 万美元。NYU 的 Tristan Buckmaster 公开质疑 OpenAI「截胡」了他和 Anthropic 研究员 Levent Alpöge 近一年的未发表成果，OpenAI 否认。Terence Tao 把这场竞赛说成「狂热的竞争」，担心数学研究被逼进私人公司的黑箱。
带着这段前科看 722，数学界的反应就不难理解了。陶哲轩发起的公开信《人工智能在数学中的严重错位》，9 月 11 日由 25 位菲尔兹奖得主联署，邓煜、Peter Scholze 在首批，到 9 月 12 日约 2500 名学者署名。陶哲轩的比喻是把未经核验的 AI 结果批量倒出来，等于「把生肉尸骸倒在村庄公共餐桌上」；哈佛的 Curtis McMullen 则把 OpenAI 说成「发现登山者营地后，空投机械登山者抢先登顶」的人。
最克制的评价来自 MIT 的 Andrew Sutherland：在模型发布、可复现之前，这些都该视为「未验证」。挂靠普林斯顿高等研究院的 AGMAI 咨询组（成员有 Gowers、De Lellis、Hairer、Witten）给这场发布定的调是「理解的开始，而非完成」，还建议 OpenAI 停止用前沿难题给私有模型当基准，OpenAI 没听。
上图：一个月内，从单点突破到批量放出，数学界的警惕是逐步升级的。
这件事对 AI4S 意味着什么
把 722 篇放进 AI 做数学的谱系里，位置很清楚。2024 年 DeepMind 的 AlphaProof + AlphaGeometry 拿下 IMO 银牌，证明 AI 能「做对题」；今年 8 月 OpenAI 的「十道数学开放问题」只交 10 题，但每题附完整 Lean 4 证书、单题成本约 200 美元。10 月的 722 篇，是同一个策略的规模化：从「10 题加完整证书」，变成「722 篇加约六成形式化、大量未核验」。
这里藏着一个产业级的转折。AI 把「提出一个候选证明」的成本压到了 3 小时算力一个，但「判断它对不对」的成本一点没降，反而因为供给爆炸变得更稀缺。我判断，未来几年 AI-for-Math 的胜负手不在「谁的模型证得更多」，而在「谁能建立一套让数学界愿意信的验证机制」。Lean 形式化只是半套，剩下的半套（命题对应、独立复核、可复现），OpenAI 至今没交。
这条线对国内也有映射。北京 7 月印发的《AI4S 十八条》圈定了高能物理、材料、生命科学等六大领域，鼓励的是「AI 做实验、做发现」的实验范式；OpenAI 展示的是「AI 做纯数学证明」的证明范式。两条腿里，数学恰好是「可验证性」最弱的那条，这也解释了 722 的争议为什么能爆到这个程度：没有一个「跑个实验就能复现」的出口，一切都要回到逐行读证明的人。
至于那个「未发布模型」的策略，动机值得拆：不开放权重、不公开名称，却把成果全摊出来，一边用结果给模型做能力营销，一边用热度招人，再把验证成本转嫁给整个数学界。The Next Web 的标题点得最准：722 篇论文，来自一个它不肯发布的模型。
上图：AI-for-Math 的竞争重心，正在从「能不能证」转向「能不能被信」。
一个月前，我还觉得「AI 攻克千禧难题」至少得等上几年，结果 OpenAI 一下就把话题顶到了「黎曼猜想」的高度。但拆开看，这次真正被打穿的其实不是数学本身，而是证明的生产与验证分工：产出爆炸了，验证的人力一点没变多。看这类新闻，我给自己定了三问：它证的是不是完整版、有没有机器形式化、有没有人独立验过。三个里有一个是「否」，就该标成「声称」，而不是「定理」。
参考来源
- OpenAI Math — GitHub 官方仓库（一手）
- The most interesting mathematical discoveries in OpenAI’s 722 new papers — New Scientist
- OpenAI maths release: 722 papers from a model it has not released — The Next Web
- 突发！OpenAI一次放出722篇数学成果，准黎曼猜想、4D挂谷都在列 — 机器之心
- 翻完OpenAI的722篇数学手稿，我们挑出了最重的30道名题 — 36氪
- How an AI math breakthrough ignited a controversy — Science
- 陶哲轩、邓煜等25位菲尔兹奖得主联名示警 — 知乎专栏
