Axiom Math 发布 Stacks Project 的 1600 万行 Lean 形式化库
Vibe coding at scale has a reputation for slop, so Axiom Math formalized the Stacks Project to show otherwise.
Axiom Math 发布 Stacks Project 的完整形式化版本，共 1600 万行 Lean 代码，保留其高度互联的结构并优化了代码质量。该工作由智能体集群完成，人类负责分配架构、核心定义和单个证明等任务，每个完成的证明都经 Lean 校验，并链接回原文与依赖。这一免费开源库让现代代数几何的大部分内容以计算机可校验的代码形式存在，数学家和 AI 模型可直接复用已验证的定义与定理。
推荐理由
AI 评分 65
Axiom Math 用智能体集群把 Stacks Project 转成 1600 万行 Lean 代码，展示了大规模 vibe coding 在形式化数学上的可行性。
主题
查看原帖大多数人认为大规模 vibecoding 是垃圾。这里有一个反例。 今天我们发布了整个 Stacks Project 的 1600 万行形式化版本——它是现代数学的基础关键设施——代码质量经过优化，其高度互联的结构得以保留。 一座数学之城 🌆 https://t.co/KMTNXpdr6s
查看原文
Most think vibecoding at scale is slop. Here’s a counterexample. Today we release a 16M-line formalization of the entire Stacks Project, critical infra underlying modern math, with optimized code quality and its highly interconnected structure preserved. A mathematical city 🌆 https://t.co/KMTNXpdr6s
正文 · AI 翻译
大规模“氛围编程”素有粗制滥造之名，因此 Axiom Math 将 Stacks Project 形式化，以证明事实并非如此。
数学家通常信任一个证明，是因为专家读过它；Axiom Math 将整个领域的参考书变成了 Lean 代码，因此计算机现在可以逐行确认其逻辑。
Axiom 像运作一个工程组织那样运行其智能体集群，由人类为一些智能体分配架构任务，为另一些分配核心定义，还有一些则负责单个证明。
Lean 会检查每一个完成的证明，每个带标签的结果都链接到其原始文本和依赖项，因此各部分像卢浮宫金字塔的玻璃板一样严丝合缝地拼合在一起。
而且，除非逻辑成立，否则任何内容都不得进入该库。
所有这些意味着，我们现在有了一个免费的开源库，现代代数几何的很大一部分以计算机可校验的代码形式存在，而不再仅仅作为书中的文本。
在实践中，任何想要在这一领域证明新东西的人（无论是数学家还是 AI 模型），现在都可以复用这些已经验证过的定义和定理，而不必从头重建，并且计算机会标记出任何不成立的步骤。