Axiom Formally Verifies the Stacks Project With AI Agents

Axiom says it has formally verified the Stacks Project, one of the largest collections of mathematical work, according to TechCrunch. Its AI agents translated roughly 7,654 pages into about 16 million lines of computer checked Lean code.

The Stacks Project is an open source mathematical reference started by Johan de Jong in 2005. It covers algebra, geometry and number theory. Formal verification converts proofs into code that a proof assistant checks line by line for logical consistency.

Axiom assigned its agents a loose hierarchy, allowing them to select tasks and work in parallel while preserving connections among definitions and theorems. The company also trained its own mathematics models and initially used a Lean specialist to guide the agents. The resulting library gives researchers a verified foundation for building further proofs in algebraic geometry.