本文来自微信公众号： APPSO ，作者：发布明日产品的，原文标题：《刚刚，OpenAI甩出722篇数学论文！准黎曼猜想也来了，奥特曼要让数字家「瘫坐」》
好家伙，OpenAI刚刚直接给数学界端上了722篇论文。
这是OpenAI一款内部未发布模型产出的数学成果，已经打包放进了GitHub。这些手稿归为372组成果，供所有人查看。
APPSO先给你把重点划出来：
722篇手稿，归为372组成果。同一组可能包含主结果、配套论证、推论和不同证明，不能直接理解成解决了722道独立难题。
重点课题涉及准黎曼猜想、唯一博弈猜想、霍奇猜想的特殊情形，以及自由群因子问题。光看题目，含金量已经拉满。
结果处于不同验证阶段。部分附有Lean形式化材料，公开上传也不意味着全部完成学界审查。
论文公开了，模型还没开放。人类现在拿到了研究材料，接下来要逐项检验、理解和使用它们。
GitHub🔗https://github.com/openai/math
奥特曼则发文表示：
我们正在进入一个发现的新时代。
OpenAI的说法，现有数学评测快刷满了，于是把更多开放研究问题搬上考卷。模型接到约4000个问题，输出经过归组和重要性筛选，形成了这份目录。
每项结果，平均消耗相当于约三小时ChatGPT Pro思考的算力。
看这架势，奥特曼怕是想让数学家们看完目录，先瘫坐在地上缓一缓。
准黎曼猜想，这次到底走到了哪一步？
OpenAI发布这个论文包后，罗格斯大学数学教授Alex Kontorovich在X上的反应，问号和感叹号都快装不下了：
准黎曼猜想？！？你在开玩笑吗？如果这是人类做出来的，立刻就是一枚菲尔兹奖，毫无疑问。
黎曼ζ函数与素数的分布密切相关。它在某些位置的值为零，这些「零点」的位置，会影响我们能多精确地描述素数的分布。
黎曼猜想认为，所有非平凡零点都落在实部等于1/2的直线上。这次手稿提出的结论是：实部大于7/8的区域，没有零点。
Kontorovich解释，过去在临界带靠近实部1的一侧，已知的无零点区域会随着虚部升高越收越窄。他原本以为，能把这片区域拓宽一点，就已经是重大突破。
这次手稿给出的，却是一条宽度固定、无限延伸的条带。在0到1的临界带内，7/8右侧整片区域都被划进了「零点禁区」。仓库提供了相关Lean形式化材料。
「准」字必须要加上，完整的黎曼猜想还没有因此解决。
唯一博弈猜想，多少有点给算法优化泼冷水的意思。
很多计算问题，想快速拿到最优答案太难，只好争取一个足够好的近似答案。比如Max-Cut：把关系网里的点分成两拨，尽量让更多连线跨过两拨之间。
这组论文宣称证明了唯一博弈猜想，并给出Max-Cut等问题的近似难度界限。若证明成立，在P≠NP这个尚未证实的前提下，高效算法在一般输入上的最坏情况近似保证，就无法突破相应界限。具体数据或特殊结构上的表现，仍可能继续改善。
翻到霍奇猜想，又是一个千禧年大奖难题。它关心复杂几何空间中的某类特征，能否由多项式方程定义的几何部件来表达。
这次论文处理的是CM阿贝尔簇上的有理霍奇猜想，一个特殊而重要的类别。
完整的霍奇猜想依然不能就此宣布解决。这项成果目前也未列出配套Lean形式化。
自由群因子的问题，读起来有点绕。
想象用两套基础操作，分别搭出庞大的数学运算系统。一个从两个生成元出发，另一个从三个出发：最终形成的算子代数，结构上能不能完全对应？
论文给出的答案是可以，范围还覆盖了所有参数大于1的插值自由群因子，包括无穷参数情形。仓库提供了相关Lean形式化材料。这里相同的是构造出的算子代数结构，原来的自由群并没有因此变成同一个群。
谈到AI给数学界带来的变化，美国西北大学数学家Bryna Kra在此次发布前接受WIRED采访时说：
这是个令人不安的时刻，但也着实令人兴奋。
Lean都附上了，能开香槟了吗？
按公开目录统计，162篇手稿的主结论附有Lean形式化材料。
所谓形式化，就是把命题、定义和证明写成有严格规则的代码，再交给计算机检查。Lean按逻辑规则核对推导，证明不能靠一句「显然成立」糊过去。验证时还要检查它依赖的公理和假设，以及有没有尚未补齐的证明。
康奈尔大学数学副教授Daniel Halpern-Leistner正在开发工具，把自动形式化接入数学家的日常研究，他前两天在采访中说：
现在这件事显得非常紧迫，因为用自然语言写出的论证正大量涌来。
不过，机器首先得拿对题目。若把「所有情况都成立」写成「满足额外条件才成立」，它检查的就是后一个命题。代码里的定义是否对应原问题，需要人来核对。
覆盖范围也有区别。准黎曼成果的说明就注明，论文后续应用不在该形式化范围内。因此，「主结论附有Lean材料」还不能给整篇论文的所有结论盖章。
OpenAI也承认，部分未形式化结果可能存在问题，会继续修订。
准黎曼成果的形式化范围说明
即便推导经得起检查，数学家还要弄清楚，这个方法为什么有效、能搬到哪些问题上。
这两个月，数学家和OpenAI没少拉扯
OpenAI这两个月可算是跟数学家杠上了。
8月，OpenAI召集约40位数学家，暗示模型已解出数百道题。大家要求发表能供同行研究的论文。有与会者称，公司保证不会一次性发布；OpenAI发言人则表示，不知道有过这个保证。
连有没有答应过，双方都没对上。
9月8日，OpenAI公布纳维—斯托克斯千禧年大奖问题的解答主张，附上论文和Lean形式化证明。三天后，陶哲轩等25位菲尔兹奖得主作为最初联署者，发表了关于AI与数学目标错位的公开信。
他们批评AI公司把攻克开放问题当作模型评测目标，却忽略了理解、引用和人才培养。数学家研究难题，还希望从中长出新概念、新方法。答案来得太快，这些工作未必跟得上。
也有菲尔兹奖得主没有签字。Timothy Gowers在9月17日的博客里设想，即使一年涌来1000项重要成果，数学家仍可以按领域分工消化。这会是项大工程，但未必做不到。他更担心，支撑这些研究和理解工作的学术环境会被破坏。
随后，独立数学与AI咨询小组AGMAI成立。OpenAI在9月21日的公告中回应了公开信。它还声称，一款从8月28日开始训练的新内部模型，已解决「100多个长期开放问题」。不过，公告并未附上这批成果的逐项清单和证明。
9月29日，咨询小组给出发布建议：完善引用，写成便于同行理解的论文，放到独立学术存档平台，并资助人类消化这些成果。它还明确反对继续用科学共同体无法访问的专有模型测试前沿数学问题。
今天，OpenAI甩出722篇手稿放上GitHub。OpenAI设置了修订和引用规范，公开10份推理摘要，承诺资助相关研讨会，也表示仍在寻找符合建议的社区托管方式。
同一天，AGMAI专门说明，提供建议不等于评定成果的影响，更不代表认可其产生过程。数学家需要公平获取工具和算力，才能选择自己的研究问题。
目前，生成这些成果的模型仍未向公众开放。研究者可以下载答案，却还不能普遍使用同一款工具，接着问下去。
更值得期待的下一步，是数学家也能用上这款模型，拿自己的问题去验证。
否则，大家可能忙着消化AI公司选好的题目，自己的研究还在排队。原本盼着来个科研助手，最后却给AI当起了助理，这就有点反客为主了。
更让APPSO好奇的是，看完这些AI写的论文，陶哲轩等数学家有什么反应？
