近一个月以来，AI 正逐步探入数学研究的腹地。10 月 6 日，OpenAI 在代码托管平台 GitHub 上一次性公开了 722 份由内部模型生成的数学手稿，涉及数百个开放问题；10 月 26 日，OpenAI 团队又公布了其模型在调和分析、计算复杂性理论和量子场论上的新发现。
AI 产出证明的速度越来越快，如何确认这些证明可信，就成了数学界必须面对的问题。
其中一种应对办法是形式化验证，即借助证明助手 Lean 等工具，把数学家用自然语言写成的证明逐句“翻译”成计算机能够检查的形式语言。论文中常见的“显然”“同理可得”在 Lean 里行不通，任何省略的推导和隐含的条件都必须写明，每一步推理都要经过 Lean 内核的逐条检查才算通过。
10 月 27 日，美国 AI 数学公司 Axiom 公开了一项体量罕见的成果，宣布其 AI 智能体已在 Lean 中为有限单群分类定理（CFSG）完成了完整的形式化。CFSG 的原始证明约 15,000 页，分散在 500 多篇论文中，出自约 100 位数学家之手，是人类数学史上篇幅最长的证明，人称“巨型定理”。
Axiom 的工程师和数学家调度数十个 AI 智能体，用 24 天写出约 4,310 万行 Lean 代码，目前已在 GitHub 将其开源。
一份没人能读完的证明
数学家用“群”描述对称性。一个正方体有 24 种旋转方式能让它看上去和原来一模一样，这 24 种旋转连同它们的组合规则就构成一个群。整数可以分解为质数的乘积，有限群也可以层层拆解，最终得到无法再拆分的基本单元，即有限单群。
CFSG 给出了所有有限单群的完整名录：素数阶循环群、交替群、16 个由有限域构造的李型群家族，外加 26 个不属于任何家族的“散在群”。其中最大的魔群（Monster group）约有 8×1053 个元素。数学家常把这份名录比作对称性的元素周期表。
列出名录相对容易，难的是证明名录之外再无遗漏。这项工作从 20 世纪 50 年代起步，约翰·汤普森（John Thompson）因奠基性贡献获得 1970 年菲尔兹奖和 2008 年阿贝尔奖。1983 年，群论学家丹尼尔·戈伦斯坦（Daniel Gorenstein）宣布分类完成，但很快有人发现，其中“拟薄群”一类情形只依靠一份未完成的手稿。
这个缺口直到 2004 年才由迈克尔·阿施巴赫（Michael Aschbacher）和斯蒂芬·史密斯（Stephen Smith）用一部 1,221 页的专著补上，2008 年学界又修补了另一处漏洞。这些论文和专著共同构成了如今所说的“第一代证明”。
证明的分散也成了难题：不同年代的论文使用不同的记号和组织方式，结论之间层层引用，弄清它们如何拼接需要深厚的专门知识。
从 20 世纪 80 年代末开始，参与分类工作的学者着手撰写更系统的“第二代证明”，到 2023 年已出版 10 卷，预计至少需要 12 卷，至今仍未写完。与此同时，代数、数论、组合数学乃至数学物理中的大量结论都以 CFSG 为前提。
一家想“形式化验证一切”的公司
Axiom 成立于 2025 年 3 月，创始人兼 CEO 洪乐潼（Carina Hong）是在广州长大的 00 后。她高中时入选广东数学奥林匹克省队，在麻省理工学院（MIT）用三年修完数学与物理双学位，因本科期间的研究获得美国本科生数学研究最高奖项摩根奖（Morgan Prize），并以罗德学者身份赴牛津大学深造，在进入斯坦福大学读博期间辍学创业。
公司的“创始数学家”、数论学家小野健（Ken Ono）2025 年离开弗吉尼亚大学加入 Axiom，洪乐潼本科期间曾在他主持的暑期科研项目中做研究。公司先后完成 6,400 万美元种子轮和 2 亿美元 A 轮融资，估值已超 16 亿美元。
Axiom 把“形式化验证一切”当作使命，其智能体系统 AxiomProver 能调度多个 AI 智能体协同完成大型形式化任务。今年 8 月，团队完成了素数间隙领域“246 定理”的形式化，这一定理表明存在无穷多对相差不超过 246 的素数。
用小野健的话说：世界即将运行在没人读过的代码之上，证明的形式化是应对这一挑战的试验场。
CFSG 把这个试验场推到了极限。它体量最大、结构最分散，真正能读懂全部论证的人却越来越少。项目核心成员瓦西里·伊林（Vasily Ilin）在社交媒体上写道，真正理解这个证明的人大多已经退休或离世。在一份靠集体记忆维系的证明上做机器核验，对数学界是一项基础建设，也是对Axiom技术能力最直接的检验。
24 天里，推倒再重来
Axiom 并非从零起步。Lean 社区数百位贡献者共同维护的数学库 Mathlib 提供了大量基础定义和定理。在丘成桐的倡导下，清华大学求真书院学生联合丘成桐数学科学中心等机构推进的 CFSG 形式化项目此前已积累了大量群论代码，Axiom 将其中约 120 万行纳入了自己的工程。
团队参照第二代证明的多卷著作绘制了一张证明地图，把整套论证拆成 108 个里程碑、约 380 项子任务。但由于第二代证明尚未写完，形式化的对象定为第一代证明。
10 月 2 日，第一批智能体集群上线。负责统筹的智能体拆解复杂论证、审核待证命题的表述，其余智能体检索已有结论、编写 Lean 代码。某项任务依赖尚未完成的前置结论时，系统会把这部分交给其他智能体，完成的结果汇入共享代码库供后续调用。人类数学家处理数学上的卡点，工程师维持系统运转。
起初的推进并不顺利。早期一些看似可控的里程碑背后藏着大量尚未证明的前提，智能体直接把它们当成既定事实写了下去。团队删掉了建立在这些假设上的数万行代码，部分工作因此必须推倒重来。
10 月 10 日，项目频道里传来消息，魔群的单群性证明完成。智能体还同时证明了魔群的存在，这是整个分类中最关键的环节之一。
公司记录显示，3 天后，进度突然陷入停滞，当天只完成了 1 个里程碑。工程师很快意识到，问题出在里程碑划分过粗，剩余工作量难以判断，于是他们重新规划，把未完成的里程碑拆成更小、表述更精确的定理。
代码规模膨胀也带来了新的问题。智能体写证明的速度超过了 Lean 重新检查的速度，改动一处共享结论，所有依赖它的内容都要重新校验，分布在不同机器上的智能体还会重复计算。工程师为此搭建了缓存分发系统，未改动的代码直接复用此前的检查结果，整体校验速度提升了几个数量级。
10 月 26 日，形式化完成。Lean 内核确认，从基础公理出发直到最终的分类定理，所有推理环节首尾相接。形式化陈述是否准确表达了数学家心目中的 CFSG，仍需要人类审阅，Axiom 在发布时邀请群论学者和 Lean 社区重新运行检查，并核对定理陈述与原定理是否一致。
逐行核对的过程，也是对文献的一次彻底体检。智能体在形式化中记录下大量疑点，其中不少源于智能体自身的误读，需要人工逐一排查。已得到确认的问题大多是笔误、表格数据错误和遗漏的前提条件，另有 34 处与已发表文献的偏差需要专门处理。Axiom 表示将与群论学者合作，把整理好的勘误表公开给学界。
最棘手的问题出现在非平衡群定理（Unbalanced Group Theorem）。分类证明的基本思路是反证：假设存在一个不在名录上的单群，取其中最小的一个，再逐一排除它可能具有的结构。非平衡群定理负责排除其中一大类情形，是通往最终结论的必经环节。
团队沿用群论学家约翰·沃尔特（John Walter）1986 年的论证，智能体却在其中一条断言上找到了明确的反例。原文认为某种操作产生的单群始终留在一个特定的群族之内，实际上它可以产生恰好被排除在该族之外的群。反例没有推翻定理本身，但原论证的关键一步失去了依据。
换一条已发表的证明路线并不轻松，每条新路线都会牵出一批尚未形式化的前置结果，工作量可能成倍增长。
团队为此请教了当年参与分类工作的理查德·莱昂斯（Richard Lyons）和罗纳德·所罗门（Ronald Solomon）。理查德帮助梳理了可行的证明路线及其历史脉络，罗纳德 1976 年提出的“极大 2-分量”理论则提供了替代论证的核心思路。
AxiomProver 据此构造并形式化了一条新的论证路线，其间证明了一个此前没有的群论结果，相关论文已发布在预印本平台 Hexagon。
形式化完成后，Axiom 的数学家又在第一代证明的方法框架内找到一条更短的推导，不借助这一新定理也能得到所需结论，论文因此同时保留了两条路线。
谁来理解机器写下的证明？
就在 Axiom 发布成果的前一周，陶哲轩与邓煜在非营利机构 SAIR 基金会（SAIR Foundation）的播客中讨论了 AI 与数学的关系。OpenAI 的批量发布此前已在数学界引发激烈争论，9 月，两人与其他 23 位菲尔兹奖得主联名发表声明，批评 AI 公司把攻克数学难题当作模型能力的基准测试。
邓煜在对谈中区分了两条边界：一条圈定已经有证明的问题，另一条圈定人类能够理解其证明的问题。过去，两条边界几乎重合，有证明就有人懂；但如今出现了只有 AI 才懂的证明，两条边界开始分离。
他认为，AI 能把事情做好的前提，是人类已经充分理解问题、手里有证明的整体思路。陶哲轩则把 AI 公司批量解题的产出形容为模型训练中的某种“有毒废料”，最终要由数学家来消化处理。他希望 AI 公司在项目启动之初就请数学家加入，避免事后由学界收拾残局。
CFSG 项目和两人描述的理想状态有不少重合之处。它处理的是一份已有路线图的证明，第一代证明和第二代证明的多卷著作为智能体指明了方向；原始证明的参与者在关键节点介入，并将继续以顾问身份参与勘误整理。形式化过程也从方法层面回应了数学界对 AI 证明难以核验的担忧。
今年 6 月，得到国际数学联盟（IMU）支持的《AI 与数学莱顿宣言》将结果不可靠列为 AI 带来的风险之首，并强调人类应当为数学结论的正确性负责。
CFSG 被多个数学细分领域引用了几十年，但它却一直分散在数百篇论文中，没人能完整核验所有结论。如今，所有前提条件、推导依赖都变成了可追溯的代码，任何研究者可以顺着依赖链查到每一步论证的源头，也可以直接复用已完成的数学模块开展后续研究。正如 Axiom 在公告中所写：这不是故事的终点，群论领域的工作仍在继续。
数学的可靠性长久以来建立在同行之间的信任上，人们相信审稿人读懂了论证，相信前人没有出错。
但当越来越多的证明出自机器之手，这份信任需要新的支点，比如一份任何人都能重新运行、逐步核对的形式化证明。如果 AI 能接手繁琐的验证过程，数学家就能留出更多心力解决机器尚不擅长的事：提出值得追问的问题，同时在证明之外寻求理解。
参考内容：
https://axiommath.ai/research/the-enormous-theorem-formalized/
https://github.com/AxiomMath/CFSG
https://hexagonmath.org/2610.00575?version=1
https://spectrum.ieee.org/axiom-math-246-theorem-formalization
https://www.thepaper.cn/newsDetail_forward_34296807
https://leidendeclaration.ai/
注：首图/封面由 AI 辅助制作
热门跟贴