Stanford dropout's $1.6B AI startup claims to have built world's largest computer-verified math library

The company announced Wednesday that its AI agents had converted about 7,654 pages of the Stacks Project, a mathematical reference developed over two decades, into 16 million lines of code.

"Spanning some 16 million lines of code, it is the largest integrated, reusable library of formalized mathematics ever built," Axiom said, adding that the work could help researchers and AI systems develop new mathematical proofs using previously verified knowledge.

Hong, who left a mathematics PhD program at Stanford to establish Axiom in March 2025, aims to address a growing challenge: AI systems can generate mathematical proofs faster than researchers can manually check them.

Her company initially raised $64 million in funding in 2025 at a valuation of $300 million. It secured another $200 million in a funding round led by venture capital firm Menlo Ventures in March 2026, lifting its valuation to more than $1.6 billion.

Hong has also attracted prominent researchers from some of the world's largest technology companies, including Meta and Google, as well as leading mathematicians.

Carina Hong, founder of Axiom Math. Photo from Hong's LinkedIn

Before enrolling at Stanford, Hong earned bachelor's degrees in mathematics and physics from the Massachusetts Institute of Technology and a master's degree in computational neuroscience from the University of Oxford, where she studied as a Rhodes Scholar.

The Stacks Project, the focus of Axiom's latest achievement, was launched in 2005 by mathematician Johan de Jong as a free online reference for algebraic geometry, a field that studies shapes and mathematical equations.

Over the years, it has grown into a vast collection of mathematical explanations, established results and proofs that researchers can use in their work. Axiom's AI technology converts this material into a form that computers can examine step by step.

In mathematics, a proof is a series of logical steps demonstrating why a statement is true. Even a small mistake in one step can undermine the entire argument. Axiom uses a computer system called Lean to check whether each step follows logically from the previous ones, according to tech site TechCrunch.

It said its AI agents worked on thousands of mathematical problems simultaneously while ensuring that the different parts of the collection remained consistent with one another. It said the process also uncovered problems in some of the original mathematical statements, including missing conditions and claims that were not always true. Its AI systems identified examples that challenged those statements and proposed corrections or alternative proofs.

The resulting collection has been made publicly available, allowing mathematicians to examine and use the computer-checked material.

In January, Axiom reported that its AI system had solved all 12 problems from the prestigious Putnam mathematics competition for university students, although only eight were completed within the official time limit.

Beyond mathematics, it aims to apply its technology to software development, helping engineers detect errors and verify the reliability of AI-generated code.