The Startup Race to Make AI Mathematicians

The New Gold Rush in Mathematics

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.

Ken Ono, a professor at the University of Virginia, went on leave in 2025 to join Axiom Math, a start-up aiming to build a maths-focused AI. He had been asked by another company, Epoch AI, to help craft hard-to-solve maths problems to 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.

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. Its 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 have raised hundreds of millions of dollars.

Why Verification Matters

Large language models like ChatGPT still cannot be relied upon for correctness without checking by human reviewers. “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. This presents an opportunity for verification.

Mathematical verification isn’t new. In recent decades, mathematicians have developed systems like Lean, a programming language that can instantly check whether a proof is correct. This can help with research-level mathematics, where it can take an inordinate amount of time from already-stretched researchers to verify a proof.

A similar problem exists in computer programming, because large language models produce vast amounts of code that frequently contain small and hard-to-spot errors. Companies like Axiom Math and Harmonic see this as their way to generate revenue. Just as a mathematical proof can be verified as correct with Lean, 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, both companies also 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 reveal Axiom Math’s exact roadmap, but he said it aimed to have dozens of written papers by next year, compressing many years of work into weeks and days.

The Tech Giants' Approach

These start-ups are up against stiff competition from tech behemoths that 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, the most recent AI models have performed stunning feats, first winning gold at the International Mathematical Olympiad, an elite high-school competition, and more recently disproving an 80-year-old conjecture that some mathematicians thought they wouldn’t see progress on in their lifetimes.

Unlike Axiom Math and Harmonic, which have hired mathematicians to train their models to be specifically adept at maths, OpenAI isn’t optimising its AI systems to be specifically good at mathematics, but rather trying to produce more generally intelligent systems. “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 Sébastien Bubeck at OpenAI. Bubeck notes that six months ago, there were fields of mathematics where the model was only saying nonsense, but today that’s no longer the case.

The Future of Mathematics: Open or Paywalled?

All of this intense interest has arrived suddenly, creating a sense of unease amongst mathematicians. 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.”

Another concern 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, pointing to large hedge funds that do mathematical modelling inaccessible to others. However, he adds 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.” But he also says that if the company believes math is important for the future, they will always want to support mathematicians. “I don’t think any company sees mathematicians as a way to extract all the value for the company.”

As I left Axiom, Ono compared the advent of maths-capable AI systems to when Srinivasa Ramanujan first burst onto the scene. Ono’s father, who died in January, had told him in 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.”