Axiom Math wants to keep AI slop out of mathematics

Axiom Math, a $1.6 billion startup, has formally verified the Stacks Project, a comprehensive library of mathematics, using its AI agents. The project, started by mathematician Johan de Jong in 2005, contains 7,654 pages of math, which the AI agents translated into 16 million lines of computer-checked code. This process, called formal verification, ensures the logical soundness of the math.