Axiom Math 发布 Stacks Project 的 Lean 形式化版本

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.