Axiom Math formally verifies the Stacks Project with AI agents

Axiom Math says its AI agents have formally verified the Stacks Project, a large open-source mathematical reference created by Johan de Jong in 2005. The library spans algebra, geometry and number theory, and has grown through contributions from mathematicians. Columbia mathematician Peter Woit has compared its importance with the Bourbaki books.

The company converted about 7,654 pages of material into roughly 16 million lines of Lean code. A proof assistant checks that code line by line, allowing mathematicians to test whether the underlying arguments are logically consistent. Because results in Stacks depend on one another, Axiom had to preserve the links among definitions and theorems throughout the formalization.

Axiom CEO Carina Hong said the agents worked in parallel within a broad hierarchy and identified tasks for themselves. The company also trained its own mathematics-focused models. Axiom says the completed work provides researchers with a foundation for formalizing algebraic geometry, an area with relatively little existing Lean material. The startup argues that verified mathematical libraries could also support future software written by AI agents. Axiom was founded in March 2025, and in March it raised a $200 million Series A led by Menlo Ventures.