OpenAI公开722篇AI生成数学成果，数学家称需数年消化

OpenAI在GitHub上公开了722篇由内部未发布前沿模型生成的数学研究成果，涉及数论、代数几何、分析、组合数学等多个方向，部分成果配有Lean形式化证明。这是本次事件中少数没有争议的事实。

但发布之后，数学界面对的第一个问题不是“这些结果对不对”，而是“这些结果是什么”。几位研究者称，光是看完大约40页的目录和摘要就花了将近一个小时。康涅狄格大学数学教授Álvaro Lozano-Robledo表示，仅仅浏览完整的摘要列表就已经让人感到不堪重负。

《The Verge》就此采访了30多位数学家，他们用“令人震惊、压得人喘不过气、前所未有、恍如梦境、简直疯狂”等词形容这次冲击。研究人员普遍认同，仅仅理解OpenAI这次发布的内容可能就需要数年时间。

这里出现了一个结构性错位：AI产出新数学的速度，开始超过数学界理解、验证和吸收数学的速度。发布是一次性的，消化却是逐年累加的。

OpenAI表示，在700多篇手稿中只有300项核心结果完成了形式化验证，约占42%，并称会随着获得更多形式化证明继续更新仓库。截至报道发稿时，这批手稿中完成形式化验证的比例还不到一半。

多位数学家向《The Verge》抱怨形式化验证覆盖不足，尤其是在成果数量如此庞大的情况下。他们强调，即便某项结果附带了Lean代码，评估也不意味着可以立刻完成——研究人员还需要进一步检查：这份形式化证明究竟证明了论文声称的那个结论，还是只证明了一个与之相关、但并不完全等价的命题。

伦敦帝国理工学院数学教授Kevin Buzzard提供了一个具体切片。他在自己研究的代数数论领域里发现了不少相关定理，但其中只有大约六个结果第一眼就特别突出，而这些结果中几乎没有一个看起来已经在Lean中完成了正式验证。他的处境因此变成：要么去读这些可能并不正确的材料，要么等其他人先读，要么等有人把它们形式化之后才能确定对错。

验证不足并非抽象担忧。研究者Fan Nie表示，他们用自建验证系统OSVerify检查OpenAI 10月4日版本的《Global quantum geometric Langlands at irrational level》时发现了两个重大问题，其中一个问题还由系统提出了修复方案。这提示了一种新格局：AI负责生成证明，另一套AI系统负责找错和修补。