Axiom 将约 7500 页的 Stacks Project 完整形式化为 Lean 库

Axiom 发布 Stacks Project 的 Lean 形式化版本，把这部约 7500 页的代数几何开源参考书变成单一机器校验库，代码约 1600 万行。该库保留原书永久标签，可把每条 Lean 声明映射回原文，研究者与 AI 智能体可直接导入定义和定理。项目由分层协作的 AI 智能体并行完成翻译与证明，过程中发现数十条需要补充假设或修正的陈述，并构造反例。