Axiom Math's Stacks Project formalization

Axiom Math used a coordinated swarm of AI agents to convert the Stacks Project, a roughly 7,500-page algebraic geometry reference, into a 16-million-line Lean library of computer-verified proofs, released as free open-source software. Every proof is checked by Lean's kernel, with no `sorry` placeholders or `native_decide` present, and each result links back to its original text and dependencies. The agent swarm was organized like an engineering organization, with different agents handling architecture, core definitions, and individual proofs. In the course of formalization, AI agents identified dozens of statements in the original text that required correction. The formalized library is intended as a reusable foundation for further mathematical work. However, Stacks Project original maintainer Johan de Jong asked on October 21, 2026 that contributors not submit AI-generated comments or pull requests to the upstream project.