Start-ups race to make AI prove math correctly

In Silicon Valley, mathematicians are leaving academia to build AI systems that don’t just solve problems but provide verifiable proof. Companies including Axiom Math and Harmonic are betting that mathematical correctness—and the ability to check it—can drive

When Ken Ono walked out of a University of Virginia professorship in 2025 and joined Axiom Math, he wasn’t chasing novelty. He was grieving—then recalculating what science could look like.

“Last May. I was honestly kind of grieving for my scientific identity. ” Ono says. describing the pull he felt as AI began outperforming many expectations in mathematics. He had been asked by another company. Epoch AI. to help craft a set of hard-to-solve maths problems designed to test AI’s problem-solving ability. But once he put those systems through their paces, he realized they were far more capable than he’d imagined.

“After a few months of that, I recognised, maybe this is that moment where the sharecropper confronts the combustion engine in the field and thinks maybe we can do more by embracing these technologies,” Ono says.

Axiom Math is one of a string of start-ups launched in the last two years with a focused promise: build AIs that don’t just do mathematics. but prove they’re doing it correctly. Harmonic. based in Palo Alto as well. is pursuing a similar ambition with a goal it describes as “mathematical superintelligence” that produces verifiable results.

Both firms sit in nondescript buildings near Stanford University. Between them, they have attracted enormous funding—investors pouring in hundreds of millions of dollars to pursue that same core bet: that mathematics can serve as the most demanding guide for an AI-powered future.

Inside Axiom Math’s offices—rooms named after famous mathematicians including Carl Friedrich Gauss and Ada Lovelace—Ono is blunt about why the world’s wealthiest AI labs have still left a gap that specialist start-ups think they can fill.

“ChatGPT is the librarian; you can’t find something it hasn’t read, but do you want your librarian to be your neurosurgeon?” Ono says.

The issue, as he tells it, isn’t that large language models can’t sound convincing. It’s that correctness still requires checking. For now, he argues, human verification remains necessary, and that creates an opening.

Verification, however, isn’t new to math. In recent decades, mathematicians have built systems to confirm whether a proof is correct. One of the most popular is Lean. a programming language that lets mathematicians translate handwritten proofs into a format that a computer can instantly check—an approach that can save significant time in research settings where even verifying a proof can consume a large share of already-stretched researchers’ energy.

A similar bottleneck exists in computer programming. Large language models produce vast amounts of code that often contain small, hard-to-spot errors. The result, in practice, is that many human programmers have become what Ono and others describe as babysitters for AI output.

Companies like Axiom Math and Harmonic see revenue in the same remedy: mathematical verification that a result is correct.

“As AI starts writing more and more code, the complementary value of verification increases, because humans then become the bottleneck,” says Harmonic CEO Tudor Achim.

The projection is straightforward. If a mathematical proof can be verified as correct with Lean or a similar system, then software can be verified as correct using mathematical proof techniques—mathematically proving a program contains no bugs.

Revenue is the headline, but it isn’t the whole story. Both companies also have AI tools that are adept at solving mathematics problems in active research areas. They say those tools have generated checked proofs in fields including algebraic geometry and number theory.

Axiom Math adds a concrete milestone: five papers written entirely with Axiom Math’s AI tools have now been accepted in mathematical journals.

Ono wouldn’t lay out Axiom Math’s exact roadmap for future challenges, but he said the company aims to have dozens of written papers by next year—compressing years of work into weeks and days.

The start-ups aren’t competing only with each other. Tech giants are pouring resources into math-solving AIs too.

“Mathematics is wonderful for developing AI because it’s very measurable,” OpenAI chief scientist Jakub Pachocki says. He adds that early language models struggled with “very quantifiable things,” but that they have improved. “Also, for the initial language models, it was a great example of something that was hard for them. They really weren’t good at very quantifiable things. But now they’ve become quite good.”.

OpenAI describes a shift in performance. After a slow start—when large language models struggled to make simple mathematical arguments—more recent AI systems have produced results that surprised even their creators. OpenAI points to a sequence of achievements: winning gold at the International Mathematical Olympiad. an elite high-school competition previously thought out of reach for AIs; and more recently. disproving an 80-year-old conjecture that some mathematicians thought they wouldn’t see progress on in their lifetimes.

Sébastien Bubeck, of OpenAI, frames the change as a move away from obvious failure modes. “The weaknesses that we saw six months ago were extremely apparent,” he says. “There were fields of mathematics where the model was only saying nonsense. Today, I think it’s not quite like that.”

Bubeck also distinguishes OpenAI’s approach from companies like Axiom Math and Harmonic. He says OpenAI isn’t optimizing specifically for mathematics. Instead, it aims at general AI training—and capabilities emerge as the system becomes more generally capable.

“We are doing general AI training, and through this general improvement come out capabilities that are shocking all of us in terms of mathematics,” Bubeck says.

The uncertainty is what makes the current moment feel both exhilarating and fragile. If the math-driven push comes and goes, what happens to the institutions and careers built around it?

At Stanford University, Ravi Vakil puts the concern in plain terms. “Right now. there’s a lot of money being put into this. and we’re going to miss it when it’s gone. ” he says. He adds that the interest improves AI models more broadly—making them better at thinking like mathematicians—but warns that the money won’t be comparable later. “In five years, it won’t be like this. There’s not a lot of money to be made out of solving the Riemann hypothesis.”.

The risk goes beyond funding. Another possibility, Vakil’s worry implies and start-ups acknowledge, is that mathematics becomes access-controlled—an AI-and-cash “walled garden.”

Shubho Sengupta at Axiom Math says the future may not be free. “Some math today is already paywalled,” he says. “[Large hedge funds] do a lot of mathematical modelling. None of that is accessible to anybody else. for good reason. because that is their intellectual property; that is how they make money.”.

Sengupta draws a line at that idea. “The pushing of the bounds of knowledge of math forward should be free.”

Achim at Harmonic shares a different model: a service you pay for, and a system you build to avoid treating mathematicians as disposable. “A tool that’s useful for math costs money. We want to give people an opportunity to pay in exchange for getting a service they want.”

He says the company also intends to support mathematicians and rejects the notion that they are simply a means to corporate ends. “If the company believes that math is really important for the future. we’re of course always going to want to support mathematicians the best way we can. I don’t think any company sees mathematicians as a way to extract all the value for the company.”.

For now, predicting which vision wins out is difficult. AI progress is fast enough to make “foreseeable” feel like a gamble. Still, most of the people in this space—including Ono—suggest the near-term reality is that mathematicians will remain central.

As he left Axiom. Ono compared the rise of math-capable AI systems to the moment when Srinivasa Ramanujan burst onto the mathematical scene. Ramanujan. a self-taught mathematician from India. produced discoveries largely driven by intuition—shocking the mathematical community in the early 20th century because they seemed to arrive “out of nowhere.”.

Ono’s personal history is tangled up in that story. He says his father, a Japanese mathematician who moved to the US partly because he was inspired by Ramanujan’s story, died in January. Ono recalls one of their last conversations.

“Maybe it is like your Ramanujan moment, maybe other people won’t understand, and if you see a computer coming up with something that looks like magic, you should embrace it, because it already happened to all of us,” Ono says.

In the buildings near Stanford, with rooms named after Gauss and Lovelace and investors underwriting the next leap, the question isn’t whether AI can do mathematics. It’s whether the proof will come with it—checked, verifiable, and trusted by the people whose work is built on certainty.

Axiom Math Harmonic OpenAI mathematics artificial intelligence Lean verification mathematical proofs International Mathematical Olympiad algebraic geometry number theory Riemann hypothesis Lean programming language