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
正文 · AI 翻译
Axiom 发布了一个开源 GitHub 仓库，数十个 AI 智能体在 24 天内将一份 15,000 页的数学证明转化为约 4300 万行代码。
该证明被称为有限单群分类，耗费 100 位数学家数十年时间，列出了数学中所有基本的对称性构建块。
代码用 Lean 编写，这是一种会检查证明每一步的编程语言，使得整个结果可以通过运行代码来验证，而无需重读数百篇论文。
Axiom 的图表追踪了自 2025 年年中以来 AI 编写的 Lean 项目规模的增长情况，据其估算大约每 37 天翻一番，而该项目达到了 4300 万行。