Axiom 发布了一个开源的 GitHub 仓库，其中数十个 AI 代理在 24 天内将一份 15,000 页的数学证明变成了约 4300 万行代码。

这项被称为“有限单群分类”的证明花费了 100 名数学家几十年的时间，列出了数学中对称性的每一个基本构建模块。

该代码是用 Lean 编写的，这是一种可以检查证明每一步的编程语言，允许通过运行代码而不是重新阅读数百篇论文来验证整个结果。

Axiom 的图表追踪了自 2025 年年中以来，AI 编写的 Lean 项目的增长规模，据其估计，大约每 37 天翻一番，该项目达到了 4300 万行。