Axiom releases full Lean formalization of the 7,500-page Stacks Project

Axiom, a startup valued at $1.6 billion according to TechCrunch, has formally verified the entire Stacks Project, converting the foundational algebraic geometry reference into about 16 million lines of machine-checked Lean code. Axiom describes the result as the largest integrated, reusable library of formalized mathematics ever built.

A reference text, translated

The Stacks Project is an open-source reference for algebraic geometry, started in 2005 by Columbia University mathematician Johan de Jong and expanded over two decades by hundreds of contributors. Axiom puts its length at roughly 7,500 pages; TechCrunch counts about 7,654. Columbia's Peter Woit, quoted by TechCrunch, said there is "nothing else really comparable" and likened the project to the Bourbaki books that rebuilt mathematics from its foundations in the 20th century.

The release preserves the project's permanent four-character tags, so every Lean declaration links back to the corresponding passage in the canonical text. Axiom has also published an online viewer that shows the original pages alongside the Lean code, plus an interactive dependency graph. Because a single tag can expand into several formal definitions — some newly written, some bridged to the existing Mathlib library — the interface records those mappings explicitly. According to Axiom, Lean's kernel guarantees that a cited result can only be applied when its exact hypotheses are satisfied.

What formalization buys

Formalizing a proof means rewriting it as code in Lean and letting a program called a proof assistant check it line by line. If the proof passes, mathematicians can trust it is logically sound. As TechCrunch notes, engineers use the same technique, formal verification, to confirm chip designs, and researchers in France have used it to catch bugs in software that calculates family benefits.

For the Stacks Project, checking individual theorems was only part of the job. Its results form a dense dependency tree in which everything builds on what came before, and the whole corpus has to stay coherent. "Things that are big and things that are delicate in life just don't go together," Axiom CEO Carina Hong told TechCrunch, adding that the definitions must not "fight with each other."

Agents working in parallel

Axiom says it ran large, coordinated teams of AI agents that translated, proved and integrated thousands of theorems in parallel. TechCrunch reports the team imposed a loose hierarchy rather than dictating every task, letting agents identify work they could do simultaneously. The company also trained its own models to be good at mathematics, an approach Hong said other verification startups have generally not taken.

Hong, whom TechCrunch describes as 25 years old, left a Stanford mathematics PhD program to found the company in March 2025. In March, Axiom raised a $200 million Series A led by Menlo Ventures.

This is Axiom's second major release this season. On October 27, 2026, the company released a Lean formalization of the Classification of Finite Simple Groups. But the two represent different engineering challenges, Axiom notes: that project centers on a single landmark theorem, while the Stacks Project is a foundational library whose value lies in thousands of interlocking, reusable definitions and lemmas.

Filling the algebraic geometry gap

The release addresses what Ashvin Swaminathan, a member of Axiom's technical staff, called a black hole in formalized mathematics. Modern algebraic geometry was difficult to approach in Lean because a contemporary proof may invoke long chains of results across commutative algebra, schemes, sheaves, cohomology and algebraic stacks before its core argument even begins. Researchers who wanted to check new work in the field previously had little Lean infrastructure to build on — and now, Swaminathan told TechCrunch, they do.

Why it matters

The backdrop is a rising volume of machine-generated mathematics that humans cannot easily inspect. TechCrunch notes that OpenAI alone released 719 manuscripts claiming solutions to hard problems last month, and that even computer checks can slip. Formal verification is one answer that scales with that flood: the proof assistant does not tire, and each verified theorem becomes a building block for the next. UCLA mathematician and Fields Medal winner Terence Tao, quoted by TechCrunch, summarized the compounding effect: "The more formalized proofs you have, the more formalized proofs you can make."

Axiom's larger bet reaches beyond pure mathematics. As AI agents write more of the world's code, the company argues they will need verified foundations to avoid what Hong calls slop, and its Lean library is positioned as the substrate agents build on. Hong went as far as to challenge "all the coding companies to work on formalization at this scale."