16M行形式化代码，Axiom把整座数学城市搬进机器

Axiom在X上发布了一个16M行的形式化项目，对象是整个Stacks Project。Turing Post转发了这条发布。

先补上下文。Stacks Project是代数几何领域长期协作的参考文本，研究者用它查定义、定理和证明。形式化指把这些内容写成机器可检查的代码。16M行这个量级已经超出示例代码，属于一整套需要互相引用的文本被搬进代码库。

Axiom在推文里给的判断更直接：很多人觉得大规模vibecoding是slop，这个项目是反例。它说代码质量做了优化，Stacks Project高度互联的结构也保留下来。

对形式化项目，结构比行数更难。定义、定理、证明之间要能互相引用，改一处可能牵动一片。Axiom把“保留互联结构”单独拿出来说，说明他们知道难点在哪。行数本身不说明质量，16M行也不是自动加分项。可检查、能定位、依赖清楚，才决定这套东西能不能用。如果只比行数，很多仓库都能赢；难的是让每一行挂到该挂的位置。

画面把项目比作一座数学城市。普通读者可以把它理解成：每栋楼、每条路、每根管线都有编号，还保留它们之间的连接关系。AI从业者更该看的是，这种项目给代码生成提供了一个压力测试场景：规模大、关系密、错误不能靠肉眼糊过去。

来源：Turing Post 转发 Axiom 发布