16M行形式化代码，Axiom把Stacks Project盖成一座数学城市

Axiom 今天发布了一个 16M 行的 Stacks Project 形式化版本。Stacks Project 是代数几何领域持续多年的大型协作项目，被当作现代数学的关键基础设施。形式化通常指把定义、定理和证明写成机器可检查的代码。

多数人对大规模 vibecoding 的直觉是，量一大，代码就会变成 slop。Axiom 把这个发布当成反例：16M 行，代码质量经过优化，Stacks Project 高度互联的结构也保留了下来。行数只是规模，真正难的是依赖网络别散架。数学形式化像一座城市，单栋楼能盖，路网和管线最难维护。

发布里配了这段视频，把它称作一座数学城市。对做 AI 代码生成的人来说，值得看的是规模化之后结构还能不能读、能不能查、能不能继续长，16M 这个数字本身说明不了太多。Axiom 的发布给出了一个可核对的样本。Yao Fu 转发了这条消息。