# Axiom Math releases a Lean formalization of the Stacks Project

> Original title: Vibe coding at scale has a reputation for slop, so Axiom Math formalized the Stacks Project to show otherwise.

- Source: Rohan Paul
- Published: 2026-11-04T17:53:57.000Z
- Bad Influence: https://badinfluence.news/items/b6h9ecr85sa7ui9qiwz978ict
- Original: https://x.com/rohanpaul_ai/status/2118039060354900210

## Summary

Axiom Math says it has released a 16-million-line Lean formalization of the Stacks Project, a reference textbook on algebraic geometry. Lean checks each completed proof, and each tagged result links to its original text and dependencies. The library is described as free and open source, so mathematicians and AI models can reuse verified definitions and theorems.

## Why it matters

The source names the scale of the Lean formalization and its open-source access, showing how verified definitions can be reused in algebraic geometry.

## Post

Vibe coding at scale has a reputation for slop, so Axiom Math formalized the Stacks Project to show otherwise.

Mathematicians usually trust a proof because experts read it; Axiom Math turned an entire field’s reference book into Lean code, so a computer can now confirm the logic line by line.

Axiom ran its agent swarm like an engineering org, with humans assigning some agents the architecture, others core definitions and others individual proofs.

Lean checks every completed proof, and each tagged result links to its original text and dependencies, so the pieces fit together like panes of the Louvre’s pyramid.

And nothing entered the library unless the logic held.

All these means that now we have a free, open-source library where a big chunk of modern algebraic geometry exists as computer-checked code instead of only as text in a book.

In practice, anyone (a mathematician or an AI model) who wants to prove something new in this field can now reuse these already-verified definitions and theorems instead of rebuilding them, and a computer will flag any step that doesn’t follow.

![](https://badinfluence.news/api/img-proxy?u=https%3A%2F%2Fpbs.twimg.com%2Fmedia%2FHWTHl6eaYAAKh_f.jpg&mode=thumb&exp=1794009600&sig=3810bfb19a10d92f)

## 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