Axiom formally verifies the Stacks Project, a 16-million-line Lean library of algebraic geometry
The library gives researchers a machine-checked base for algebraic geometry that did not exist before, and Axiom argues it matters for AI-written software.
Axiom, a startup valued at $1.6 billion, announced it has formally verified the Stacks Project, an open-source mathematics reference begun in 2005 by Johan de Jong. Its AI agents converted roughly 7,654 pages into about 16 million lines of Lean code, which a proof assistant checks line by line. The team had to preserve the many interdependent results across the whole library, and it said the work fills a major gap in formalized algebraic geometry. Axiom argues that verified foundations will matter for software written by AI agents, and CEO Carina Hong challenged other coding companies to attempt formalization at comparable scale.
Why it matters
For mathematicians, the verified library means proofs in algebraic geometry can be checked line by line in Lean instead of relying on manual review alone, and later work can build on a foundation that has already been checked. Axiom's argument is that verified foundations will matter as AI agents write more software, and Carina Hong's challenge to other coding companies suggests the approach may spread beyond mathematics. The story shows an open-source reference being turned into machine-checkable form at scale, a step that changes how that reference can be trusted and reused.
Matters or hype?
Does this story matter, or is it hype? Vote before you see what everyone else said.