# Axiom releases a 16-million-line Lean formalization of the Stacks Project

> Original title: Huge release for AI and math!

- Source: Elvis Saravia
- Published: 2026-11-04T17:22:43.000Z
- Bad Influence: https://badinfluence.news/items/k3fuyx4qncrkc8y2jsvfei565
- Original: https://x.com/omarsar0/status/2118031199255879758

## Summary

Axiom has released a 16-million-line formalization of the Stacks Project in Lean, a foundational reference for modern algebraic geometry. The company says the code is optimized and keeps the project's highly interconnected structure intact. Elvis Saravia, who shared the announcement, says AI agents can now build new mathematics on this foundation.

## Post

Huge release for AI and math!

Many people assume AI-generated code at scale means low quality. 

Axiom's new Stacks Project formalization in Lean says otherwise.

The Stacks Project is a massive, deeply interconnected foundation for modern algebraic geometry.

They turned it into machine-checkable code and kept that structure intact. AI agents now have a reusable foundation to build new math on.

## Quoted post @axiommathai

> Most think vibecoding at scale is slop. Here’s a counterexample.
> 
> Today we release a 16M-line formalization of the entire Stacks Project, critical infra underlying modern math, with optimized code quality and its highly interconnected structure preserved.
> 
> A mathematical city 🌆

https://x.com/axiommathai/status/2118028834515874112