AxiomMath announces the formalization of the Stacks Project in Lean

AxiomMath says it has formally verified the Stacks Project, a reference library in mathematics. In an article published on November 5, TechCrunch reports that the company’s AI agents translated its roughly 7,654 pages into around 16 million lines of computer-verified code. The announcement was made on Wednesday, according to the outlet.

The work relies on Lean, a language in which proofs are reformulated as code and then checked by a proof assistant. For a library of this scale, the challenge extends beyond verifying each theorem individually: definitions and results depend on one another. AxiomMath explains that it had to preserve these relationships throughout the translation.

The company presents this formalization as a reusable foundation, particularly in algebraic geometry. According to its team, researchers seeking to verify new work in this field previously had few foundations available in Lean. Its agents worked in parallel within a hierarchical structure that gave them latitude to identify their tasks.

The potential value lies in accumulating checked results on which other proofs could build. AxiomMath also wants to transfer this approach to software. That prospect remains an ambition: the reported announcement concerns mathematical formalization and does not, on its own, establish that agents can produce software free of defects.