Axiom Math Formally Verifies the Stacks Project with AI Agents
Axiom Math wants to keep AI slop out of mathematics
- Who
- Axiom Math
- What
- formally verified the Stacks Project
- Quote
On Wednesday, the company announced it had formally verified the Stacks Project, one of the largest bodies of mathematics ever written by humans.
What happened
Axiom Math says it has formally verified the Stacks Project, an open-source mathematics reference started by Johan de Jong in 2005. The company’s agents translated roughly 7,654 pages into about 16 million lines of Lean code, checked line by line by a proof assistant. Axiom says the verified results give researchers a foundation for future work in algebraic geometry and could also support software built by AI agents.
Why it matters
Axiom’s formalization of the Stacks Project shows how a large, interconnected mathematical library can become a checked foundation for future proofs and agent-built software.
Read next
See the full storyAxiom Math Says Its AI Agents Formally Verified the Stacks ProjectThe story so far
Axiom Math says its agents formally verified the Stacks Project, an open-source mathematics reference founded by Johan de Jong in 2005. The company says they translated about 7,654 pages into roughly 16 million lines of Lean code, which a proof assistant checked line by line. Axiom says the verified results could give researchers a foundation for future work in algebraic geometry and support software built by AI agents.
Keep up with AI, one email a day
Model releases, price changes and compute developments, with original sources. Free, confirmed by email, and easy to unsubscribe. Read a past issue · 2026-11-05