Axiom Math 将 Stacks 项目形式化为 Lean 机器校验的开源库
Axiom Math 用一队 AI 智能体把整个 Stacks Project 改写成 Lean 代码，机器逐行验证证明，现在免费开源，做数学的人可以直接复用。
Axiom Math 用智能体集群把代数几何参考书 Stacks Project 整体转写为 Lean 代码。团队按工程组织分工，不同智能体分别负责架构、核心定义和具体证明，Lean 逐条校验逻辑后才收入库中。每条被标记的结果都链接回原文及其依赖，形成可追溯的结构。这个免费开源库让后续研究者或 AI 模型能直接复用已验证的定义和定理来证明新命题。
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.
