AI systems are increasingly producing flawed or incomplete mathematics, but one startup aims to counter that by formalizing huge chunks of the mathematical corpus so machines can use it reliably. Axiom Math has just completed a formal verification of the Stacks Project, transforming its roughly 7,654 pages into about 16 million lines of machine-checked Lean code. The goal: reduce AI “slop” in math working from a foundation mathematicians can trust.
What’s the Stacks Project & Why It Matters
The Stacks Project, begun in 2005 by Johan de Jong at Columbia University, is a major open mathematical reference that spans from college algebra to cutting-edge algebraic geometry and number theory. Scholars have long valued it as foundational work—comparable to the Bourbaki books, for bringing clarity and consistency to modern mathematics.
The challenge is huge. Mathematical texts aren’t just standalone theorems—they’re interconnected, with definitions and proofs depending on earlier ones. Axiom Math didn’t just have to translate each theorem; it had to preserve all of those dependencies within a vast web of logic. That meant keeping consistency across every formalization so no contradictions emerge.
How Axiom Pulled It Off
Formal verification was the technique: converting mathematical texts into code in a proof assistant—specifically Lean—that checks logical soundness step by step. Axiom trained its own models focused on math, and their fleet of AI agents worked in parallel, choosing tasks autonomously. Initially there was concern about preserving the elegance and internal coherence of Stacks when converting to code.
The team structured its verification work hierarchically, but not so rigidly that agents were micromanaged. Agents found subtasks they could tackle in parallel, learning “mathematical taste” first through human mentorship and then through exposure to the formal logic environment itself. That approach helped them fill one of the biggest blank spots in formalized math—algebraic geometry, which until now has lagged behind in formal proof tools.
Broader Implications: Beyond Pure Math
This isn’t just an academic exercise. In software, verified foundations help prevent bugs, security flaws, and unreliable output—issues that loom larger as AI writes more code. A body of rigorously formalized mathematical knowledge means future research and AI-generated proofs or software can build on trustworthy blocks instead of re-deriving everything from scratch.
Axiom Math, founded in March 2025 by Carina Hong, raised a $200 million Series A led by Menlo Ventures earlier this year. The company sees verified math not just as useful for mathematicians, but as essential infrastructure for robust AI systems. As agents become more powerful, sloppy foundations won’t be just undesirable—they’ll be dangerous.
This formal verification of the Stacks Project marks a leap forward—a reusable substrate for mathematics that others can build on. AI agents now have a solid groundwork for algebraic geometry and beyond, which previously was sparsely formalized.
What this means: As computational tools are increasingly tasked with proving new math or generating proofs, reliability becomes paramount. Axiom’s work shows that rigorous formalization is scalable and practical. What to watch: whether the project accelerates formalization in other underrepresented areas, how accessible this codebase is to researchers, and how long it takes for AI systems to start drawing on it meaningfully in research or critical software.
