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

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系统可能生成的每项新数学结论或软件都经过验证。