Axiom Math 发布 Stacks Project 的 16M 行 Lean 形式化库

Rohan Paul· @rohanpaul_ai · X·2026-11-05 01:53· 1 小时前AI 评分59

AI 导读

Axiom Math 发布了对整个 Stacks Project 的形式化，共 16M 行 Lean 代码，由其 agent swarm 以类似工程组织的方式分工完成，Lean 逐条检查每个证明。62,975 个 Lean 文件、663,090 个声明建立在 Mathlib 之上，每个带 tag 的结果都链接到原文和依赖。这是免费开源库，后续研究者或 AI 可直接复用已验证的定义和定理来证明新结果。

正文 · 原文

大规模 vibe coding 素有粗制滥造之名，Axiom Math 形式化 Stacks Project 正是为了证明并非如此。

数学家通常信任一个证明，是因为专家读过它；Axiom Math 把整个领域的参考书变成了 Lean 代码，因此计算机现在可以逐行确认其逻辑。

Axiom 像工程组织一样运作其 agent swarm，由人类分配部分 agent 负责架构，另一些负责核心定义，还有一些负责单个证明。

Lean 检查每一个完成的证明，每个带 tag 的结果都链接到其原文和依赖，因此各部分像卢浮宫金字塔的玻璃板一样严丝合缝。

而且只有逻辑成立的内容才能进入该库。

所有这些意味着，我们现在有了一个免费的开源库，现代代数几何的很大一部分以计算机检查过的代码形式存在，而不再只是书中的文字。

在实践中，任何想在该领域证明新东西的人（数学家或 AI 模型）现在都可以复用这些已经验证过的定义和定理，而不必从头重建，计算机将标记任何不成立的步骤。

引用Axiom@axiommathai

大多数人认为大规模 vibecoding 是粗制滥造。这里有一个反例。今天我们发布了整个 Stacks Project 的 1600 万行形式化，这是现代数学背后的关键基础设施，代码质量经过优化，其高度互联的结构得以保留。一座数学之城 🌆

在 X 查看被引用的帖子

来源：Rohan Paul · x.com