Stacks: 7,500 Pages of Algebraic Geometry, Now in 16M Lines of Lean

Background and Phenomenon: “Largest Ever” Claim with 94 Stars

On November 4, 2026, Axiom (axiommath.ai) published a signed blog post announcing the completion of the Lean formalization of the entire Stacks Project: approximately 16 million lines of code (according to the official statement, due to the large repository, no independent line count was verified), claiming it as “the largest integrated, reusable formal mathematical library ever.” The corresponding repository AxiomMath/Stacks uses Apache-2.0 license, and the toolchain is locked at lean4 v4.34.0-rc2. According to data captured on November 6, 2026, the repository received 94 stars, with only 66▲ HN entries and 17 comments. The claimed scale and the enthusiasm of responses formed the first observation point of this breakdown. Why is the release of a mathematical library worth technical breakdown? Because it may be the largest “AI writes code, humans set standards, machines verify” engineering example currently available.

Stacks Project itself is the foundation of algebraic geometry: an open-source reference book initiated in 2005 by Columbia University mathematician Johan de Jong, with about 7,500 pages. Over twenty years, hundreds of mathematicians have contributed to it, following the principle that each theorem comes with a proof, assumptions are explicitly stated, and dependencies can be traced back to four-character tags. De Jong compares himself to “organizing mathematical foundations like maintaining the Linux kernel.” Modern algebraic geometry’s contemporary proofs may involve long theorems chains across commutative algebra, scheme, layer, homology, and algebraic stack theory. Lean previously lacked this infrastructure. Axiom’s motivation is straightforward: the speed at which AI generates mathematical arguments far exceeds human review capabilities, making formal verification essential.

Architecture and Technical Principles: Tag Mapping, Two-Level Review, Multi-Agent Audit

The first layer of mechanism is permanent comparison. Each Lean statement carries the @[stacks TAG] attribute, linking back to the four-character tag from the Stacks Project original text. A single tag can correspond to multiple statements, with attribute notes indicating which parts are covered when some are shared. Tags already covered by Mathlib are registered to Mathlib statements through add_to_stacks. Statements also mark their proofs as corresponding to entries in Grothendieck’s “EGA” and “SGA” (e.g., the @[ega] attribute carries entry number IV 7.8.3), with attribute notes distinguishing between four levels: “entire statement,” “more general,” “partial clause,” and “special case.” The accompanying website stacks.axiommath.ai provides side-by-side browsing of the original text and Lean code, along with interactive dependency graphs.

The second layer is a two-level review system. The repository is divided into two directories: StacksCore and StacksFrontier. Core contains code that has been manually reviewed, compared to the original text, and met Mathlib’s naming/ generality/styling standards. Frontier code is written by AI agents and covers the fastest-growing parts, which need the most review before entering Core. The README explains clearly: the only difference between the two layers is “who has reviewed the code,” both having been checked by the Lean kernel.

The third layer is the agent engineering. Axiom has deployed a “coordinated AI agent cluster” that parallelly translates statements, retrieves existing abstractions from Mathlib, constructs proofs, and resolves prior dependencies. It employs a hierarchical agent system and strict coordination protocols (the blog does not provide details of these protocols). Fidelity of statements is ensured by three mechanisms: multi-agent auditing, cross-checks on the semantics of the original text, and the hard constraint that “each definition lemma must successfully connect to downstream theorems.”

The fourth layer is an example-driven correction loop. During the formalization process, dozens of statements in the original Stacks text required local corrections: missing assumptions, edge cases in the positive feature domain, and statements that were too broad to hold. The agents are responsible for diagnosing mathematical obstacles and constructing explicit counterexamples; when a false lemma creates a proof gap in a deeper theorem, alternative paths are found in the literature, and the main theorem is rebuilt under the original assumptions.

Key Data: 63k modules, zero sorry, three axioms

The following numbers are reported by the official team or described in the repository; no third-party verification has been conducted yet.

The total size is reported as approximately 16 million lines; the README describes about 63,000 modules, stating that “every tag in the Stacks Project that has formable content has been formalized” (according to the README). Unformalized examples, exercises, and remarks are left as tasks for the community.

There are three hard indicators of quality: Lean kernel checks each proof; the entire library has no sorry or native_decide; only three standard axioms are used: propext, Classical.choice, and Quot.sound. Anyone can verify with the #print axioms command.

The construction cost is a practical barrier: the official command is lake exe cache get && lake build, which is time-consuming and memory-intensive for full compilation. The official plan to provide a compilation cache service has not been launched yet. This means that this 63k-module library is not currently friendly for ordinary personal machines.

Community Data: Retrieved on November 6, the repository has a rating of 94★; HN entries (story 50380979, published on November 5, 2026) have a rating of 66▲ with 17 comments. The comment section is not large, but the quality is high: there are both positive assessments of the formalization process and direct inquiries about verification philosophy. For reference, on October 27, 2026, the same organization published a formalization of limited single-group classification (CFSG), and Axiom has distinguished between the two: CFSG revolves around individual landmark theorems with a loose organization; Stacks is a foundational library whose value lies in thousands of interlocking definitions, constructions, and lemmas being repeatedly reused, and the engineering challenges are fundamentally different.

Impact and Significance: Turning “statement fidelity” into an auditable attribute

The first is usability. This is not a monument, but the foundation: mathematicians and AI agents can import Stacks and directly call basic algebraic geometry, using #stacks tags and #stacks! commands to list all items with tag declarations. What it fills in is the gap in modern algebraic geometry within the Lean ecosystem, allowing formalization in this field to stand on top of it without having to translate everything from scratch. This is especially true for agents: the task board breaks down “which examples have not been formallyized” into actionable tasks, and the README clearly welcomes community review of Frontier code being moved to Core, essentially paving a track for AI-assisted mathematics contributions.

The second is the signal of formalization feeding back into mathematics. Dozens of original statements were identified as needing correction, and agents constructed explicit counterexamples, showing that large-scale formalization is not just translation but also automatic review of the original text. HN noted that Stacks Project itself is akin to “Lean written in natural language”: each theorem comes with proof, assumptions are explicitly stated, and dependencies can be traced back, so high-quality formalization is not surprising; another commenter said that CFSG’s release anticipated someone would work on Stacks.

The third is the methodological insights for AI engineering beyond mathematics (this is my judgment). When AI generates code in bulk, the most vulnerable point is often not whether the proof can pass, but whether the statement is faithful to the original intent: kernel checks can ensure the former, but not whether “the theorem is translated correctly.” The three-piece set provided by Axiom—multi-agent auditing, semantic cross-checking, and downstream hard constraints—essentially turns “statement fidelity优先over proof correctness” into an engineering axiom. This approach can be directly applied to any large-scale auditing scenario where AI translation requires code generation.

Controversy and Risks: Rejection from upstream, criticism of the text, and the gap between cold start

The most sharp boundary lies in upstream attitudes. On October 21, 2026, de Jong requested in an upstream announcement that AI-generated comments and PRs not be directly submitted to the Stacks Project repository (as quoted by Axiom blog). Axiom stated that they respected this boundary: formalization, counterexamples, and corrections would all remain in their own repository, while upstream was still managed by de Jong and the community, available for mathematicians to review and use at their own pace. HN noted the sharpness of this: the latest post on the original Stacks Project blog on October 21 was titled “No AI for now,” and the commenter’s algebraic geometry friend was frustrated by AI advances in mathematics. In other words, these 16 million lines of code currently only have the status of an independent project and have not yet received upstream endorsement.

The second controversy concerns the copywriting. Many HN commentators criticized the blog post as a typical example of AI slop: Metaphors like “This milestone begins with” are mixed, which actually undermines confidence in the results. The counterarguments were equally direct: Some users pointed out that Axiom had received substantial funding (the commenter claimed this without independent verification), and the released content was a large Lean proof built by AI, with AI explicitly stated in the domain name. There’s no need to criticize the AI tone in the copywriting. My view: The criticism of the copywriting doesn’t address the technical essence, but it touches on an important issue: The blog lacks open-source documentation for the coordination protocol of the “agent cluster.” The more opaque the engineering black box, the easier it is for the copywriting tone to be magnified and scrutinized (this is my judgment).

The third issue is the gap between cold start and warm start. The claim of “the largest formal mathematical library in history” doesn’t match the 94★ ratings and 17 HN comments, showing a clear mismatch in popularity. Objective reasons include: high barriers to full build, cache services not yet available, and a narrow audience for algebraic geometry. The topic has even gone beyond the geometric circle: Some commenters corrected the misdirection, indicating that this Stack is a “stack” in algebraic geometry, not a technology stack. This misinterpretation itself proves that the attention attracted by the release has crossed professional boundaries. However, HN also raises questions about the philosophy of auditing: How can the fidelity of assumptions be verified? The multi-agent auditing section in the blog is actually the answer, but the commenting user claimed they didn’t read it. Another comment is more fundamental: Even if the proof is completely correct, the bottleneck in AI-era mathematics remains human understanding. Those who don’t solve problems or read proofs won’t gain understanding just because the library grows larger.

Conclusion and Outlook: Only libraries that can be imported are real monuments

The core message is: Axiom has translated a 7,500-page algebraic geometry masterpiece into about 16 million lines of Lean code (official claim), using three standard axioms, zero sorry, full kernel inspection, and a dual review system for Core/Frontier. However, the identity boundary of “rejecting AI contributions upstream” remains unresolved.

The entry point to participate is ready-made: Import Stacks and use them directly. #stacks_tags can search with tag declarations; claim tasks on stacks.axiommath.ai/contributing, and use the claim tag in GitHub issues to prevent duplication. Reviewing Frontier code and pushing it into Core is the most needed way of contributing now. Three things worth watching next: Whether the compilation cache service will be available (determining if 63k modules can be used by ordinary developers), whether Axiom will disclose details of the agent coordination protocol (determining whether multi-agent auditing can be replicated), and whether de Jong’s upstream policies will loosen (determining whether this library can become part of active text from independent projects).

For ordinary developers, even if you don’t work on algebraic geometry, this repository provides a reference model: How to design hierarchical reviews for large-scale code libraries generated by AI, and how to make “fidelity to original requirements” into verifiable constraints. My conclusion in one sentence: What’s most interesting about Stacks isn’t the 16 million lines of code, but its breakdown of “Is mathematics written by AI credible?” into two separate issues that can be verified: correctness is left to the kernel, and fidelity to original requirements is left to comparative auditing. The former provides a hard guarantee, while the latter provides engineering arrangements but lacks protocol-level disclosure. This is precisely its current biggest unresolved tension.

Reference Sources

• Axiom official blog (axiommath.ai, published on 2026-11-04, signed by Axiom; 16 million lines, agent cluster, and counterexample corrections all according to official statements; full text stored locally in stacks.txt)
• Repository: github.com/AxiomMath/Stacks (94★ / Apache-2.0 / lean4 v4.34.0-rc2 / main branch, snapshot captured on 2026-11-06; 59 lines of README read in full; repository too large to clone, line count not measured)
• HN entry: story 50380979 (66▲ / 17 comments, published on 2026-11-05, snapshot on 2026-11-06; comment pool hn-stacks-full.json contains 11 entries, all text quoted without direct citation)
• Stacks Project upstream background and de Jong’s announcement on 2026-10-21: All according to Axiom official blog quotes

Signed by: Yongliang