Axiom Math Wants to Keep AI Slop Out of Mathematics
It feels like AI is cracking a new math problem every week. Last month, OpenAI alone released 719 manuscripts claiming solutions to some of the field’s hardest problems. Even the computer checks can slip. After years of AI slop, it’s fair to wonder whether math is next.
Axiom Math is betting math can avoid that fate—not by slowing down, but by standing on firmer ground. The $1.6 billion startup wants to build a verified foundation that AI agents can rely on to write software and, eventually, do science.
On Wednesday, the company announced it had formally verified the Stacks Project, one of the largest bodies of mathematics ever written by humans. Mathematicians often hold Stacks in rare regard—Columbia mathematician Peter Woit has claimed there’s “nothing else really comparable,” comparing the project to “the famous Bourbaki books,” a series that rebuilt math from its foundations in the 20th century.
Woit’s Columbia colleague Johan de Jong started the Stacks Project in 2005 as an open-source reference. Mathematicians have contributed to it ever since, building out results from college-level algebra all the way up to the field’s most advanced ideas across algebra, geometry, and number theory.
The company’s fleet of AI agents translates the library’s roughly 7,654 pages into about 16 million lines of computer-checked code.
What Formal Verification Means for Mathematics
Formalizing math is a way of making sure the structure underneath it is sound. Mathematicians rewrite the proof as code in a programming language called Lean, and a program called a proof assistant checks the code line by line. If the proof passes, mathematicians can trust that it’s logically sound.
Engineers use the same idea, called formal verification, to confirm their chip designs work, while researchers in France have used it to catch bugs in software that calculates family benefits.
The Challenge of Interconnected Theorems
For a library like the Stacks Project, checking each theorem is only part of the job. The theorems and definitions in Stacks are interconnected, and each one builds on the ones before it. Like a family tree, many results in Stacks trace back to the ones that came before them.
That interconnectedness made Axiom unsure the project would work at first. The team had to keep every connection intact across about 16 million lines of Lean code.
“Things that are big and things that are delicate in life just don’t go together,” Axiom CEO Carina Hong told TechCrunch. “[Stacks] is a collection of mathematical results that is the foundation of mathematics. You want [theorems] to be consistent and not, like, paradoxical. You want the definitions to not fight with each other.”
The 25-year-old CEO [article continues]
via TechCrunch AI