1600万行形式化Stacks Project，视频里是一座数学城市

Axiom发布了Stacks Project的1600万行形式化版本。Jeff Dean转发了这条消息。Axiom的说法很直接：多数人认为大规模vibecoding是粗制滥造，这里有个反例。

Stacks Project是代数几何和代数栈领域的开放参考项目，体量大，定义、定理、证明之间互相引用密集。把它形式化，意味着把自然语言写成的数学内容改写成机器可检查的代码。普通读者可以把它理解成给数学证明做机器校验，很多隐含步骤会被逼出来。对开发背景的读者，难点不在行数，而在依赖关系是否完整、证明是否可检查、后续修改会不会连锁崩塌。

Axiom称这个版本保留了优化后的代码质量和高度互联结构。视频里把这个结构比作一座数学城市，道路和建筑之间的关系比单纯的行数更有信息量。

1600万行很容易制造声势。更值得看的是，大规模生成代码之后，结构是否还能维护，证明是否真的能过检查，人工审查成本有没有被转移到别处。如果形式化过程大量依赖模型生成，评估指标就不该只有行数，还要看可检查比例、依赖完整性、重构成本和审查成本。Axiom给出的反例，价值在这里。

原文链接：Jeff Dean 转发 Axiom