OpenAI 本周突然向数学界投放了近 400 项 AI 生成的数学结果,分布在 700 多份手稿中,覆盖组合数学、多个几何分支、数论、理论计算机科学、代数、拓扑、概率与统计力学以及数学物理等方向。据 The Verge 报道,超过 36 位数学家在受访时用「惊人」「压倒性」「前所未有」「超现实」「纯粹的疯狂」来形容自己的反应。这批材料的体量之大,甚至让 OpenAI 自己都觉得有必要发布一份导航指南,帮助研究者在这座庞大的 GitHub 仓库中找路。

即便只是做初步评估也异常困难。多数受访数学家表示,在发布后的数小时乃至数天里,他们仍在努力消化全部内容;有几位说,光是过一遍约 40 页的目录与摘要就花了将近一小时。康涅狄格大学数学教授 Álvaro Lozano-Robledo 表示,仅仅浏览全部摘要就已经让人不堪重负。

手稿中夹杂着用 Lean 写成的形式化内容。Lean 是一种编程语言兼证明助手,可让结果被计算验证。这类形式化在此前评估 OpenAI 的数学声明时发挥过关键作用,能让研究者即便不完全理解论证过程,也对某个声明的逻辑正确性抱有信心。有研究者形容,如果这些 AI 现在消失,就像外星人来到地球后又离开,数学界接下来十年都会用来研究这批东西、试图理解全部内容。

但每项结果被验证的程度差异极大。OpenAI 在 GitHub 上承认,这些结果处于「不同的验证阶段」,「许多但并非全部手稿已被形式化」。截至报道时,这批手稿中不到一半似乎有形式化描述。OpenAI 表示,719 份手稿中只有 300 项主要结果完成了形式化,约占 42%,并称会随着获得更多形式化内容而更新仓库。

多位数学家向 The Verge 抱怨形式化不足,尤其是在结果数量如此庞大的情况下,并强调即便有 Lean 代码伴随,评估也并非瞬时完成。研究者必须核对形式化内容是否真的证明了结果所声称的东西,这又是一个耗时的过程。有几位翻查论文的人表示,即便提供了可被计算机验证的证明,质量也不一致,而且被验证的陈述并不总能与随附手稿中的声明严丝合缝地对应。

伦敦帝国理工学院数学教授 Kevin Buzzard 表示,他在自己从事的代数数论领域识别出大量定理,其中只有大约 6 个立刻「脱颖而出」,而这些定理中几乎没有几个看起来在 Lean 中完成了形式化验证。他的困境颇具代表性:要么去读可能并不正确的「垃圾内容」,要么等别人去读,要么等有人把它们形式化,之后才能确定结果是否正确。

Buzzard 对 AI「垃圾内容」的担忧并非孤例。这个词是低质量、常常出错的 AI 生成材料的简称,这类内容正越来越多地出现在网上乃至现实世界中,包括学术论文。数学家们告诉 The Verge,近年来用 ChatGPT 和 Claude 等工具生成的此类材料大幅增加,其中许多内容令人费解、难以阅读,对主题的理解也很有限,在引用其他研究者成果方面尤其粗糙。OpenAI 此前的数学写作就曾因草率而受到专家广泛批评,尤其是署名与出处标注糟糕甚至完全缺失。

在发布前与 The Verge 的交流中,多位研究者已把即将到来的论文洪流称为「slopocalypse」(垃圾内容末日)或类似说法。这场担忧中的「末日」是否真的成为现实,很难判断,很大程度上是因为材料数量令人眼花缭乱。早期迹象显示,OpenAI 这一次对论文更为用心,至少对其中一部分是如此。有几位数学家表示,第一印象远好于他们的预期,不过他们也承认,鉴于该公司此前出版物质量堪忧,这个门槛本来就不高。

从产业视角看,这次发布把两个问题同时摆上台面。其一是能力问题:如果这批结果中确有大量成立的新定理,那意味着前沿模型在形式化推理与数学发现上的能力又向前迈了一步,这对 AI 在科研、工程与药物研发等需要严密推理的场景中的可信度是正面信号。其二是可信度问题:形式化比例仅约四成、质量参差、声明与验证内容未必对齐,意味着「AI 能产出数学成果」与「这些成果可被数学界采信」之间仍隔着巨大的验证鸿沟。

对关注 AI 产业的人而言,这件事的意义不只在数学本身。它是一次关于 AI 生成内容如何进入严肃知识生产体系的压力测试:当产出速度远超人类审阅速度时,验证机制、署名规范与学术信用体系都会承压。OpenAI 选择继续向前推进,而数学界则要花数年时间,从海量手稿中分辨哪些是真正的成果、哪些只是看似合理的「垃圾内容」。这一分工本身,或许就是 AI 时代科研生态正在形成的新常态。