ARTICLE · 1149257
OpenAI 把 372 个 AI 写的数学证明丢到了 GitHub,顺手踢了一脚学术界
10 月 7 日清晨，推特上几乎所有跟 AI 沾边的账号，都同时在做同一件事：打开同一个 GitHub 仓库——openai/math。三小时内，它涨到了 2000 多颗星。
仓库里装着722 份数学手稿，被归进372 个“成果族”。每一族通常包括一个主结果，加上配套论证、推论或替代证明。Apache 2.0 开源协议，带版本历史，带引用规范，带 Lean 形式化证明。
Lean 是什么？它是一种“证明用的编程语言”——你把数学证明写成代码，让计算机机械地检验每一步逻辑是否成立。如果 Lean 通过，证明就是真的；如果 Lean 拒绝，证明就是错的——没有“看起来差不多对”这种暧昧地带。
Sam Altman 在推特上配了一句话：
我们正在进入一个发现的新时代。
这句话一出来，数学圈的反应几乎可以分成三种颜色：兴奋的、转发的、和直接发火的。
如果你点开目录，会发现 OpenAI 列出的清单密度很高——一份足以让任何读过研究生数学课程的人多看几眼的清单。
黎曼猜想 167 年了没人能证，数学家退而求其次：能不能证明存在某个小于 1 的常数 θ，使得黎曼 zeta 函数在实部大于 θ 的整个半平面里都没有零点？哪怕只是把“零点的稀疏区”往前推一步，都是几十年的事。OpenAI 这次给的结论是θ = 7/8，并且已经给出 Lean 形式化。
挂谷猜想今年 7 月刚被王虹和 Joshua Zahl 在三维上证明，拿了菲尔兹奖。四维版还摆在“未解决”的招牌下。清单里这一族同时声称解决三维挂谷的“极大函数”猜想和四维的“豪斯多夫维数”猜想。
理论计算机科学方向，编号 102声称证明了 2002 年提出的唯一游戏猜想，并据此给出 Max-Cut、顶点覆盖等经典问题的最优近似难度门槛。代数几何方向，编号 032声称对所有复 CM 阿贝尔簇证明了霍奇猜想。数论方向，有理数域上的希尔伯特第十问题给出了否定解答——这是一道千禧年大奖难题级别的标志性问题。
剩下还有：π 的无理性测度恰为 2、卡塔兰常数是无理数、马勒猜想在所有维数成立、平面不能用五种颜色完成单位距离染色、Kaplansky 零因子猜想、Hadwiger 猜想的反例构造……
清单里的每一个名字，放在一个数学系研究生面前，都是一个“可能要为之耗掉半辈子”的题目。
而 OpenAI 的同事把它们喂给一个 AI 模型，平均每条结论大约花了 3 小时 ChatGPT Pro 思考算力。
如果你只看 372 这个数字，会以为这是某种科研奇迹；但如果你细看 OpenAI 在 README 里披露的“流水线”，你会发现这件事真正可怕的地方不在“做数学”，而在“做数学的成本结构”。
整个评估里，模型被投喂了约4000 个研究问题。几乎每个成果，都来自对单一 AI agent 发出的单一提示——有些需要多次尝试，但没有一次需要像两个月前那次 Navier-Stokes 那样，动用 10000 个并行智能体协同工作 88 小时、再花数百万美元算力。
这意味着什么？意味着在 4 个月的时间里，同一家公司把“啃下一道千禧年大奖难题”的成本，从“一次奥林匹克级别的人类协作”压缩到了“一个工程师一下午的工作”。
这不是数学上的胜利，这是算力经济学上的胜利。
而 OpenAI 在这之上又叠加了一层更深的赌注——他们选的不是把论文投到期刊，而是直接扔到 GitHub，带版本历史、带修改日志、带引用协议。给“为什么要这么做”的解释，他们只在 README 写了一句很轻的话：“这是为了让结果能更可被检查。”
但所有人——包括 25 位菲尔兹奖得主——都听出了这句话背后的意思：传统期刊的同行评审，跑不过这个速度。
这件事最不缺是在公开反应。
4000 多名数学家联署《莱顿宣言》，要求 AI 公司遵守数学界的标准——披露 AI 使用、做好同行评审、承认前人工作、保持开放获取。
OpenAI 发布 Astra 第一批 10 道难题结果时，Yeshiva 大学的Steven Miller就公开指控：其中球填充密度上界的核心论证，实际上来自他 2016 年的论文，被当作原创新出。另一位剑桥的Francesco Fournier-Facio也说，OpenAI 的“AI 突破”叙述，抹掉了人类数学家在同期已经做出的进展。
25 位菲尔兹奖得主（包括陶哲轩）联署了一封公开信——《A Severe Misalignment of AI in Mathematics》。信的核心论点是：解题只是工具和代理指标，真正的目标是概念性理解；仓促发布会留下大量真话但污染思想地基的命题。
Fields Medal 获得者Gowers进一步警告：“一到二十年内，数学文献可能爆炸式增长，但能真正读懂它的人类共同体却在消失。”
有数学家开始担心有人抢跑。纽约大学的Tristan Buckmaster公开指控 OpenAI 抢跑了他与 Anthropic 员工 Levent Alpöge 私下合作的研究——他们还没发表，OpenAI 的工具已经在协助他们研究，但 OpenAI 却单独发布了相关方向的结果。
MIT 的Andrew Sutherland干脆把话说得更死：“在模型公开、别人能复现之前，‘一个 agent 一次提示就解决一道题’这种说法，应该被当作未经验证处理。”
Toronto 的Daniel Litt更直接：“如果数学共同体想要这些问题的答案，没理由要依赖一家公司来掌握生产它们的手段。”
陶哲轩在 9 月的一篇博文中给了一个很精准的判断，后来被反复提及：
真正的冲突不是人类推理对机器推理，而是充沛的证明产出与稀缺的专家注意力之间的错配。
这句话翻译成大白话：不是 AI 抢了数学家的饭碗，是数学家忽然发现——自己的时间变成了整个系统里最稀缺的资源。
过去 100 年，数学的瓶颈是“想出新定理”。一个天才花 10 年想出一个证明，够让整个领域震动 50 年。
OpenAI 这次入门级算力的清单一旦被数学共同体接受，瓶颈立刻移到了下一个位置：谁来读懂这些证明，谁来评价它是否真的重要，谁来把它接进人类已有的知识地图。
OpenAI 自己显然也意识到了这一点。所以他们在 README 里专门写了一行：“我的档案设定中，数学家可以建议如何发布结果，但不能建议是否、如何快地生产结果。”
——也就是说，咨询小组对怎么写论文有发言权，但对要不要这么大规模生产没有否决权。
Adobe 在博客里也说会“资助一系列工作坊、会议、专项计划，围绕理解 AI 产生的重要结果展开”。这些会议里讨论的对象，会有一批 AI 已经做完、不再回头看的命题。
你可能跟数学没什么关系。但这件事有三层意思值得每个普通上班族记一下。
这次是数学，下次可能是法律判例、芯片架构、药物分子、新材料结构——任何“可以被明确反馈信号驱动”的领域。今天的 ChatGPT Pro 每月 200 美元；明年的“Pro+”可能就能让一个文科生在法学、医药学、社会科学里复刻 OpenAI 这次在数学里的复刻。
372 个结果没有一篇投到期刊，而是直接扔到 GitHub 上。这是一个对学术惯例的结构性主动让步——不是推翻论文，而是判断期刊的模式正在被绕过。下一步会是什么？GitHub 上贴的论文 + Lean 验证，直接取代期刊的同行评审？
数学家的发展节奏跟机器的产出节奏一旦错位，就会出现一种新身份——“数学结果翻译”。不是把外文翻成中文，是把机器生成的证明，翻译成人类能消化、能讲给学生听、能纳入研究路径的内容。这件事机器暂时干不了，因为它需要的不是验证，是理解。
陶哲轩在 9 月那份联署信的结尾，写了一句很克制的话：
这并不是要阻挡 AI 走入数学，而是要确保 AI 进入的方式，与数学的健康相容。
这句话，与其说是给 OpenAI 的，不如说是给我们每一个人的。
372 个结果不是终局，只是一个工业流水线刚刚被调试完的信号。这个信号告诉我们：当一件事的成本被足够压低，被压低的不会是这件事本身，而是我们理解它的能力。
GitHub 上那个仓库，3 小时涨 2000 颗星——这是 AI 圈的反应。
数学社区的反应，可能要等半年到几年才会真正显现。
我们等得起。但我们也要做好准备：下一个被这样压低成本的，可能不是数学。