Axiom Math Formally Verifies Stacks Project with AI Agents
Artificial intelligence startup Axiom Math has formally verified the Stacks Project, translating one of the largest collaborative mathematical libraries into computer-checked software. The $1.6 billion startup stated that it completed the milestone on Wednesday, aiming to build a verified foundation that autonomous agents can rely on to write software and conduct scientific research.
Automated Translation of Algebraic Geometry
Originally initiated in 2005 by Columbia University mathematician Johan de Jong, the open-source Stacks Project compiles extensive mathematical knowledge spanning collegiate algebra, number theory, and advanced geometry. Columbia mathematician Peter Woit compared the comprehensive reference to the famous Bourbaki books that rebuilt mathematics from its foundations during the twentieth century. Axiom Math deployed a fleet of autonomous software agents that converted the sprawling library's roughly 7,654 pages into approximately 16 million lines of computer-checked code written in the Lean programming language. Under the formal verification approach, an automated proof assistant verifies mathematical proofs line by line, ensuring that passing proofs are logically sound. Axiom's formalization is built on Lean and Mathlib, containing no sorry placeholders or native_decide, and relies on standard axioms propext, Classical.choice, and Quot.sound, according to MLQ News. Axiom Math's public repository divides the Stacks Project formalization into StacksCore, which is human-reviewed, and StacksFrontier, which was formalized autonomously and awaits human review, according to MLQ News. Stacks Project founder Johan de Jong stated on October 21, 2026, that contributors should not submit AI-generated pull requests upstream, leaving Axiom's Lean formalization maintained in an independent repository.
For an interconnected library like Stacks, checking each theorem represents only part of the challenge because definitions trace back to earlier results like a family tree. That dense interconnectedness initially made the team uncertain whether vibe coding would successfully preserve the beauty and structural consistency of the underlying mathematics.
Parallel Agent Architecture and Mathematical Training
To accomplish the formal verification, the engineering team gave its agents a loose operational structure rather than dictating every individual task, allowing them to identify parallel assignments. Axiom also trained proprietary models to excel at mathematics, initially relying on an in-house Lean expert to impart taste before the agents gradually developed taste on their own.
Formal Verification Infrastructure and Enterprise Applications
The completed verification fills what researchers described as a historical black hole in formalized algebraic geometry, giving mathematicians verified building blocks for future discoveries. Mathematician and Fields Medal winner Terence Tao has observed that accumulating larger libraries of formalized proofs systematically accelerates the generation of additional verified proofs.
Founded in March 2025 by 25-year-old Chief Executive Officer Carina Hong after leaving a doctoral program at Stanford University, Axiom raised $200 million in a Series A funding round led by Menlo Ventures. Beyond pure academic mathematics, Axiom plans to apply formal verification techniques to commercial software engineering, providing mathematical guarantees that prevent bugs and security vulnerabilities as generative models produce increasing volumes of code.