Axiom Math scales formal verification to clean up AI-generated math

Axiom Math has announced the formal verification of the Stacks Project, one of the most comprehensive human-written mathematics libraries in existence. By turning thousands of pages of proofs into computer-checked code, the startup aims to provide a robust foundation for AI agents to rely on, preventing the spread of unverified AI-generated content.

• The team converted approximately 7,654 pages of the Stacks library into 16 million lines of computer-checked Lean code.
• Axiom’s AI agents autonomously identified and performed tasks in parallel to verify interconnected theorems.
• The project fills a massive gap in formal algebraic geometry, creating a reusable substrate for future research.
• CEO Carina Hong has challenged other coding companies to embrace formalization at a similar scale to improve AI reliability.

Building on a Verified Foundation Formal verification allows mathematicians to rewrite proofs in the Lean programming language, where an automated assistant checks for logical consistency. The Stacks Project, a community-driven resource, serves as a cornerstone for modern mathematics. Before Axiom’s intervention, the interconnected nature of these theorems made systematic verification a significant challenge.

How the AI Agents Succeeded Unlike traditional methods, Axiom trained its own models specifically to understand mathematical logic. By providing agents with a loose structure and enabling them to work in parallel, the team ensured the system could maintain consistency across 16 million lines of code. The agents learned to distinguish between valid logical chains and potential paradoxes over time.

Impact on Developers and Science This work is a critical step toward ensuring that future AI-written software is free of bugs and security vulnerabilities. Axiom argues that as AI agents perform more complex reasoning, they require a reliable, reusable library of verified facts to prevent them from producing flawed or unreliable results.