TechCrunch reports that Axiom Math, an AI startup valued at $1.6 billion, has announced the completion of a full formal verification of the Stacks Project—an open-source mathematics reference book—translating approximately 7,654 pages of content into roughly 16 million lines of code, each verified line by line by the Lean proof assistant.