# Axiom 完成 Stacks Project 的 Lean 形式化，代码约 1600 万行

> 原标题：The Stacks Project, Formalized in Lean

- 来源：Hacker News 首页
- 发布时间：2026-11-05T16:16:59.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/wntelzs3gp9mmmrtiilrl4vxx
- 原文：https://axiommath.ai/research/the-stacks-project-formalized/

## 摘要

Axiom 发布整个 Stacks Project 的 Lean 形式化开源库，将约 7,500 页代数几何参考文献转为约 1600 万行机器检查代码。研究人员和 AI 智能体可直接导入定义与定理，并在 stacks.axiommath.ai 查看原文与 Lean 代码的对应关系及交互式依赖图。