AI agents turn 7,500 pages of mathematics into proofs that a computer can check

A mathematical proof is only reliable once someone has checked every step. For long proofs that is a lot of work, and mathematicians make mistakes too. That is why more and more researchers write proofs as computer code. A program, called a proof assistant, then checks that code line by line. Lean is one such program; the company Physical Superintelligence also used it earlier to check five quantum proofs.

The US company Axiom Math announced on 4 November that its AI agents have done this for a complete reference work: the Stacks Project. It is an open collection of about 7,500 pages on algebraic geometry, the branch of mathematics that describes shapes using equations. Johan de Jong of Columbia University started it in 2005. His colleague Peter Woit writes that there is nothing else really comparable to it.

The result is about 16 million lines of Lean code. According to Axiom, this is the largest coherent body of mathematics in this form ever built.

How the agents went about it

Theorems in a reference work like this rely on one another. The agents therefore worked on different parts of that network at the same time. They translated theorems into code, searched Mathlib, the large shared Lean library built by mathematicians, for what already existed, and built the proofs. Axiom trained its own AI models for this.

Lean checks whether a proof is correct, but not whether the theorem in the code says the same as in the original text. Axiom itself calls that the most important part. It therefore had agents compare the code with the text, and carried out extra checks on the basic concepts and the main theorems.

This brought up dozens of statements in the reference work that needed refining, for example because a condition was missing or because a claim did not hold as generally as it said. The agents then built a counterexample. When a supporting lemma turned out to be wrong, they looked for another route to the same main result.

People are now reviewing further

The library has two parts. StacksCore has been compared with the reference work by people and meets the requirements of Mathlib. StacksFrontier was written by agents and has not yet had that check. Lean checks the proofs in both parts. The code is public, and four maintainers review every new contribution.

The claim that the whole work has now been converted comes from Axiom itself. On 21 October, Johan de Jong asked that AI contributions not be sent directly to the Stacks Project itself for the time being. Axiom therefore keeps the converted version in a project of its own.

Why this matters

Anyone who wanted to check new results in this field with Lean had little to build on until now, says Axiom. Researchers and AI agents can now use the theorems directly in new proofs.

This comes at a time when AI is producing more and more mathematics. Last month OpenAI released 719 manuscripts with solutions to hard mathematical problems, reports TechCrunch, which turned out not yet to meet the standards of the field. Checked proofs make such work easier to assess.

Axiom thinks beyond mathematics. The company expects that software, too, will soon have to rest on such checked foundations, now that AI is writing more and more code. Chief executive Carina Hong, who founded the company in 2025, challenged coding companies in an interview with TechCrunch to work on formal checking at this scale.

What does this mean for the road to the singularity?

The more AI writes itself, the less people can read through everything. A computer that checks the work step by step can then take over much of that reviewing. This project is a large test of that: AI agents build a foundation on which other agents and researchers can continue. Human review of the AI-written part is the next step. If the approach also works elsewhere, AI could soon deliver mathematics and software that come with their proofs built in.

What is the technological singularity? Read the explanation →