Axiom Math 发布 1600 万行 Stacks Project AI 形式化成果

Axiom Math 发布 Stacks Project 完整 AI 形式化成果，生成约 1600 万行可由计算机验证的代码。该成果横跨数百章和数万条结果，并保持高度互联的结构与优化的代码质量。Scobleizer 将其视为“大规模 vibecoding 必然产出垃圾代码”观点的反例，并提出 AI agent 能在这一严谨基础上走多远的问题。