Axiom opens a 16-million-line AI-built library for algebraic geometry
The company says coordinated agents formalized every formalizable tag in the Stacks Project, while separating AI-written code from the human-reviewed tier.
Axiom has open-sourced a Lean formalization of the Stacks Project, a sprawling reference for algebraic geometry. The company says the library spans about 16 million lines and covers every Stacks tag with formalizable content.
Unlike a single theorem proof, this release is designed as reusable infrastructure. Researchers can import the library, inspect dependencies and build new machine-checked results on top of it. Axiom says a hierarchical system of specialized AI agents translated statements, searched Mathlib for abstractions, constructed proofs and resolved prerequisites across the project’s dependency graph.
Lean’s kernel checks the proofs, and the repository says they contain no sorry placeholders or native_decide shortcuts. During formalization, Axiom says its system found dozens of statements that needed local refinement, including missing hypotheses and edge cases in positive characteristic.
That does not mean the entire translation has already received independent mathematical review. The repository separates human-reviewed StacksCore modules from AI-written StacksFrontier modules, where review is still needed. Axiom’s claim that this is the largest integrated reusable formal-mathematics library is also the company’s own. Even with those caveats, the project is a striking test of whether coordinated agents can produce coherent, inspectable scientific software at a scale far beyond one theorem.
