Axiom 发布 Stacks Project 的 Lean 形式化库

Axiom 发布 Stacks Project 的完整 Lean 形式化版本，覆盖约 7500 页代数几何基础文献，代码规模约 1600 万行，称其为目前规模最大的可复用形式化数学库。该库保留原文本的永久 Stacks 标签，每个 Lean 声明可回溯到对应原文，研究者与 AI 智能体可直接导入定义和定理。Axiom 表示通过分层多智能体协同完成翻译与证明，并在过程中发现数十处原文陈述需要补充假设或修正。