Axiom Math Formalized the Stacks Project to Show Vibe Coding at Scale Can Be Rigorous

Axiom Math has formalized the Stacks Project — a core reference for modern algebraic geometry — into Lean code, so a computer can now verify its proofs line by line. Its agent swarm worked like an engineering org, with humans assigning teams to architecture, core definitions, and individual proofs, and nothing entered the library unless the logic held. The result is a free, open-source library covering a large part of the field, and a counter-example to the idea that vibe coding at scale can only produce slop.

• Rohan Paul2026-11-04 17:53