Axiom Math has released a machine-checked version of the Stacks Project, a major open-source reference for algebraic geometry. The formalization translates the project’s mathematics into about 16 million lines of Lean code, which a proof-checking program checks step by step. Axiom says researchers and AI agents can use the results as a connected library when building new formal proofs.
The sources give slightly different page counts: TechCrunch reports about 7,654 pages, while Axiom describes the project as roughly 7,500 pages. The original reference was started by Columbia mathematician Johan de Jong in 2005 and expanded over two decades by mathematicians. Axiom’s work formalizes that existing scholarship; it does not mean the AI agents independently discovered the underlying mathematics.
Why does a connected library matter?
A proof library is useful not just because its individual theorems have been checked, but because later proofs can reuse them and their dependencies. Axiom says it preserved the Stacks Project’s permanent tags, linking Lean declarations to the corresponding parts of the original text. Its website also lets readers view the text alongside the code and explore how results depend on one another.
That matters especially in algebraic geometry, where a proof can rely on a long chain of ideas from areas such as commutative algebra, schemes, sheaves and cohomology. Axiom says that, before this release, researchers had much less Lean infrastructure for formalizing modern algebraic geometry. The company’s library gives them a starting point rather than requiring them to formalize those foundations again for each project.
A foundation for future proofs—and software
Axiom says its agents worked in parallel to translate, prove and integrate thousands of theorems. TechCrunch reports that the company gave the agents a loose structure so they could identify tasks to work on, and that Axiom also trained its own math-focused models. The company says the finished library is the largest integrated, reusable library of formalized mathematics; that is Axiom’s characterization of its release.
The same kind of checking is used in areas such as chip design and software verification. Axiom argues that reusable, checked foundations could help AI agents build more reliable systems as they write more code. But the release verifies the formalized Stacks Project, not every new mathematical claim or piece of software an AI system might produce.
Why it matters
For mathematicians working in algebraic geometry, the library offers checked results they can reuse instead of rebuilding the same foundations in Lean. It confirms the formalization of this reference, but does not establish that future AI-generated proofs or code will be reliable without checking.
