Axiom 用 AI 智能体集群把整部 Stacks Project 形式化为 Lean：约 1600 万行，称史上最大的可复用形式化数学库
Axiom 于 11 月 4 日（X 官方账号 UTC 17:13 发帖，帖子浏览超 200 万）发布整部 Stacks Project 的 Lean 形式化。这部约 7500 页的代数几何开源参考书由 Johan de Jong 于 2005 年发起，形式化后约 1600 万行代码，官方称是迄今最大的一体化、可复用形式化数学库。工作由分层协调的 AI 智能体集群完成，过程中发现了原文数十处需要局部修正的命题，并给出反例。成果开源，可在 stacks.axiommath.ai 对照原文浏览。
核心要点速览
- 规模：约 7500 页原文、约 1600 万行 Lean 代码，官方称是最大的一体化可复用形式化数学库（厂商自述）。
- 方法：分层 AI 智能体集群并行翻译命题、在 Mathlib 中查找已有抽象、构造证明，并用多智能体审计和与原文的语义交叉检查保证命题忠实。
- 发现：系统找出原文数十处需修正的命题，包括缺失假设、正特征下的边界情况，并为错误处构造了显式反例。
- 保留 Stacks 永久标签结构，每个 Lean 声明都能对应回原文；stacks.axiommath.ai 提供对照阅读和依赖图。
- 这是 Axiom 继 10 月 27 日发布有限单群分类（CFSG）形式化之后的又一大型发布；按 de Jong 的要求，修正内容不直接提交到上游仓库。
关联模型 / 智能体 / 厂商:
