Axiom Formalizes Entire Stacks Project into 16M Lines of Verified Lean Code

Axiom Math announced on November 5 that it has formalized the entire Stacks Project: roughly 16 million lines of verifiable Lean-based code spanning hundreds of chapters and tens of thousands of mathematical results — widely seen as a powerful rebuttal to the popular claim that "AI-generated code at scale is inevitably slop."

Confirmed

• Scale and content: The entire Stacks Project has been formalized into Lean definitions and proofs — about 16 million lines of code covering tens of thousands of results across hundreds of chapters (@Scobleizer, @ChrSzegedy).
• Engineering foundation: Built on top of Mathlib, with every completed proof automatically verified by the Lean kernel; every definition, lemma, proposition, and theorem bearing a four-character tag in the project now has a corresponding Lean formalization (@LinusEkenstam, @rohanpaulai).
• Quality and structure: According to the announcement, the formalization preserves the highly interconnected dependency structure of the original text, ships with a visualized dependency graph, and has been optimized for code quality (@Scobleizer, @LinusEkenstam).
• Background: The Stacks Project, originally started by Johan de Jong, is the largest open-source textbook and reference work in algebraic geometry, described by many as key infrastructure for modern mathematics, especially algebraic geometry (@LucaAmb, Ken Ono as quoted by @m5, @ChrSzegedy).
• Math community attention: Mathematician Ken Ono publicly announced the project, positioning it as Axiom Math's next step after formalizing the CFSG (Classification of Finite Simple Groups), with the goal of preserving and verifying humanity's existing body of mathematics (@LucaAmb).

Why it matters

• The Stacks Project sits in one of the deepest areas of mathematics, and its complete formalization means a vast body of modern algebraic geometry has received machine-level verification for the first time, with value for both mathematical preservation and verification.
• The work was carried out by AI at scale, under a highly interconnected structure, and passed Lean kernel checks — directly countering the claim that "AI-written code at scale must be garbage," making it a key counterexample in debates over AI coding capability.
• The visualized dependency graph reveals the interconnected structure of such an enormous proof network, offering a useful reference for future formalization projects and the Lean community.

2026-11-05 ~ 2026-11-05 · 6 related posts

• [source] Axiom ships 16M-line AI formalization of the Stacks Project, countering 'AI code is slop' — Scobleizer · 2026-11-05
• [source] The Stacks Project, algebraic geometry's giant reference, is now formalized in Lean — LinusEkenstam · 2026-11-05
• Axiom Math launches STACKS to preserve and verify humanity's math with Lean — LucaAmb · 2026-11-05

3 near-duplicate retellings: rohanpaul_ai · kimmonismus · ChrSzegedy