数学 · 4310 万行 Lean 代码跑通了一部 15000 页的天书

把这套代码库打印出来，A4纸单面印，一页50行，能摞出一座86米高的纸塔——六分之一座上海中心。这就是4310万行Lean代码的物理体积。（原帖首段的1300米量级算错了：4310万行按每页50行是86.2万页，每页约0.1毫米，摞起来86米。数学没算错，比喻算错了。）它的内容是有限单群分类定理（CFSG）的完整形式化验证——百余名数学家跨越半个世纪写下的约15000页证明，被一个多智能体系统在24天内全部跑通。【直引：36氪10-31报道、DeepTech10-29、Axiom官方研究页】

定理的份量

CFSG被叫做「巨型定理」。约100位数学家在500多篇论文里拼出完整证明，1983年宣布完成，之后发现拟薄群情形只靠一份未完成手稿，直到2004年Aschbacher与Smith用1221页补上。此前没有人能完整通读它——它分散在半个多世纪的期刊里，靠数学共同体的分工互信维持整体成立。【直引：公开数学史表述】核心成员Vasily Ilin的那句话最重：真正理解这个证明的人大多已经退休或离世。在一份靠集体记忆维系的证明上做机器核验，是基础建设。

10月1日启动，人类把「巨型」拆成108个里程碑、约380个子任务；10月2日蜂群上线：领头agent拆解高难论证，其余agent检索已有结果或写Lean代码，未证明的先决条件自动外包；10月10日频道消息「我们证明了魔群是单群」；10月26日全部完成，Lean内核确认从基础公理到分类定理首尾相接。【直引：Axiom官方时间线】工程底账也核了：复用Mathlib与求真书院CFSG项目的约120万行，走Lean v4.35.0-rc3，全量构建不到24小时。按声明数，这是史上最大的开源软件项目——超过Linux内核与Chromium。

两个被低估的细节

第一，AI产出过快，Lean依赖重检出现算力瓶颈，团队被迫自研分布式缓存把校验速度提升几个数量级。验证速度跟不上生成速度，这在形式化历史上第一次成为工程问题。【直引：DeepTech复盘】第二，过程中揪出人类原证明的34处值得注意的偏差：多数是笔误、表格错误、遗漏前提，最棘手的一处在非平衡群定理——沿用John Walter 1986年的论证时，agent找到一个明确反例PSL2(49)，原文的关键闭包断言失效。团队请教了当年参与分类的Richard Lyons与Ronald Solomon，基于Solomon 1976年的理论让AxiomProver构造并形式化了一条新路线，期间证明了一个此前没有的群论结果「simple tops的保持性」，预印本已挂在Hexagon；后来数学家又找到一条更短的老路线，论文两条并存。【直引：Axiom研究页与i10X核】机器不只是验算器，第一次当了合作研究员。

与此前事件的坐标

8月Axiom完成246素数间隙定理形式化（验证人类已有证明）；10月下旬Resolution的agent用约一周自动形式化Hironaka奇点消解，60万行、13.5万美元token费（自报）；10月26到27日OpenAI与Anthropic发布推翻ETH的确定性算法结果附Lean机检。从一道定理到一部天书，间隔三个月。【直引：Import AI 478等】瓶颈从「能不能」移到了「多久多少钱」。要如实记录的边界：这套证明尚未被独立重建，Axiom未披露用了哪些模型与多少算力，形式化陈述是否准确表达了数学家心目中的CFSG仍待群论学者复核——公司自己也发了邀请。

数学界在消化什么

Ken Ono发文悼念今年1月去世的父亲，回忆父亲引他走近群论巨匠的岁月，在人机协作跨过终点线时当场落泪。有人因研究被AI抢先而崩溃，有人为「发现的快乐」消失而悲伤。情绪背后是结构问题：当验证可以批量完成，数学家向「选择哪些问题值得形式化、如何把结果反馈回人类理解」迁移。邓煜在播客里划的两条边界最清楚——有证明的问题，与人类能理解证明的问题，过去重合，如今分离。【直引：36氪转述】

小贴士：有限单群是「积木块」级别的对称结构，所有有限群都由它们搭建。分类定理相当于给元素周期表做了一次完备普查。魔群是表中最大的散在单群，元素个数约8后面跟53个数字。

参考

• 36氪：《AI补全人类史上最大数学证明》（10-31）
• DeepTech深科技：《24天写4310万行代码》（10-29）
• Axiom官方研究页与GitHub仓库AxiomMath/CFSG
• i10X News：34处偏差、2.05百万声明、独立复现缺位的快评
• Import AI 478：Resolution奇点消解形式化（60万行/13.5万美元）

一句话收束：15000页写了半个世纪，4310万行写了24天。纸塔的真实高度是86米，两座塔底下的数学是同一座。