有限单群分类定理这道长达约1.5万页、散落在500多篇论文里的“巨大定理”，几十年来没有一个人从头到尾读完过。Axiom于10月26日宣布，用几十个AI a… · @ThanksuTrump · TwKit

@ThanksuTrump

有限单群分类定理这道长达约1.5万页、散落在500多篇论文里的“巨大定理”，几十年来没有一个人从头到尾读完过。Axiom于10月26日宣布，用几十个AI agent花了24天，把它全部改写成Lean代码，并表示检查已经全部通过。 这个定理给出所有有限单群的完整清单：它们要么属于几个有固定规律的大家族，要么是26个不属于任何家族的特例。最大的特例叫“魔群”，元素个数是8后面跟53个零。找到这些单群不算最难，难的是证明清单里没有漏掉任何一个。约100位数学家花了几十年才完成证明。 证明太长，人查不过来，出过错也不奇怪。1983年牵头数学家宣布证明完成，后来发现其中一块根本没写完，直到2004年才用一本1221页的书补上。2012年有团队用类似工具，花了约6年才查完这个定理里一篇255页的论文。 Lean会一步一步核对每一步是不是真的能从前面推出来，不接受人读论文时默认“显然成立”的跳步。检查结论是定理本身没错，清单还是那张清单。问题出在中间一篇论文的证法上：整个证明要用到“不平衡群定理”这个中间结论，Axiom照着John Walter 1986年给出的证明来翻译，AI发现其中引用的一个说法是错的，并举出了具体反例。 Axiom请教了当年参与原始证明的数学家Richard Lyons和Ronald Solomon，借用Solomon 1976年的一套思路，由AI写出一个新证法，绕开出错的那一步，也通过了Lean检查，并整理成一篇35页的论文。除此之外，查出来的大多是笔误、表格写错、少写了前提这类小毛病。Axiom博客说其中34处值得专门处理，完整清单还没公布；推文说法更重，称修了“几百处重大勘误”。 几十个AI agent分工：有的把大论证拆成小定理，有的去找已有结果，有的写Lean代码。人类数学家处理AI卡住的数学难题，工程师维护系统。最后写出约4310万行代码（推文说约5000万行，博客和官网都是4310万），其中约120万行来自清华大学求真书院团队此前开源的同类项目。AI有时会把还没证明的东西直接当成已知条件用，Axiom发现后删掉了几万行代码重来。用的是哪些AI模型，Axiom没说。 Lean能保证推导的每一步都对，但它判断不了代码开头写的那句“定理”是不是真的就是有限单群分类定理。如果这句话翻译走了样，后面证得再对，证的也是另一件事。这部分只能靠人读。Axiom邀请群论学家和Lean社区自己重跑检查、核对这句话。目前这还是Axiom自己的发布，还没有外部独立核查的结果。

曝光 388 · 评论 5 · 点赞 5 · 书签 0