Axiom 发布 1600 万行 Stacks Project 形式化，反击大规模 AI 代码必烂论

Scobleizer · x · 2026-11-05

Axiom Math 发布了对整个 Stacks Project（现代数学的关键基础性形式化工程）的完整 AI 形式化成果：横跨数百章的数万条结果，约 1600 万行可由计算机验证的代码，且保持了高度互联的结构与优化的代码质量。这是对「大规模 vibecoding 必然产出垃圾代码」这一流行观点的有力反例。Scobleizer 评价其像卢浮宫玻璃金字塔——结构精密优美，并好奇在如此严谨的地基上 AI agent 还能走多远。