Axiom Math 发布 Stacks Project 形式化库 1600 万行代码验证代数几何
Axiom Math 利用智能体集群将现代数学核心参考书《Stacks Project》转化为 1600 万行 Lean 代码，实现了大规模代数几何知识的计算机可验证形式化。该项目通过模拟工程组织的多智能体协作模式，确保了逻辑的严格性与开源可用性，为 AI 辅助数学证明提供了坚实的基础设施。
报道正文
Rohan Paul (@rohanpaul_ai) · 2026-11-04 17
大规模“氛围编程”（Vibe coding）常因产出质量低劣而饱受诟病，因此 Axiom Math 将 Stacks Project 形式化，以证明并非如此。
数学家通常因为专家审阅过证明而信任其正确性；Axiom Math 则将整个领域的参考书转化为 Lean 代码，使得计算机现在可以逐行确认逻辑。
Axiom 像运营一个工程组织那样运行其智能体集群（agent swarm），由人类分配部分智能体负责架构设计，其他智能体负责核心定义，还有部分负责单个证明。
Lean 会检查每一个完成的证明，且每个标记的结果都链接到其原始文本和依赖项，因此这些组件就像卢浮宫金字塔的玻璃面板一样严丝合缝地组合在一起。
除非逻辑成立，否则没有任何内容会被纳入该库中。
这意味着我们现在拥有一个免费、开源的库，其中现代代数几何的大部分领域不再仅仅以书本中的文本形式存在，而是以经过计算机验证的代码形式存在。
在实践中，任何想要在该领域证明新定理的人（无论是数学家还是 AI 模型），现在都可以复用这些已经验证过的定义和定理，而不必重新构建它们，并且计算机会标记出任何不符合逻辑的步骤。
↳ 引用 @axiommathai (Axiom): 大多数人认为大规模的 vibe coding 只是垃圾。这里有一个反例。
今天，我们发布了整个 Stacks Project 的 1600 万行形式化代码，这是支撑现代数学的关键基础设施，同时保留了优化的代码质量及其高度互联的结构。
一座数学之城 🌆
