真正震撼的不是一次抛出多少论文，而是数学界第一次要同时面对机器批量产出、形式化验证和专家注意力不足。
导读：OpenAI在2026年10月6日公开了一座AI数学成果库：首发口径为722篇手稿、372个成果族，由尚未发布的内部前沿模型生成，涉及准黎曼猜想、四维挂谷、唯一游戏猜想等重量级问题。但必须先把最重要的一句话放在前面：公开手稿不等于数学结论已经被共同体确认。
先把数字说清楚：722是首发口径，仓库还在变化
OpenAI官方公告确认，这批成果来自内部前沿模型。官方仓库首发时写明722篇手稿，按相关性归并为372个成果族；模型在评估中接触约4000个开放研究问题，绝大多数结果平均消耗相当于约3小时ChatGPT Pro思考的算力。
不过仓库不是静态展览。发布后的README已经出现过手稿数量调整，并明确要求通过history查看修订。做视频网核对时，当前页面显示719篇手稿、372个成果族，并写明约42%的顶层结果完成形式化。
为什么数字会不同？“有Lean说明页的成果族”“顶层结论完成形式化”“仓库里的手稿总数”是不同指标，而且项目仍在修订、补证和更新。引用时要写明查看日期，不能把首发统计当成永久数字。
372个成果族，不是372道题的最终判决
一个成果族可能包含主结果、配套论证、推论或替代证明，因此722篇手稿并不等于独立解决了722个长期难题。仓库覆盖理论计算机科学、组合数学、代数与复几何、数论、概率、统计力学、微分几何、数学物理和算子代数等方向。
| 公开内容 | 能说明什么 | 不能自动说明什么 |
|---|---|---|
| 自然语言手稿 | 给出命题、证明路线与数学论证 | 不代表已通过同行评审 |
| Lean工件 | 检查已编码命题的形式推理 | 不保证编码命题完整对应原问题 |
| 推理摘要 | 帮助理解模型如何寻找路线 | 不是完整思维过程或独立复现 |
| 版本记录 | 追踪修正、替换和撤回 | 不能替代专家逐行审读 |
最受关注之一：准黎曼猜想的7/8零点自由区域
黎曼猜想要求非平凡零点全部落在实部为1/2的直线上。准黎曼猜想退一步，希望找到一个固定的常数θ
成果族003的手稿声称给出θ=7/8的零点自由半平面，并把结论扩展到狄利克雷L函数等对象。仓库的Lean覆盖说明列出了形式化范围，同时明确论文后续应用并未全部纳入。
这里最容易被标题误导：这不是“黎曼猜想被证明”。即使7/8结论最终成立，它证明的是更弱但仍重要的固定零点自由区域；而且仓库仍在更新，论文陈述、形式化范围和数学意义都需要领域专家核对。
另一颗重磅炸弹：四维挂谷结果仍要等专家接住
挂谷问题研究一个集合在包含所有方向单位线段时，维数和测度能有多小。仓库中的相关手稿声称推进三维挂谷极大函数问题，并处理四维豪斯多夫维数方向。
这类结果分量极重，但不能因为出现在官方仓库里就直接写成“猜想已经解决”。尤其是尚未完整形式化的部分，接下来要经过命题核对、证明逐行检查、与既有文献比较和独立复现。
还有哪些重量级“声称成果”？
- 理论计算机科学：涉及唯一游戏猜想及Max-Cut、顶点覆盖等近似难度门槛。
- 代数几何：涉及复CM阿贝尔簇上的霍奇猜想。
- 数论：涉及BSD公式的特定族、有理数域上的希尔伯特第十问题等。
- 算子代数：涉及不同秩自由群因子的同构问题。
- 其他方向：还包括π的无理性测度、马勒猜想、单位距离染色和若干反例构造。
这些标题足够惊人，但正确写法应当是“仓库中的手稿声称证明或推进”，直到相关研究者完成审读并形成稳定共识。
Lean能解决什么，又解决不了什么？
Lean可以让计算机内核检查形式化命题的每一步推理是否成立，大幅降低隐藏逻辑漏洞的风险。但它仍有三层边界：
- 命题对应：形式化的命题是否准确覆盖数学家真正关心的问题。
- 覆盖范围：论文哪些结论已经编码，哪些应用、前提或边界条件没有编码。
- 学术价值：证明是否新颖、是否正确引用前人、是否带来新的概念理解。
因此“Lean通过”不等于“论文所有内容都正确”，更不等于“已经完成同行评审”。反过来，没有Lean也不代表结果一定错误，只是验证成本更高。
神秘模型没有公布，OpenAI只给出过程线索
OpenAI没有公开模型名称，只称其为内部前沿模型，并表示正在推进负责任发布。官方同时公开了10份精简推理摘要、计算量估计和尝试问题数量。
这意味着外界目前可以检查手稿和部分形式化工件，却无法用同一模型完整复现实验。对于科学发现来说，模型访问、提示词、失败率和计算预算都是理解结果来源的重要组成部分。
为什么数学家一边兴奋，一边警惕？
当AI可以在很短时间内批量产生前沿手稿，数学界的瓶颈可能从“有没有候选证明”转向“谁有时间读懂、验证和吸收”。机器能同时跑几千个问题，但能够审读某个专业方向的专家依旧有限。
争议还包括署名、引用、抢发、未公开模型带来的访问不平等，以及实验室是否应以营销方式发布尚未被共同体理解的重大结果。
负责任发布，至少要过这三道关
第一关：机器可检查
尽可能形式化关键命题，公开覆盖范围、验证配置和可比较的挑战文件。
第二关：专家可理解
把证明写成传统数学论文能够阅读的形式，补齐相关工作、引用、动机和概念解释，并支持研讨会与阐释性写作。
第三关：共同体可追踪
提供模型、提示词、推理摘要、耗时、算力、失败率、持久标识和版本历史，修订不能悄悄覆盖旧版本。
普通读者如何查看这座仓库？
- 先读README，确认最新手稿数、成果族数和形式化比例。
- 打开overview与CONTENTS，按学科选择成果族。
- 阅读论文标题和摘要，不要只看社交媒体转述。
- 查看对应Lean说明页，确认形式化覆盖了哪些命题。
- 检查history，了解是否修订、撤回或替换。
- 等待领域专家的独立审读，不把仓库自述当成最终裁决。
做视频网观点
这次发布最值得关注的，不是“AI一天解决了多少世界难题”这种简单叙事。真正的变化是候选证明的供给开始爆发，而专家注意力、概念理解和学术治理变成新的稀缺资源。
如果其中一部分结果经得住长期审读，AI数学将从“辅助搜索”进入“批量提出可验证成果”的阶段；如果大量手稿需要修正，这个公开仓库同样有价值，因为它让外界能观察错误、修订和验证流程。最不应该做的，是在共同体还没读完前，用一个夸张标题替他们宣布胜利。
相关站内内容
OpenAI Math站内导航：https://www.zuoshipin.com/link/48387.html
OpenAI PrimeGaps186项目：https://www.zuoshipin.com/link/32209.html
GPT-6 Astra站内导航：https://www.zuoshipin.com/link/32152.html
Anthropic Formal Math站内导航：https://www.zuoshipin.com/link/48322.html
Claude形式化概率论成果解析：https://www.zuoshipin.com/article/48323
GPT-6 Astra素数间隔186解析：https://www.zuoshipin.com/article/32210
