Axiom releases a 16-million-line math library, with human review still pending

Axiom Math released a Lean library of the Stacks Project on November 4, describing it as roughly 16 million lines of code. Researchers can import its definitions and theorems into new proofs. The public repository separates human-reviewed material from AI-written formalizations awaiting that review.

The original Stacks Project is an open reference for graduate students and researchers in algebraic geometry. It develops the mathematics needed for algebraic stacks. Permanent tags identify results, while links let readers follow the definitions and lemmas on which a proof depends. Its scope includes commutative algebra, schemes, varieties and algebraic spaces. It is a specialist reference rather than an introductory course. Axiom's release is a separate formalization of that material.

Axiom says coordinated AI agents translated statements, searched existing mathematical libraries and assembled proofs in parallel. Its account emphasizes preserving compatible definitions and dependencies across chapters, alongside producing proofs of individual results.

Kernel checks and human review

In the repository, StacksCore contains formalizations that people have checked against the source and brought to Mathlib's standards. Mathlib is Lean's existing mathematical library. StacksFrontier contains AI-written code awaiting that review before migration into Core. The README says Lean's kernel checks proofs in both tiers, with no use of the unfinished-proof placeholder sorry.

The project's formalization metadata labels its review status self-assessed. It says each Frontier statement was checked against its Stacks tag, but has yet to receive human review. Logical acceptance of the code therefore comes with a separate question: whether its formal statements faithfully represent the source text.

The metadata fixes a particular Git revision of the source, identifying chapters 1–109 and excluding exercises and obsolete chapters. Foundational definitions and Core were formalized and reviewed manually; most Frontier material was formalized autonomously using Axiom's AxiomProver system. Development took place in an internal Axiom repository.

The public code also has a follow-up repair. Commit 012108f changes two files to make the build succeed, according to its description. It addresses a duplicate generated equation lemma rejected by the kernel. AI Ping has not independently built the complete library; the account of the repair's effect comes from that public commit.

Axiom's explorer connects Stacks tags to Lean source, the original statements and dependencies. When several declarations formalize different parts of one tag, the interface provides separate code tabs. Readers can investigate both a result and the formal material supporting it. The site identifies tags already in Mathlib in green and those judged inapplicable to Lean in red.

The graph groups declarations by part, chapter and section. It distinguishes Lean dependency references from citations in the natural-language text. Its contribution section lists new formalizations, review of Frontier code, migration into Core and improvements to existing proofs.

The original Stacks Project retains its own contribution policy. In an October 21 post, maintainer Johan de Jong asked people temporarily to withhold AI-written comments and pull requests. He continues to welcome observations and fixes that contributors write themselves, while maintaining the source by hand.

Reusing the release also carries a build requirement. The README warns that compiling its roughly 63,000 modules takes substantial time and memory. Compiled Mathlib files can be downloaded; a cache service for the Stacks modules themselves is listed as planned.