Axiom Math wants to keep AI slop out of mathematics

Axiom Math, a $1.6B startup founded in March 2025 by Stanford math Ph.D. dropout Carina Hong, announced it has formally verified the Stacks Project, translating its roughly 7,654 pages into about 16 million lines of computer-checked Lean code using a fleet of AI agents. The company argues that verified results become building blocks for future proofs and that the approach can extend to software written by AI agents.