Axiom 开源仓库：数十个 AI 智能体 24 天生成约 4300 万行 Lean 代码
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.
Axiom 发布一个开源 GitHub 仓库，数十个 AI 智能体在 24 天内把 1.5 万页的有限单群分类证明转成约 4300 万行代码。代码用 Lean 编写，可逐步校验证明，整个结果通过运行代码验证而非重读数百篇论文。Axiom 的图表追踪 2025 年年中以来 AI 编写的 Lean 项目规模，按其估算约每 37 天翻一倍。
查看原帖CFSG 的正式证明如今或许已跻身有史以来规模最大的开源项目之列。观看智能体们将其组装起来，会让人想起其背后那令人敬畏的人类成就。这张图代表了数学家们数十年来发展出的约 15,000 页错综复杂的论证。https://t.co/13THDKI50f
查看原文
The formal proof of CFSG may now be among the largest open-source projects ever. Watching agents assemble it is a reminder of the awe-inspiring human achievement behind it. The graph represents some 15,000 pages of intricate arguments developed by mathematicians over decades. https://t.co/13THDKI50f
正文
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.