Axiom Math 发布 Stacks Project 的 16M 行 Lean 形式化库

Axiom Math 发布对整个 Stacks Project 的形式化，共 16M 行 Lean 代码，由其 agent swarm 以类似工程组织的方式分工完成，Lean 逐条检查每个证明。62,975 个 Lean 文件、663,090 个声明建立在 Mathlib 之上，每个带 tag 的结果都链接到原文和依赖。这是免费开源库，后续研究者或 AI 可直接复用已验证的定义和定理来证明新结果。