OpenAI 称 AI 推翻了指数时间假设，接下来轮到人类专家验货
OpenAI 周一一口气放出三项由 AI 产出的结果，任何一项站得住都够一个学者吃一辈子。一项宣称证明了所有维度的局部光滑性猜想，OpenAI 说这顺带解决了 Kakeya 猜想和 Stein 限制猜想。一项宣称指数时间假设（ETH）是错的。还有一项宣称给出了四维含规范场和费米子的相互作用量子场论的严格存在性证明，其中包括量子色动力学 QCD，这已经是千禧年大奖里 Yang-Mills 问题的地盘了。
时间线写得很清楚。局部光滑性的结果 10 月 18 日得到，第二天完成 Lean 形式化。ETH 的自然语言反证 10 月 16 日找到，17 日完成 Lean 形式化。Yang-Mills 存在性的自然语言证明 9 月 9 日出来，QCD 是 9 月 18 日，Yang-Mills 的 Lean 形式化 10 月 16 日完成。数学和计算机那两项的文件周一 UTC 20:52 已经推到 openai/math 仓库。
最有意思的是交接方式。局部光滑性的结果直接原样公开。ETH 交给 Russell Impagliazzo、Ramamohan Paturi、Ryan Williams 三位组成的小组，OpenAI 承诺出钱办一场会。物理那项交给 David Gross 牵头，加上 Douglas、Jaffe、Klebanov、Nekrasov，材料暂不公开。OpenAI 定了四条规矩：不签保密协议，OpenAI 不要学术署名，给验证者应有的认可，评审自愿且不付费。
分寸要拿住。Lean 证明是很硬的证据，但前提是形式化的命题和数学家心里那个定理是同一个东西，这一步翻译恰恰是专家要盯的地方。到现在为止，三项里没有一项获得独立专家的认可。被点名的验证者之一 Ryan Williams 在 X 上把计算机那项概括为：n 个变量的 3SAT 能在大约 exp(n/(log n)^(1/2+o(1))) 的时间里解出，这是一个可以被具体检验的命题。别忘了，OpenAI 之前也撤回过 AI 写的数学论文。这次发布真正说明的是瓶颈挪了位置：生成证明只花了几周，验证却变成了一个有名有姓的人类评审流程，OpenAI 出的是会议的钱，不是评审的钱。验证才是产品，在数学前沿和在 CI 流水线里都一样。
OpenAI 原文：https://openai.com/index/building-scientific-understanding-with-academic-communities/ 预印本和 Lean 文件：https://github.com/openai/math HN 讨论：https://news.ycombinator.com/item?id=50251344
← 返回所有文章
时间线写得很清楚。局部光滑性的结果 10 月 18 日得到，第二天完成 Lean 形式化。ETH 的自然语言反证 10 月 16 日找到，17 日完成 Lean 形式化。Yang-Mills 存在性的自然语言证明 9 月 9 日出来，QCD 是 9 月 18 日，Yang-Mills 的 Lean 形式化 10 月 16 日完成。数学和计算机那两项的文件周一 UTC 20:52 已经推到 openai/math 仓库。
最有意思的是交接方式。局部光滑性的结果直接原样公开。ETH 交给 Russell Impagliazzo、Ramamohan Paturi、Ryan Williams 三位组成的小组，OpenAI 承诺出钱办一场会。物理那项交给 David Gross 牵头，加上 Douglas、Jaffe、Klebanov、Nekrasov，材料暂不公开。OpenAI 定了四条规矩：不签保密协议，OpenAI 不要学术署名，给验证者应有的认可，评审自愿且不付费。
分寸要拿住。Lean 证明是很硬的证据，但前提是形式化的命题和数学家心里那个定理是同一个东西，这一步翻译恰恰是专家要盯的地方。到现在为止，三项里没有一项获得独立专家的认可。被点名的验证者之一 Ryan Williams 在 X 上把计算机那项概括为：n 个变量的 3SAT 能在大约 exp(n/(log n)^(1/2+o(1))) 的时间里解出，这是一个可以被具体检验的命题。别忘了，OpenAI 之前也撤回过 AI 写的数学论文。这次发布真正说明的是瓶颈挪了位置：生成证明只花了几周，验证却变成了一个有名有姓的人类评审流程，OpenAI 出的是会议的钱，不是评审的钱。验证才是产品，在数学前沿和在 CI 流水线里都一样。
OpenAI 原文：https://openai.com/index/building-scientific-understanding-with-academic-communities/ 预印本和 Lean 文件：https://github.com/openai/math HN 讨论：https://news.ycombinator.com/item?id=50251344
评论