Start-ups are racing to revolutionise mathematics with AI

Mathematicians have never been so sought after by the world’s richest people. At universities across the world, academics are seeing their colleagues mysteriously disappear and join private companies. Some of these companies are household names, like OpenAI and Google, but others are newly formed and just months old, hoping to capitalise on a moment in which mathematics is seen as the secret ingredient with which to improve artificial intelligence – which may in turn transform mathematics itself.

“Last May, I was honestly kind of grieving for my scientific identity,” says Ken Ono, who in 2025 went on leave from a professorship at the University of Virginia to join Axiom Math, a start-up aiming to build a maths-focused AI.

Ono had been asked by a different company, called Epoch AI, to help craft a set of hard-to-solve maths problems that would test AI’s problem-solving ability. But as he put these AIs through their paces, he realised they were far more capable than he 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,” says Ono.

Ono’s realisation wasn’t unique: Axiom Math is one of a string of companies started in the last two years that aim to build AIs that can not just do mathematics, but prove that they are doing it correctly. In April, I visited these companies in Silicon Valley, California, to understand why they had placed such enormous faith in mathematics as a guide to an AI-filled future.

Axiom Math’s offices are based in Palo Alto, a stone’s throw away from Stanford University, where its founder, Carina Hong, who is also Ono’s former student, previously studied. A few doors down is another start-up, called Harmonic, which similarly aims to build a “mathematical superintelligence” that produces verifiable results. Both companies occupy nondescript buildings, but they have amassed vast pools of money, with investors pouring in hundreds of millions of dollars to achieve their aims.

Inside an unassuming office, with rooms named after famous mathematicians like Carl Friedrich Gauss and Ada Lovelace, I asked Ono why there is a need for companies like his, especially with the existence of such well-funded and massive AI companies like OpenAI and Google.

“ChatGPT is the librarian; you can’t find something it hasn’t read, but do you want your librarian to be your neurosurgeon?” says Ono. Ono explains to me that, despite the success of large language models like ChatGPT, they still cannot be relied upon for correctness without checking by human reviewers, which presents an opportunity for verification.

Mathematical verification isn’t a new concept. In recent decades, mathematicians have come up with various systems with which to verify whether a proof is correct. The most popular of these systems is a programming language called Lean, which mathematicians can use to translate their handwritten proofs into a form that can be instantly checked by a computer. This can help with research-level mathematics, where it can take an inordinate amount of time from already-stretched researchers to verify whether a proof is correct.

Too much to check

A similar problem now exists in computer programming, because large language models produce vast amounts of code that frequently contain small and hard-to-spot errors, which has reduced many human programmers to act as babysitters for AI outputs.

It is this latter category that companies like Axiom Math and Harmonic see as their way to generate revenue, as the available cash for solving tricky maths problems is small. Just as a mathematical proof can be verified as correct with Lean or a similar programming language, so too can computer software, mathematically proving that it is correct and contains no bugs. “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.

While software verification is the main projected source of revenue for both companies, they also both have AI tools that are remarkably adept at solving some math problems in active research areas, and have generated checked proofs in areas such as algebraic geometry and number theory. Five papers written entirely with Axiom Math’s AI tools have now been accepted in mathematical journals. Ono couldn’t tell me Axiom Math’s exact roadmap for future challenges, but he said it aimed to have dozens of written papers by next year, compressing many years of work into weeks and days.

These companies are up against stiff competition, not least because tech behemoths have also been increasingly focused on maths-solving AIs. “Mathematics is wonderful for developing AI because it’s very measurable,” says OpenAI chief scientist Jakub Pachocki. “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.”

After a slow start, during which large language models struggled to make simple mathematical arguments, the most recent AI models have performed a string of stunning feats, first winning gold at the International Mathematical Olympiad, an elite high-school competition that was 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.

“The weaknesses that we saw six months ago were extremely apparent,” says Sébastien Bubeck at OpenAI. “There were fields of mathematics where the model was only saying nonsense. Today, I think it’s not quite like that.”

Unlike companies like Axiom Math and Harmonic, which have hired mathematicians to train their models to be specifically adept at maths, Bubeck claims OpenAI isn’t optimising its AI systems to be specifically good at mathematics, but rather trying to produce more generally intelligent systems, which also happens to be the overarching goal at OpenAI. “We are doing general AI training, and through this general improvement come out capabilities that are shocking all of us in terms of mathematics,” says Bubeck.

Whichever approach wins out, the future of mathematics being controlled by a small number of well-funded technology companies has created a sense of unease amongst mathematicians. All of this intense interest has arrived suddenly. What if it disappears just as fast?

“Right now, there’s a lot of money being put into this, and we’re going to miss it when it’s gone,” says Ravi Vakil at Stanford University. “It improves AI models in general, to become better mathematical thinkers. But 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.”

Paywalled theorems

Another possible future is that maths itself becomes a walled garden, where you can solve a problem only if you have enough money or access to the right AI model. While many of Axiom Math’s tools are currently free to use, the company couldn’t rule out that they might cost money at some point in the future.

“Some math today is already paywalled,” says Shubho Sengupta at Axiom Math. “[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 adds, however, that the “pushing of the bounds of knowledge of math forward should be free.”

Achim at Harmonic has a similar view. “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.” This doesn’t mean, however, that they won’t support mathematicians, he says. “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.”

Predicting the future is a notoriously tricky thing, especially for AI models, given their recent progress, but it is likely that for the foreseeable future, mathematicians will play a leading role. As I left Axiom, Ono compared the advent of maths-capable AI systems to when Srinivasa Ramanujan first burst onto the scene. Ramanujan was a self-taught mathematician from India whose mathematical discoveries arose largely from intuition, shocking the mathematical community in the early 20th century as they appeared to come out of nowhere.

Ono’s father, a Japanese mathematician who moved to the US in part because he was inspired by Ramanujan’s story, died in January. Ono recalls one of their last conversations together: “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.”