Axiom Math 用 AI 将 Stacks Project 转化为可验证 Lean 代码库

Axiom Math 将代数几何参考书 Stacks Project 转化为约 1,575 万行 Lean 代码库，覆盖书中所有具备可形式化内容的标签。该代码库建立在 Mathlib 之上，分为经人工核验的 StacksCore 和由 AI 智能体编写、待审查的 StacksFrontier 两层，每条证明都由 Lean 内核检查。