AI 形式化验证群分类定理,揪出顶刊论文 96 处错误

skdh · x · 2026-11-03

Axiom Math 团队在形式化「有限单群分类定理」(CFSG)的过程中,发现 47 篇已发表论文中存在 96 处实质性数学错误,并发布了「百项精选出版论证偏差」清单——完整的勘误清单多达数千条。这些论文均经同行评审,发表在《Annals of Mathematics》等顶级数学期刊上。

团队指出,这正是形式化验证的价值所在:即便是经过严格审稿的顶级成果,也会有错误和漏洞被机器可验证的形式化过程揪出,尤其在「vibeproving」(凭感觉让 AI 写证明)盛行的时代,形式化更显关键。配图为清单目录,逐条列出各案例的错误类型,如「L₄(2) 归约缺少两个非包含假设」「Sylow 2-子群与 3'-子群的分类案例」等。