OpenAI 往 GitHub 扔了 722 篇数学论文，还没人读得懂
周二晚上 OpenAI 推了一个叫 openai/math 的仓库，Hacker News 一夜给了 1,205 分。里面是 722 篇手稿、372 个结果族，出自一个未发布的内部模型，题目全是数学家追了几十年的东西。Unique Games 猜想的证明。L=BPL。整数乘法突破 n log n，打破 1960 年代以来的界。矩阵乘法做到 n 的 9/4 次方。Kaplansky 直接有限猜想的反例。Ryser 覆盖猜想和 Kurosh 除环问题的反例。Scott Aaronson 的妻子把整个职业生涯押在 Unique Games 猜想上，Aaronson 说这"肯定是数学史上最大的日子之一"，然后引了妻子第一晚的反应："像嗑了药的人写的""不靠 AI 根本读不下去"。
对做 agent 的人来说，方法比结果更值得看。OpenAI 给一个内部模型出了大约 4,000 道题，每个结果平均烧掉三小时 ChatGPT Pro 的思考算力，然后把产出聚成结果族、按显著性筛。就这么一套流程，几周里产出了看上去像十年理论界的工作量。随仓库放出了十份推理摘要，包括 pi 的无理性指数、稀释自旋玻璃的 Mezard-Parisi 公式、三维相对论 Vlasov-Maxwell 系统。这个仓库是对高等研究院"数学与 AI 顾问组"的回应，该顾问组 9 月 29 日要求各实验室带引用、带修订、带版本地发布结果。OpenAI 说会资助理解这些结果的研讨会，并且"正在负责任地准备发布这个模型"。
然后是很大的但书。OpenAI 自己的 README 写着：结果"处在不同的验证阶段""并非都有 Lean 形式化""部分未形式化的结果可能有问题"。Aaronson 的妻子发现引用"经常不相关且令人困惑"，构造是"某种外星式的疯狂"。同一天，Bastounis、Circelli、Hansen 的论文（arXiv 2610.08144，HN 191 分）论证一张 Lean 证书并不能证明它翻译自的那篇自然语言证明。他们证明把数学散文里的歧义忠实消解掉，在可解性复杂度指数层级里高到任意位置，比停机问题还难；并且声称 OpenAI 早先那个 Navier-Stokes 的 Lean 证明和它本该验证的自然语言论证对不上。如果这成立，这 722 篇论文的验证故事比 Lean 徽章显得的要薄。
诚实的说法是：理解的赛跑才刚开始，而且理解得靠 AI 帮忙，因为论文不靠 AI 读不动。Aaronson 的预言是一个"有远见和创造性想法、让 AI 帮你检验和实现"的天堂般数学界。眼下的现实是 372 族主张、一部分形式化了、每族可能只有几百个能读懂的人，外加一篇理论论文说最坏情况下翻译问题不可计算。这是验证积压，不是终点线。
链接：github.com/openai/math、openai.com/index/sharing-ai-progress-in-mathematics/、scottaaronson.blog/?p=10169、arxiv.org/abs/2610.08144
← 返回所有文章
对做 agent 的人来说，方法比结果更值得看。OpenAI 给一个内部模型出了大约 4,000 道题，每个结果平均烧掉三小时 ChatGPT Pro 的思考算力，然后把产出聚成结果族、按显著性筛。就这么一套流程，几周里产出了看上去像十年理论界的工作量。随仓库放出了十份推理摘要，包括 pi 的无理性指数、稀释自旋玻璃的 Mezard-Parisi 公式、三维相对论 Vlasov-Maxwell 系统。这个仓库是对高等研究院"数学与 AI 顾问组"的回应，该顾问组 9 月 29 日要求各实验室带引用、带修订、带版本地发布结果。OpenAI 说会资助理解这些结果的研讨会，并且"正在负责任地准备发布这个模型"。
然后是很大的但书。OpenAI 自己的 README 写着：结果"处在不同的验证阶段""并非都有 Lean 形式化""部分未形式化的结果可能有问题"。Aaronson 的妻子发现引用"经常不相关且令人困惑"，构造是"某种外星式的疯狂"。同一天，Bastounis、Circelli、Hansen 的论文（arXiv 2610.08144，HN 191 分）论证一张 Lean 证书并不能证明它翻译自的那篇自然语言证明。他们证明把数学散文里的歧义忠实消解掉，在可解性复杂度指数层级里高到任意位置，比停机问题还难；并且声称 OpenAI 早先那个 Navier-Stokes 的 Lean 证明和它本该验证的自然语言论证对不上。如果这成立，这 722 篇论文的验证故事比 Lean 徽章显得的要薄。
诚实的说法是：理解的赛跑才刚开始，而且理解得靠 AI 帮忙，因为论文不靠 AI 读不动。Aaronson 的预言是一个"有远见和创造性想法、让 AI 帮你检验和实现"的天堂般数学界。眼下的现实是 372 族主张、一部分形式化了、每族可能只有几百个能读懂的人，外加一篇理论论文说最坏情况下翻译问题不可计算。这是验证积压，不是终点线。
链接：github.com/openai/math、openai.com/index/sharing-ai-progress-in-mathematics/、scottaaronson.blog/?p=10169、arxiv.org/abs/2610.08144
评论