Making AI work on a math library without losing the meaning of the theorems

Axiom publishes a translation of the Stacks Project into Lean, to reuse computer-verified proofs. Human proofreading remains a work in progress.

Sixteen million lines of code to turn a reference work in algebraic geometry into a computer-usable library of proofs. The announced scale of Axiom’s project gives a sense of its scope: translating the definitions and results of the Stacks Project into Lean, a language designed to write and check mathematical reasoning. The publication combines the work of human specialists and that of AI agents.

The public repository organizes this translation into two sets. The first brings together code reviewed by people; the second contains code from agents that is still awaiting that review. The project maintainers say that the proofs pass Lean’s logical checks in both cases. This distinction is central: verifying a formal argument and verifying that it faithfully translates the mathematical text are two different tasks. Results that can be retrieved and reused

The original Stacks Project is a collective reference work in algebraic geometry. At the time of consultation, its site counted 7,654 pages and 21,446 items identified by a tag, distributed across 116 chapters. The content is intended for advanced students and researchers, with developments in commutative algebra and in the foundations needed to study the geometric spaces at issue.

A mathematical result often uses definitions and propositions established elsewhere. The difficulty of a translation on this scale is therefore to preserve the links between the elements, so that a proof can use those on which it depends. The published work is built on Mathlib, Lean’s mathematical library, from which it also reuses results already available.

Each item in the Stacks Project has a permanent four-character identifier. The translation preserves these markers to connect the source text to the corresponding declarations in the code. On the consultation site, the reader can find a result, examine its dependencies, and access its formalization. When the same result requires several Lean declarations, these remain associated with its identifier.

This organization gives researchers and proof systems a base from which to draw for new arguments. A proof can reuse a result already established in the library, along with the definitions and hypotheses that accompany it. The value of the project lies in this possibility of reuse, beyond the number of lines produced. A correct proof can translate the wrong statement

Lean’s operation differs from that of a chatbot that offers a mathematical explanation. Its kernel checks that a proof follows the logical rules and establishes the statement written in the formal language. The Lean documentation on proof validation explicitly distinguishes this validity from the meaning one intended to give the theorem.

If a translation adds a hypothesis absent from the original text, the resulting proof may be correct while establishing a narrower result. Likewise, a poorly chosen definition can shift the meaning of the problem. Automatic checking therefore does not remove the need to examine the statements and mathematical objects used.

That is the function of the separation between StacksCore and StacksFrontier. According to the project maintainers, the first set was reviewed by humans, compared with the Stacks Project, and rewritten according to Mathlib conventions. The second contains the formalizations produced by the agents, whose human review remains to be done. The project description file presents the review status as self-assessed.

The authors also say they do not use proofs left pending with the `sorry` command, nor additional axioms beyond the standard foundations adopted. These commitments describe the conditions of the announced checking. They do not, by themselves, constitute an independent review of correspondence with the source text as a whole. Announced coverage, with the scope specified

The launch wording evokes the formalization of the entirety of the Stacks Project. The repository documents add clarifications: the README claims coverage of the items with formalizable content, while leaving examples, exercises, and remarks as tasks for contributors. The descriptive file specifies a particular version of the source text, chapters 1 through 109, and the exclusion of exercises as well as obsolete chapters.

These indications define the scope of the coverage claim. The volume of code measures neither the proportion already reviewed by humans nor the quality of each translation. According to its maintainers, the repository contains about 63,000 modules; compiling it completely takes time and a lot of memory. A compiled-module cache service is announced as planned.

Expected contributions concern both review and additions. The contribution guide asks that the generality of the original statement be preserved and that a problem be reported rather than weakened in order to make the proof succeed. Moving from StacksFrontier to StacksCore is one of the tasks proposed to the community. The original project keeps its own rules

The Lean library published by Axiom and the work it is based on are two distinct projects. The former is distributed under the Apache 2.0 license; the latter falls under the GNU Free Documentation License. New contributions to the formalization repository go through its maintainers, with a prior proposal for formalization or review work.

The context of the original project is different. In his “No AI for now” post, dated October 21, Johan de Jong asked that no comments or proposed changes containing AI-written material be sent. This text predates Axiom’s announcement: it cannot be presented as a reaction to that publication.

The mathematician said he wanted to continue updating and correcting the Stacks Project by hand. He invited readers to send their observations and corrections written personally, via comments, email, or in the project repository.