Axiom Math says its AI agents turned 7,654 pages of mathematics into checked code

A vast mathematical reference now has a computer-checked counterpart, according to Axiom Math. The company announced Wednesday that its AI agents formally verified the Stacks Project, translating roughly 7,654 pages into about 16 million lines of Lean code. Its aim is to give researchers and future AI agents checked foundations they can reuse.

Turning arguments into checkable steps

The Stacks Project began in 2005, when Columbia mathematician Johan de Jong started it as an open-source reference. Contributors have built it into a body of mathematics spanning college-level algebra through advanced work in algebra, geometry and number theory. Axiom’s announcement concerns formalizing that existing work: converting its mathematical arguments into a form that software can check.

Lean is the programming language used to express those proofs. A proof assistant then checks the code line by line to establish whether the encoded reasoning is logically sound. The checking stage is central to the undertaking: the output is not simply a large collection of AI-written mathematical explanations, but proofs expressed in code for mechanical verification.

Checking individual theorems was only part of the task. Stacks’ results depend on earlier results and shared definitions, so the team also had to preserve those connections across the formalization. CEO Carina Hong told TechCrunch that the combination of size and delicacy initially made the team unsure whether the effort would work. The concern was consistency across the whole library, not just success on isolated proofs.

You want [theorems] to be consistent and not, like, paradoxical. You want the definitions to not fight with each other.

Carina Hong, Axiom Math CEO, speaking to TechCrunch

Agents chose work within a loose hierarchy

Axiom did not assign every agent a fully prescribed sequence of jobs. Technical staff member Ashvin Swaminathan said the team imposed a hierarchy, while leaving agents room to identify tasks themselves and find work they could perform in parallel. That approach combined an organizing structure with some freedom for individual agents to decide where they could contribute.

The company also trained its own models for mathematics, Hong said. Early in the project, an in-house Lean expert helped teach the agents what she described as a human sense of mathematical taste. Hong said the agents later developed that judgment themselves. That is Axiom’s account of how the system’s choices improved, rather than a separately measured result presented alongside the announcement.

A library for the next proof

Swaminathan described algebraic geometry as a major gap in existing formalized mathematics. Researchers seeking to check new work in that field with Lean previously had little to build on, he said. Axiom argues that each verified result can become a building block for later proofs. The intended payoff is cumulative: researchers would use already checked mathematics rather than reconstruct the same foundations for each new project.

The company wants AI agents to use the library too. Swaminathan told TechCrunch that agents could read the code and build infrastructure on top of it. Hong sees a reusable body of knowledge as important to agents’ future work, arguing that poor engineering choices made at the beginning can make further progress harder. In that vision, the formalization serves both human researchers and systems carrying out mathematical work.

Axiom’s ambition extends beyond mathematics to software and eventually science. Swaminathan described mathematical verification as a transferable skill. Those applications remain the company’s bet; the concrete accomplishment it is claiming here is the formalization of Stacks.