# Axiom将Stacks Project转化为经机器验证的Lean代码

> Axiom称，这项包含1600万行代码的形式化工作，让一部重要的代数几何参考资料可用于Lean验证的证明。

Oossa · 2026-11-05 · https://oossa.com/zh/axiom-turns-the-stacks-project-into-machine-checked-lean-code

Axiom Math发布了Stacks Project的机器验证版本。这是一部重要的代数几何开源参考资料。此次形式化工作将其中的数学内容转化为约1600万行Lean代码，并由证明检查程序逐步验证。Axiom表示，研究人员和AI代理可以将这些成果作为一个相互关联的库，用于构建新的形式化证明。

不同来源给出的页数略有出入：TechCrunch称约为7,654页，Axiom则称约7,500页。这部参考资料由哥伦比亚大学数学家Johan de Jong于2005年启动，之后由数学家们在二十年间不断扩充。Axiom的工作是将已有研究成果形式化，并不意味着AI代理独立发现了其中的基础数学。

## 为什么相互关联的定理库很重要？

证明库的价值不仅在于其中的单个定理已经过验证，还在于后续证明可以复用这些定理及其依赖关系。Axiom表示，该公司保留了Stacks Project的永久标签，将Lean中的声明与原文相应部分关联起来。其网站还允许读者并排查看原文和代码，并了解各项结果之间的依赖关系。

这在代数几何领域尤为重要，因为一项证明可能依赖交换代数、概形、层和上同调等领域中的一长串概念。Axiom称，在此次发布之前，研究人员可用于形式化现代代数几何的Lean基础设施相对有限。该公司的定理库为他们提供了一个起点，无需在每个项目中都重新形式化这些基础内容。

## 为未来的证明和软件打基础

Axiom表示，其代理并行开展工作，完成了数千条定理的转译、证明和整合。据TechCrunch报道，该公司为这些代理提供了较为宽泛的任务框架，让它们自行识别待处理的任务；Axiom还训练了自有的数学专用模型。该公司称，完成后的定理库是规模最大的集成式、可复用形式化数学库；这是Axiom对这次发布的描述。

芯片设计和软件验证等领域也采用了类似的检查方式。Axiom认为，可复用且经过验证的基础有望帮助AI代理构建更可靠的系统，尤其是在它们编写越来越多代码的情况下。但此次发布验证的是经过形式化的Stacks Project，并不意味着AI系统可能生成的每项新数学结论或软件都经过验证。

## 事实

- Axiom将此次发布的日期定为2026年11月4日。
- Lean形式化版本包含约1600万行代码。
- Stacks Project由Johan de Jong于2005年启动，此后不断有数学家参与贡献。
- 据TechCrunch报道，Axiom于2026年3月完成了由Menlo Ventures领投的2亿美元A轮融资。

## 为什么重要

对于从事代数几何研究的数学家来说，这个定理库提供了经过验证、可重复使用的成果，让他们无需在Lean中重新搭建相同的基础。此次发布确认的是这部参考资料的形式化版本，并不能证明未来由AI生成的证明或代码无需检查就值得信赖。

## 来源与参考

1. [Axiom Math wants to keep AI slop out of mathematics](https://techcrunch.com/2026/11/05/axiom-math-wants-to-keep-ai-slop-out-of-mathematics/) – TechCrunch, 2026-11-05
2. [Axiom](https://axiommath.ai/research/the-stacks-project-formalized/?utm_source=openai) – Axiom

最后更新: 2026-11-05