Axiom 在 GitHub 上开源了一个仓库，几十个 AI 智能体在里面干了 24 天，把一份 15000 页的数学证明变成了约 4300 万行代码。

打开网易新闻 查看精彩图片

这份证明叫有限单群分类定理（Classification of Finite Simple Groups），由 100 位数学家花了几十年完成，内容是把数学中所有基本的对称性构建块列出来。

代码用 Lean 写成。Lean 是一门会逐步检查证明过程的编程语言，这意味着整个结果可以通过运行代码来验证，而不必重读几百篇论文。

Axiom 还放出了一张图表，追踪自 2025 年年中以来 AI 编写的 Lean 大型项目规模如何增长。按它的估算，这些项目大约每 37 天翻一倍，而这个项目达到了 4300 万行。

有限单群分类定理的形式化证明，如今可能已经跻身有史以来最大的开源项目之列。看着智能体们把它拼装出来，会让人想起背后那个令人敬畏的人类成就——那张图代表的，是数学家们用几十年时间发展出的约 15000 页复杂论证。