REPORT & INSIGHTS

“数学末日”:OpenAI 生成数百项数学成果,但谁能理解这些证明?

“数学末日”:OpenAI 生成数百项数学成果,但谁能理解这些证明?

OpenAI 一次性公开数百份由内部前沿模型生成的数学手稿,将 AI 数学能力推到了一个新的争议点:如果机器能够比人类审阅更快地生产定理与证明,数学知识究竟是在增加,还是正在形成一个几乎无人真正理解的“证明仓库”?

这次事件被部分媒体称为 “Mathocalypse(数学末日)”。它并不是说数学即将终结,而是指传统研究流程可能出现失衡:AI 可以持续生成大量候选结果,形式化工具可以验证其中部分代码,但人类数学家仍需要逐项确认命题是否有意义、书面论证是否忠实、成果是否真正新颖,以及它与现有理论的关系。

为什么数字从 722 变成了 719

OpenAI 在 10 月 6 日最初发布了 722 份手稿,组成 372 个相互关联的研究系列。一天后,公司发现其中一篇代数几何手稿存在符号错误,该错误破坏了一个关键抵消论证,并影响另外两篇依赖该构造的手稿。

OpenAI 随后撤回这 3 篇手稿,因此当前统计变为 719 份。同一次更新还修订了另外 14 篇手稿,并调整了 13 篇相关论文的引用或版本记录。

这次快速纠错说明公开仓库和版本历史确实发挥了作用,但也证明“模型生成”不能直接等同于“成果已成立”。OpenAI 自己也承认,尚未形式化的结果可能存在问题,并表示会继续修订和补充验证材料。

Lean 验证了什么,又没有验证什么

截至 10 月 7 日,719 项主要结果中有约 300 项拥有 Lean 形式化证明,占比约 42%。Lean 会把数学命题、定义和推理步骤转换为严格的形式语言,再由内核检查每一步是否符合逻辑规则。

如果命题被正确表达、所用公理与定义合理,并且 Lean 代码成功通过检查,那么这份形式化证明具有很强的逻辑保障。但这里存在一个关键前提:Lean 验证的是写进代码里的命题与证明,并不会自动证明自然语言论文被准确翻译成了同一个数学问题。

剑桥大学和伦敦国王学院研究人员发布的论文《Navier-Stokes lost in translation》指出,在 OpenAI 此前公布的 Navier–Stokes 结果中,书面证明与自动形式化的 Lean 版本并不完全对应。他们认为,代码能够编译,并不意味着它忠实表达了原始自然语言论证。

这类问题可以用一个简单比喻理解:计算机可能严谨地证明了命题 B,但论文实际声称的是命题 A。如果从 A 到 B 的翻译发生了偏差,“验证通过”仍不足以证明论文中的主张。

研究人员并不是因此断言所有相关结论都错误,而是强调自然语言证明、形式化命题和 Lean 代码之间需要可审计的对应关系。仅让同一个 AI 先写论文、再把自己的论文形式化,不能替代独立同行评审。

数学成果不仅要正确,还要被理解

OpenAI 公布的结果覆盖纯数学、理论计算机科学和数学物理等多个领域。公司表示,模型大约尝试了 4000 道开放问题,每项入选结果平均使用相当于约三小时 ChatGPT Pro 深度思考的计算量。

生产速度带来了另一种瓶颈:人类数学家的时间。一个专业研究者可能需要数周甚至数月才能检查一篇陌生领域的复杂证明,理解它为何成立,并判断它是否只是对已有方法的重新组合。AI 则可以在相同时间里继续产生更多手稿。

国际知名数学家陶哲轩批评的重点,也不是机器绝对不能解决问题,而是部分 AI 成果缺少能对结果负责的人:提交者可能无法回答同行追问、做学术报告、解释关键直觉,或把结论放回整个研究领域中理解。

这说明“形式正确”与“成为数学知识”之间仍有距离。一个结果真正进入数学体系,通常还需要:

  • 专家确认命题本身有价值且没有被已有工作覆盖;
  • 自然语言证明、形式化版本和最终结论保持一致;
  • 其他研究者能够复核、解释并在此基础上继续工作;
  • 作者清楚披露依赖、假设、模型过程和修订记录。

普林斯顿高等研究院的数学与人工智能顾问小组 AGMAI 也明确表示,其顾问角色不代表对这些结果或 OpenAI 工作流程的认可。这次公开只是人类理解和吸收这些成果的开始,而不是验证工作的完成。

未公开模型带来的可复现性问题

这些手稿由 OpenAI 尚未对外发布的内部模型生成。OpenAI 提供了仓库、部分 Lean 文件、10 份推理摘要、平均计算量和问题数量统计,但外部研究者无法使用同一个模型重新运行完整实验。

这会产生一种新的科学不对称:少数前沿实验室可以使用内部模型批量探索问题,学术界却只能在结果发布后承担审阅工作。模型如何选择问题、使用了哪些提示、失败样本如何处理以及候选成果如何筛选,都会影响对研究流程的评价。

OpenAI 表示,将资助研讨会、会议和专项计划,帮助数学界理解重要的 AI 生成成果,并计划继续改善引用、数学表达和披露方式。真正值得观察的,不只是下一批手稿数量,而是发布流程能否让第三方更容易复现和审计。

为什么这场争议会延伸到 ECDSA

OpenAI 的发布没有攻破 ECDSA,也没有给出能够窃取数字资产的算法。但它让一部分密码学研究者重新评估了一个更长期的问题:如果 AI 大幅提升发现新数学方法的速度,建立在“目前没有高效算法”这一假设上的密码系统,会不会在量子计算机成熟前先受到经典数学突破的冲击?

ECDSA 是比特币、以太坊外部账户及许多数字系统使用的数字签名算法。它的安全性依赖椭圆曲线离散对数问题在现实计算资源下难以求解。这里讨论的是签名安全,而不是泛指所有“加密技术”。

以太坊研究员 Justin Drake 提出,应当为 AI 加速数学研究导致 ECDSA 提前失效的可能性准备“bunker mode”。他把“几个月而不是几年”描述为最坏情景,并建议数字资产持有者可以有序考虑使用尚未暴露公钥的新地址。

这一观点在密码学界存在明显分歧。Coinbase 密码学负责人 Yehuda Lindell 表示,目前没有证据显示椭圆曲线密码学的经典困难假设已经被削弱。Vitalik Buterin 则认为 AI 数学风险值得认真准备,但反对用户仓促迁移资产,因为错误配置和匆忙操作本身就可能造成损失。

因此,更准确的结论是:

  • 目前没有公开证据表明 ECDSA 已被 AI 或经典计算攻破;
  • OpenAI 的数学成果本身不包含针对 ECDSA 的实用攻击;
  • “数月内失效”是研究员提出的极端风险情景,不是行业共识或预测;
  • 协议开发者确实需要提前设计后量子或其他可迁移的签名方案;
  • 普通持有者不应因媒体标题匆忙转账,更不应相信声称需要提交私钥、助记词或支付费用的“紧急迁移服务”。

对于机构和大量持仓者,合理的准备不是押注某个具体时间点,而是盘点所用签名算法、识别已经公开公钥的地址、制定经审计的迁移预案,并关注钱包和网络官方发布的升级方案。这属于风险管理,不代表攻击已经发生。

真正的“数学末日”是验证能力跟不上生成能力

OpenAI 的发布同时展示了两件事:AI 已经能够在研究级数学中产出值得专家认真检查的材料;但大规模生成、形式化验证和人类理解之间仍存在明显断层。

未来的数学研究可能不再缺少候选证明,而是缺少审阅者、解释者和能够把结果组织成知识体系的人。Lean 可以成为重要的可信基础设施,却不能独自决定一个自然语言结论是否被正确形式化,也不能回答一个定理为什么重要。

所以,“谁能理解这些证明”不是对 AI 数学能力的简单否定,而是在提醒整个行业:当生成速度超过人类吸收速度时,真正稀缺的将从证明本身,转向可复现性、语义对应、同行评审和人类理解。

新闻来源: Firstpost:“Mathocalypse”—OpenAI generates hundreds of mathematical results

官方发布: OpenAI:Sharing AI progress in mathematics;OpenAI 数学仓库修订记录

独立观点: AGMAI:On OpenAI’s Release of Mathematical Results;arXiv:Navier-Stokes lost in translation

密码学风险讨论: The Block:Crypto industry split over Justin Drake’s AI warning