AxiomMath announces verification of the Stacks Project — TechCrunch

AxiomMath has announced the formal verification of the Stacks Project, a large open library of mathematical results. As TechCrunch reports, its AI agents translated approximately 7,654 pages of the project into about 16 million lines of Lean code verified by a computer proof assistant.

Checking mathematical proofs

Formalizing mathematics involves rewriting proofs in the Lean programming language. A special program, a proof assistant, checks the code line by line. If the check is successful, mathematicians can consider the proof logically correct.

The Stacks Project was launched in 2005 by Johan de Jong, a mathematician at Columbia University, as an open reference resource. Since then, mathematicians have expanded it with materials ranging from undergraduate algebra to complex topics in algebra, geometry, and number theory. Mathematician Peter Woit compared the project's significance to the Bourbaki book series, which built mathematics from its foundations in the 20th century.

The complexity of the work was not limited to checking individual theorems. Definitions and results in the Stacks Project are interconnected, so the team needed to preserve all connections while working with approximately 16 million lines of Lean code.

More current news is available on the UA.News Telegram channel Telegram.

A foundation for new proofs

Ashwin Swaminathan, a representative of AxiomMath's technical team, said the result fills a major gap in formalized mathematics, particularly in algebraic geometry. According to him, researchers who want to verify new work in this field using Lean now have a foundation for doing so.

The company believes that verified mathematical results can serve as reusable building blocks for new proofs and as a basis for infrastructure with which AI agents will work. Founder and CEO Karina Hong said that agents need a reliable knowledge library in order to develop it without errors embedded by unsuccessful engineering decisions at the initial stages.

Hong founded the company in March 2025 after leaving a mathematics PhD program at Stanford. In March, AxiomMath raised $200 million in a Series A round led by Menlo Ventures.