Sheaves

Axiom 使用 Lean 将 7500 页的 Stacks Project 正式化，创建了最大的数学库

Axiom 已将整个 Stacks Project（代数几何学的基本参考资料）正式化并发布到 Lean 证明助手。这个庞大的库包含 1600 万行代码，代表了迄今为止最大规模的集成和可重用形式化数学集合。该项目旨在使现代代数几何学更容易进行形式验证，尤其是在 AI 系统日益生成数学论证的背景下。