10月6日，OpenAI 在 GitHub 上公开了一大批数学成果：几百篇论文，来自一个还没有对外发布的内部前沿模型。有人说这是 AI 搞数学研究的里程碑，也有数学家说：先别急，还得一篇篇检查。这件事到底怎么回事？一篇文章给你讲明白。
一、先说结论：发生了什么？
OpenAI 在名为 openai/math 的公开仓库里，放出了一大批“AI 写的数学论文”。这些论文都出自同一个没有公开发布的内部模型，OpenAI 只称它为“内部前沿模型”，没有公布名字。
这次放出来的东西，大致分三类：
论文手稿：按主题分成372个“家族”，同一个家族里可能有主要结果、配套论证，也可能有换一种思路的证明；
Lean 证明文件：可以让电脑自动检查的“标准答案”（后面细说）；
推理过程摘要：只有10个结果附上了模型“怎么想”的精简版。
关于论文数量，不同报道里有719篇、722篇两种说法。仓库自述目前写的是719篇，估计是发布后有过调整，以仓库最新页面为准。
二、这些数字怎么读？
OpenAI 说，它拿大约4000个数学问题去考这个模型，这些问题大多是数学界还没解决的“开放问题”。最后挑出“够分量”的结果，整理成这批论文。
这里有两点要注意。第一，719或722是“论文篇数”，不是“解决了多少个问题”。第二，是从4000道题里挑出来的，并不是每道题都做对了。
另外，OpenAI 说，绝大多数结果用的是同一套流程，平均每个结果花的算力，大约相当于 ChatGPT Pro 想3个小时。也有例外，比如关于黎曼ζ函数零点区域的工作，以及针对一类特殊对象（CM 阿贝尔簇）的霍奇猜想证明，处理方式不太一样。
三、Lean 是什么？为什么重要？
数学证明有个麻烦：写得再漂亮，也得有人一行一行检查，几百页的论文，数学家可能要看好几个月。
Lean 是一种“能让电脑检查证明”的语言。把证明翻译成Lean，电脑就能像自动判卷机一样，逐步检查每一步对不对。只要通过，基本就不用担心中间出错。
OpenAI 说，目前大约42%的主要结果已经有了Lean版本，剩下的会陆续补上。换句话说，还有相当一部分结果没有经过这道“自动判卷”。OpenAI 自己也承认，没有形式化的部分可能存在问题，发现后会尽快修正。
四、请了“外脑”：高等研究院顾问组
文章开头那句话，说的就是这件事：OpenAI 表示，这次发布参考了普林斯顿高等研究院（IAS）“数学与人工智能独立顾问组”的建议。
这个顾问组今年9月成立，据报道有9位不拿报酬的成员，包括菲尔兹奖得主高尔斯（Timothy Gowers）、Martin Hairer和物理学家威滕（Edward Witten）。9月29日，他们公布了一份给各大 AI 公司的建议，核心是：AI 生成的数学成果，该怎么公开、怎么让数学界检验。
说白了，AI 一口气写出这么多论文，人类数学家很可能“看不过来”，所以需要一套规矩，让大家知道这些东西是怎么来的，该怎么查。
五、质疑的声音
不过，这次发布并没有一片叫好。一些报道和数学家指出：
公开的信息不够多：顾问组建议公开模型名称、提示词、推理过程摘要、耗时和算力成本，而这次只有10个结果附了推理摘要，模型名称也没有公布；
无法独立复现：模型没有发布，外界没法自己再跑一遍，“一次提示、单个智能体就得到这些结果”的说法只能暂时听 OpenAI 的；
难以逐篇检验：麻省理工的数学家萨瑟兰（Andrew Sutherland）等人认为，在模型发布前，这些说法都还没法验证；仓库也没有开放议题（Issues）功能，反馈渠道有限；
“人看不懂”的风险：哈佛大学的数学教授 Melanie Wood 说过，这类结果在发布时还没有人真正理解，真正的工作现在才开始。
也就是说，这批论文更像是“交给数学界审稿的一大摞稿件”，而不是已经盖章认证的定论。要验证它们到底站不站得住，可能需要好几年。
六、普通人怎么看？
第一，别把“发布”当成“被证明”。论文放到网上，只是起点。数学里最重要的一步是同行检验，这一步才刚开始。
第二，AI 做数学研究，确实正在加速。不管最后有多少结果经得起检验，一个模型三小时就能产出一篇值得认真阅读的论文，这个速度本身就值得重视。
第三，比结果更重要的，是“规矩”。AI 公司该公开多少细节？数学界怎么审、怎么署名、谁来负责？这些问题，这次发布才刚刚摆上桌面。
参考
[1]https://github.com/openai/math
[2]https://x.com/OpenAI/status/2107596713791767021
本文转载自微信公众号「MarsKr」，作者：Marskr，已获授权。阅读原文
发表回复