格隆汇10月31日｜据36氪，人类历史上规模最大的数学证明，现已通过计算机形式化验证。有限单群分类定理（CFSG，Classification of Finite Simple Groups），刚刚被AI彻底形式化！百余名全球顶尖数学家历经大半个世纪、写下长达15000页的「数学天书」，被初创团队Axiom研发的多智能体系统在短短24天内全部跑通。

更让人头皮发麻的是，AI构建了人类史上首个超4000万行的Lean代码库。按代码行数计算，这现在是史上最大的开源软件项目。它的规模超过了 Linux 内核、Chromium、Firefox、LLVM、GCC、FFmpeg 等。它甚至还在原有的证明中揪出了人类的漏洞，并亲自证明了新的数学定理来完成修补！

知名数学家Ken Ono动情发文，悼念今年1月去世的数学家父亲。他回忆起童年时父亲引荐自己走近群论巨匠的岁月，在见证人机协作跨过这条历史终点线时，这位数学大师忍不住当场泪崩。有人为自己的研究被AI “抢先”而崩溃，有人为“发现的快乐”正在消失而悲伤。这些眼泪背后，是数学界对AI时代自身角色和意义的真实焦虑。