Stacks Project 全面 Lean 形式化发布：史上最大可复用形式化数学库诞生
talkingdev • 2026-11-05
1478 views
近日，Axiom 宣布已完成对整个 Stacks Project 的 Lean 形式化。Stacks Project 是现代代数几何领域的重要开源参考文献，系统整理了概形、层、上同调等核心理论，是当代数学研究的基础性资源。此次发布将这一长期积累的人类数学成果转化为单一、机器可检查的数学库，成为迄今规模最大的集成式、可复用形式化数学库。研究人员和 AI 代理可以直接将其导入新的形式化证明中，显著降低代数几何形式化工作的门槛，也为人工智能辅助数学推理和发现提供了高质量的基础设施。这一进展标志着形式化数学正从单一定理验证走向学科级知识体系构建，对数学研究与 AI 数学能力的提升都具有重要意义。
核心要点
- Axiom 将整个 Stacks Project 完整形式化到 Lean 中
- 该库是迄今最大规模的集成式、可复用形式化数学库
- 研究人员和 AI 代理可直接导入该机器可检查库用于新证明