Axiom Math Formally Verifies Open-Source Math Library The Stacks Project

Axiom Math announced that it has used a multi-agent system to complete the formal verification of the open-source mathematics project The Stacks Project, translating its roughly 7,654 pages into about 16 million lines of computer-checked Lean code. The achievement fills a gap in formal mathematics for algebraic geometry. The team used proprietary mathematical models to allow agents to distribute tasks in parallel within a loose hierarchy while maintaining citation consistency. Axiom plans to use this verification milestone as a foundational layer, gradually expanding into bug-free code verification and scientific discovery.