Axiom 完成 Stacks Project 的 Lean 形式化，代码约 1600 万行

The Stacks Project, Formalized in Lean

Axiom 发布整个 Stacks Project 的 Lean 形式化开源库，将约 7,500 页代数几何参考文献转为约 1600 万行机器检查代码。研究人员和 AI 智能体可直接导入定义与定理，并在 stacks.axiommath.ai 查看原文与 Lean 代码的对应关系及交互式依赖图。