OpenAI 一次放出 372 项数学结果，数学家集体索要收据

一次提示词，372 个结果

10 月 6 日晚，OpenAI 在 GitHub 上公开了一个名为 math 的仓库。仓库里不是一篇论文，而是 722 份手稿，归入 372 个结果家族，全部由一个尚未对外发布的内部前沿模型生成。按照 OpenAI 对《Scientific American》的说法，这些结果每一项都解决或实质性推进了数学与理论计算机科学中的一个重要未解问题。

清单里最扎眼的是四维 Kakeya 猜想。除此之外，还有对若干核心计算机算法的改进、黎曼 zeta 函数的一个无零点区域（被媒体概括为向黎曼假设推进），以及 CM 阿贝尔簇上的 Hodge 猜想。这批结果覆盖代数、数论、理论计算机科学、数理逻辑与拓扑。

除非他们发布模型、并且人们能复现结果，否则任何关于「单个智能体一次提示就攻克问题」的说法都应被视为未经证实。我们应该索要收据。——麻省理工学院数学家 Andrew Sutherland

争议的核心不是结果对不对，而是过程说不清。一个月前 OpenAI 宣布用 1 万个智能体、花费数百万美元算力解决了 Navier-Stokes 问题；这次公司说，几乎每一项结果都来自一个智能体、一次提示，平均算力约等于 ChatGPT Pro 思考三小时。如果为真，意味着前所未有的数学能力可能很快人人可用；但模型本身没有发布，逐条的提示词也没有公开。

Lean 验证了逻辑，没验证重要性

仓库里最强的一块是形式化。OpenAI 的 Lean 目录列出了 162 篇带形式化主定理的论文。Lean 是能逐行检查证明逻辑的编程语言，通过检查的形式化证明几乎可以确定推理无误。但这里有一条容易被忽略的边界：Lean 只能保证从给定公理与引理出发、这个形式化证明成立，它不判断结论是否新颖、是否重要，也不保证形式化的命题与原始未解问题真的是同一个问题。

OpenAI 自己也标注了：未形式化的结果可能存在问题。帝国理工学院的 Kevin Buzzard 告诉《New Scientist》，在他熟悉领域的 30 篇论文中，只有 7 篇看起来足够惊艳，而其中只有 1 篇经过 Lean 形式化验证。

顾问组给了建议，公司没有全部采纳

9 月 21 日，OpenAI 宣布组建独立的数学与人工智能顾问组（AGMAI，挂靠普林斯顿高等研究院），请其为负责任地发布 AI 生成的数学结果提供建议。该组的建议很直接：公开模型名称、精确提示词与每条结果所耗算力，并停止用专有内部模型去测试高难度数学问题。

OpenAI 的做法是：公布平均算力与部分统计，不公布任何提示词，并明确表示公司不受这些建议约束。顾问组 10 月 6 日声明称，其角色不应被解读为对这些结果影响力的判断，也不构成对 OpenAI 获取结果的过程的背书。

有意思的是，OpenAI 发言人承认，很多新公开的结果连公司自己的数学家都还没完全看懂。多伦多大学的 Daniel Litt 认为公开发布对数学是好事——如果想知道这些数学问题的答案，看不出有什么理由让公司替我们保密；而 Terence Tao 则批评前沿实验室这种疯狂的出题节奏。这场争论真正的分歧点也许不是 AI 能不能做数学，而是当答案先于理解到达时，学术共同体该如何消化它。