Axiom Math 用 AI 验证 1600 万行 Lean 代码，完成对数学巨著 Stacks Project 的形式化

Axiom Math 已完成对数学巨著 Stacks Project 的形式化，将其约 7,654 页内容转化为 1600 万行可计算机验证的 Lean 代码；该成果覆盖代数几何等关键领域，填补了形式化数学中的“巨大空白”；其验证结果将作为未来 AI 代理构建软件与科学推理的可信赖基础。