Axiom releases Stacks Lean library with Frontier review ahead

Axiom released its Stacks Lean library on November 4, 2026, turning a major algebraic geometry reference into formal code that other proofs can reuse. The important distinction is its review status: the library separates human-reviewed material from an AI-written frontier that still needs that scrutiny. A successful proof check and a faithful translation of the original mathematics are related, but different, tests.

In its announcement, Axiom reports roughly 16 million lines of code produced by coordinated agents working across shared definitions and dependencies. That figure is the company’s count, not an independent ByteForward measurement. The release is an independent Axiom project built on the original Stacks scholarship and the Lean and Mathlib ecosystem.

What the Axiom Stacks Lean library covers

The repository describes coverage of every Stacks tag with formalizable content. That does not mean every item in the reference is finished. Examples, exercises and remarks that have not yet been formalized remain contribution tasks.

The useful output is a connected library rather than a pile of isolated answers. A researcher working in formal algebraic geometry could reuse definitions and intermediate results instead of reconstructing the same foundations for each theorem. Whether a particular result is suitable still depends on its exact statement and dependencies.

Axiom’s explorer puts source statements alongside Lean declarations and a dependency graph. One tag may correspond to several declarations, each covering all or part of it. A tag appearing in the interface is therefore a starting point for inspection, not a substitute for reading the translation.

Core and Frontier have different review histories

The project explorer describes StacksCore as human-reviewed for agreement with the original mathematics and for Mathlib conventions. StacksFrontier contains AI-written material awaiting that review. Both tiers are described as checked by Lean’s kernel. Frontier should not be confused with a folder of unfinished proofs, but kernel acceptance does not give it Core’s human review history.

There is a practical import detail here: importing Stacks brings in both tiers. Anyone who needs a narrower assurance boundary should inspect which modules a proof actually depends on rather than treating the umbrella import as a human-reviewed-only collection.

The contribution guide makes the next work concrete. Contributors claim tasks, prepare a blueprint linking original and formal statements, identify dependencies and seek maintainer review. Reviewing and polishing Frontier results for Core is part of the project, alongside new proofs and remaining examples. Moving material upstream to Mathlib is a goal, not evidence that Mathlib has already accepted the library.

Proof validity is not translation fidelity

Lean’s proof validation documentation explains the distinction that matters here. Checking a proof establishes the formal proposition under its definitions and axioms. It does not independently establish that the proposition says everything a reader intended the original prose theorem to say.

For an initial evaluation, choose a familiar tag and compare its hypotheses, objects and conclusion with the source. Follow the declarations it depends on. Check that assumptions and covered cases match the original. These are checks on mathematical meaning, even when the formal proof itself passes.

Lean also provides tools for inspecting a theorem’s axioms and validating stored proof artifacts. Those tools answer questions about the formal dependency chain. They complement, rather than replace, expert judgment about the translation. ByteForward’s earlier coverage of funding for AI mathematics and human review explains why that review work needs resources of its own.

Plan for a large build and separate licenses

The documented setup uses Lean 4.34.0-rc2 and Mathlib. The repository warns that a full build spans roughly 63,000 modules and can take substantial time and memory. Its cache command retrieves compiled Mathlib artifacts. A dedicated Stacks cache is described as planned. Do not budget a full evaluation as a quick package install.

The code is offered under Apache 2.0. The original Stacks text has its own GNU Free Documentation License. Those are separate reuse conditions. For reproducible experiments, record the repository revision, toolchain and imported modules alongside any result.

A separate project from the original Stacks

The original Stacks Project remains separate. In an October 21 post, Johan de Jong asked people not to submit AI-written comments or pull requests to it. That policy predates Axiom’s release and should not be presented as a reaction to this announcement.

For formalization researchers, the opportunity is access to reusable infrastructure with an explicit review queue. The release does not eliminate the need to check meaning, and its size is not a measure of how much human review is complete. ByteForward reviewed the public documentation and project materials, but did not build the full corpus or independently verify its mathematical translations.

Illustrative image generated for ByteForward using Axiom’s official logo for editorial identification. No affiliation or endorsement is implied.