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
正文
Vibe coding at scale has a reputation for slop, so Axiom Math formalized the Stacks Project to show otherwise.
Mathematicians usually trust a proof because experts read it; Axiom Math turned an entire field’s reference book into Lean code, so a computer can now confirm the logic line by line.
Axiom ran its agent swarm like an engineering org, with humans assigning some agents the architecture, others core definitions and others individual proofs.
Lean checks every completed proof, and each tagged result links to its original text and dependencies, so the pieces fit together like panes of the Louvre’s pyramid.
And nothing entered the library unless the logic held.
All these means that now we have a free, open-source library where a big chunk of modern algebraic geometry exists as computer-checked code instead of only as text in a book.
In practice, anyone (a mathematician or an AI model) who wants to prove something new in this field can now reuse these already-verified definitions and theorems instead of rebuilding them, and a computer will flag any step that doesn’t follow.