Axiom 将约 7500 页的 Stacks Project 全量形式化进 Lean

Axiom 发布 Stacks Project 的 Lean 形式化版本，把这份约 7500 页的代数几何基础参考书变成单一机器校验库，代码规模约 1600 万行，称其为迄今最大的可复用形式化数学库。每个 Lean 声明通过永久 Stacks 标签回链原文，研究者和 AI 智能体可直接导入其中的定义与定理。团队用协同的 AI 智能体集群并行翻译、证明并整合数千条定理。