Axiom Math wants to keep AI slop out of mathematics

Axiom Math, a startup valued at $1.6 billion, has formally verified the Stacks Project—one of the largest human-written mathematical libraries—by translating its 7,654 pages into approximately 16 million lines of computer-checked Lean code using AI agents. Formal verification, akin to methods used in chip design and software debugging, ensures logical soundness by having a proof assistant check each line. The Stacks Project, started in 2005 by Johan de Jong, covers algebra, geometry, and number theory, and its interconnected theorems posed a significant challenge for Axiom's agents, which worked in parallel under a loose hierarchy and were trained to develop mathematical taste. The achievement fills a major gap in formalized algebraic geometry and provides a reusable, verified foundation for future proofs and AI-generated software, addressing concerns about "AI slop" by enabling agents to build on trustworthy mathematics rather than starting from scratch.

(Source：TechCrunch)