Axiom用Lean形式化整个Stacks Project

The Stacks Project, Formalized in Lean

Axiom刚刚发布了基于Lean的Stacks Project完整形式化版本，这是数学史上规模最大的集成化形式化库，涵盖约1600万行代码。该项目将现代代数几何的7500页开源参考文献转化为机器可验证的单一库，让研究人员和AI代理能直接导入定义与定理。通过协调部署AI代理群，团队在保持数学严谨性的同时，解决了大规模形式化中的工程挑战。这一里程碑不仅为代数几何及其相关领域提供了全新起点，还通过形式验证发现了原文中的若干疏漏并加以修正，展现了形式化对数学文献的主动完善能力。