这只能被形容为学术界的“往人头上扔钢琴，然后请他们审阅乐谱”——OpenAI本周发布了近400个AI生成的数学成果，分布在700多份手稿中。数学界的反应从“惊人”到“纯粹的疯狂”不等——这还是客气点的说法。

这批成果涵盖组合数学、几何学的几个分支、数论、理论计算机科学、代数、拓扑学、概率论与统计力学以及数学物理。其规模之大，以至于OpenAI觉得有必要发布一份指南，教人如何浏览这个庞大的GitHub仓库——这有点像给你一张地图，指向一栋你刚刚放火烧掉的建筑。

“光是浏览全部摘要列表就让人不堪重负，”康涅狄格大学数学教授阿尔瓦罗·洛萨诺-罗夫莱多说道。多位数学家告诉The Verge，仅仅通读大约40页的目录和摘要就花了他们将近一个小时。给在家记分的人算一下：光读菜单就要一小时。

在数百份手稿中，零星散布着Lean形式化证明——Lean是一种编程语言和证明助手，允许通过计算验证结果。这些形式化证明在评估OpenAI此前的一些数学主张时发挥了重要作用，让研究者即使不完全理解背后的论证，也能对某个主张的逻辑正确性抱有信心——这有点像不懂除法却信任计算器。

但每个结果的验证程度差异极大。在GitHub上，OpenAI承认这些成果“处于不同的验证阶段”，并且“许多，但并非全部，手稿已被形式化”。截至撰写本文时，该合集中不到一半的手稿似乎有形式化描述。OpenAI表示，719份手稿中只有300个顶级结果被形式化——约42%——并且“将在获得更多形式化证明时更新仓库”。所以，大约58%的数学末日仍未经验证。安心睡吧。

多位数学家向The Verge抱怨缺乏形式化，尤其是考虑到成果数量之巨。即使有Lean代码伴随某个结果，评估也并非瞬间完成。研究者必须检查形式化是否真正证明了结果所声称的内容——这又是一个耗时的过程。几位深入研读论文的人表示，即使提供了计算机可验证的证明，质量也参差不齐，而且它们所验证的陈述并不总能与随附手稿中的主张完美对应。

伦敦帝国理工学院数学教授凯文·巴扎德表示，他在自己的研究领域——代数数论——中识别出了大量定理，其中只有大约六个立即“引人注目”。这些定理中，几乎没有几个似乎在Lean中被形式化验证。“因此，我要么得去读可能不正确的垃圾，要么等别人也这么做，要么等有人将它们形式化，然后我才能确定这些结果是否正确。”巴扎德的担忧得到了许多其他研究者的呼应，他们这周想必还有别的事要忙。

巴扎德远非唯一担心AI“垃圾”的人——这是低质量、经常出错的AI生成材料的简称，这类材料越来越多地出现在网上和现实世界中，包括学术论文。与其他领域一样，数学家们告诉The Verge，近年来他们看到用ChatGPT和Claude等工具生成的此类材料急剧增加。其中许多内容令人困惑、难以阅读，对主题的理解甚少；在引用其他研究者方面尤其粗制滥造。OpenAI此前的数学文章曾被专家广泛批评。