Axiom 开源仓库：多个 AI 智能体用 24 天将 1.5 万页数学证明转为 Lean 代码
几十个 AI 智能体 24 天写了 4300 万行 Lean 代码，把数学家几十年的证明变成可运行验证的代码，仓库已开源可以去看。
Axiom 发布了一个开源 GitHub 仓库，其中几十个 AI 智能体用 24 天把 15,000 页的有限单群分类证明转换成约 4300 万行代码。该证明原本由 100 名数学家耗时数十年完成，罗列了数学中对称性的所有基本构件。代码使用 Lean 编写，这种语言能逐步校验证明，运行代码即可验证整个结果，无需重读数百篇论文。Axiom 的图表显示，自 2025 年年中以来，AI 编写的 Lean 大型项目大约每 37 天翻一倍。
Axiom released an open-source GitHub repo where dozens of AI agents turned a 15,000-page math proof into about 43 million lines of code in 24 days.
The proof, known as the Classification of Finite Simple Groups, took 100 mathematicians several decades and lists every basic building block of symmetry in mathematics.
The code is written in Lean, a programming language that checks every step of a proof, allowing the whole result to be verified by running the code instead of rereading hundreds of papers.
Axiom's chart tracks how large AI-written Lean projects have grown since mid-2025, roughly doubling every 37 days by its estimate, with this project reaching 43 million lines.
