Axiom Math 发布 Stacks Project 的 16M 行 Lean 形式化库

Rohan Paul· @rohanpaul_ai · X·2026-11-05 01:53· 1 小时前AI 评分59

AI 导读

Axiom Math 发布对整个 Stacks Project 的形式化，共 16M 行 Lean 代码，由其 agent swarm 以类似工程组织的方式分工完成，Lean 逐条检查每个证明。62,975 个 Lean 文件、663,090 个声明建立在 Mathlib 之上，每个带 tag 的结果都链接到原文和依赖。这是免费开源库，后续研究者或 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.

来源：Rohan Paul · x.com