1600万行代码，把现代数学基础设施做成一座可导航的城市

Axiom 发布了一个覆盖整个 Stacks Project 的形式化版本，1600 万行。Thomas Wolf 转发了这条消息，并把它当作大规模 vibe coding 的反例。所谓 vibe coding，通常指让模型大量生成代码，人靠感觉和测试兜底。推文原话很直接：“Most think vibecoding at scale is slop. Here’s a counterexample.”

Stacks Project 是代数几何和代数栈领域长期协作的参考项目，很多人把它看作现代数学的基础设施。形式化通常指把定义、定理和证明写成证明助手能检查的代码。难点不止在篇幅：这些内容高度互相依赖，抽掉一条引理，周围一片定义和证明都会失去上下文。Axiom 说这次保留了这种高度互联的结构，同时优化了代码质量。视频里把它呈现成一座数学城市，定理和定义像建筑，依赖关系像道路。

1600 万行听起来像典型的规模叙事。行数当然好传播，但它只是表面积。形式化项目真正难的地方在规模上来之后，依赖关系还能不能导航，证明还能不能复现，后来者还能不能接着往上盖。把整座城市摊成互不相连的文件夹，行数再多也只是废墟。Axiom 给出的信号是，这套东西没有散架。

对做 AI 和写代码的人来说，这条消息值得看的地方也在这里。大规模生成代码常被质疑为 slop，质疑合理。这次案例不能证明所有 vibe coding 都靠谱，它只说明在特定任务、特定约束下，规模和质量可以同时成立。判断产出仍然要看结构、可维护性和可验证性，别只看生成量。

原推文