AI versus mathematics?
This summer the world of mathematics was thrown into turmoil. From around the middle of May onwards it became clear that artificial intelligence had gained the ability to solve some of the hardest mathematical problems in existence. Developments culminated on September 8th with the claim that one of OpenAI's systems had solved the Navier-Stokes millennium problem — one of seven problems considered so important that back in 2000 the Clay Mathematics Institute offered $1 million for a solution of any one of them.
Discussions immediately ensued within the mathematics community. Did AI really solve these problems on its own? What do the results mean for the future of mathematics? And how should the community respond?
Henry Bradford of the Department of Pure Mathematics and Mathematical Statistics (DPMMS) has been at the forefront of research into one of the problems solved by AI: the existence of non-sofic groups. His experience and thoughts reflect many of the points mathematicians have been discussing.
Breaking news
Bradford was drawn into the AI swirl on July 31st when, sitting with his feet in his College's swimming pool, he received news of a claim by OpenAI that it had proved the existence of non-sofic groups. The next day OpenAI announced the result on its website, along with solutions to 9 other long-standing mathematical problems. It said, "Today we are sharing a selection of ten results to problems that have been open and have seen no progress on the main result for at least a decade."
When receiving the initial news Bradford and his colleague Francesco Fournier-Facio, then Herchel-Smith Fellow at DPMMS, immediately took a look. "Francesco invited me onto a call with himself and Alon Dogon, now at Columbia University in the US. We spent an hour or so reading through this proof, trying to understand the big ideas and convincing ourselves that it was correct. We were also in contact via WhatsApp with Michael Chapman of Tel Aviv University, an expert on [some of the technical details]."
The proof was indeed correct, the group decided, but they also found some minor errors that no human familiar with the area would be likely to make. "This gave us a strong sense that this really was work that had been generated by an AI model." The team sent some corrections to OpenAI, for which they were duly acknowledged in a subsequent OpenAI publication.
An elusive group
The team were worried, however, about the claim that there hadn't been human progress on the problem in ten years.
The result in question involves mathematical objects called groups. We won't go into what these are (find out here), suffice to say that some groups are finite and some are infinite.
Infinite objects are harder to understand than finite ones, so mathematicians have come up with a way of approximating infinite groups by finite groups. An infinite group that has such an approximation is called sofic, after the Hebrew word for "finite". The question was whether all groups are sofic or whether there are also infinite groups that can't be approximated by finite ones: non-sofic groups. Mathematicians had long suspected that there were such unapproximable beasts, but had not been able to find one.
But OpenAI's system, called Astra, did. Its proof that the group it found really does fit the bill comes in two parts. The first part delivers a specific criterion: any group fulfilling this criterion would necessarily be non-sofic. The second part constructs a group that does fulfill the criterion.
Bradford and his colleagues suspected that the first part of the proof was really the hard bit. Once you have the criterion, finding a group that satisfies it should be comparatively easy, at least for experts. "Francesco stayed up all night between July 31st and August 1st [trying to find] a different example of a group that satisfied the criterion," says Bradford. He succeeded within 24 hours.
No human progress?
The mathematical meat, then, really does lie in the first part of Astra's proof. It takes an approach that not many human mathematicians would have banked on in their search for non-sofic groups. But it's not an approach that was unknown to them. Specifically, there have been two results with powerful potential. One was proved in 2016 by the Hungarian mathematician Gábor Kun. The other is from 2019 and due to Kun and the German mathematician Andreas Thom.
The problem lay in connecting these two results. The logic of mathematical proofs sometimes enables you to line them up. For an illustration, think of the statements "every animal that meows is a cat" and "every cat is a mammal". If you know that both statements are true, then you can deduce that the statement "every animal that meows is a mammal" is also true.
A similar lining-up of the Kun and Kun-Thom results would lead to powerful leverage for finding a non-sofic group. The trouble was that an exact line-up didn't work: the conclusion of the first result didn't quite serve as the hypothesis of the second.
And this is where Astra's achievement lay: it found a setting that allowed the two results to be connected, which then led to the all-important criterion for non-sofic groups. Its proof, then, relies heavily on two human results published in the past decade. "In the opinion of myself and my colleagues there isn't any proof there without those two prior theorems," says Bradford.
Is AI listening?
Thom expressed his disquiet at the apparent underplaying of human contributions in an email to OpenAI (find out more in this blog post by Thom). The response was that the "no human progress" part of the statement referred loosely to all ten of the problems that OpenAI had announced on August 1st. OpenAI did subsequently change the wording of the announcement. (You can read more about the sequence of events, as well as the mathematics involved in this post by Fournier-Facio on the Proofs and Prompts blog.)
A PR faux pas, you might say, but there's also a deeper issue worrying Bradford and other mathematicians. Many use AI in their work. To help them find ideas, work out aspects of their maths, and help with writing, for example. Mathematicians working on the sofic group problem used Large Language models (LLMs) owned by OpenAI, and so did mathematicians involved with the Navier-Stokes Millennium problem.
Could the conversations the mathematicians had with the LLMs have been used by OpenAI's systems to solve the high-profile problems? This could have happened through humans providing the information to the system through prompts. Or it could have happened through the system being trained on data from the conversations.
When Thom asked OpenAI about this with regards to the sofic groups problem, the answer was an unequivocal no (though Thom later came to feel it was somewhat misleading). When Tristan Buckmaster, a mathematician involved with the Navier-Stokes problem, asked the same question the answer wasn't so reassuring. Eventually OpenAI confirmed that Buckmaster's input to its LLMs from the previous two months could "not have influenced the system in any way, including through training."
"But Buckmaster and [his collaborator Levent] Apölge had been interacting with these AI models for at least a year," says Bradford. "Also it's not clear to me, as a non-expert in AI, how one can be sure of what the LLMs are doing behind the scenes. They are notoriously difficult to interrogate as to their internal workings and have in several high-profile instances disobeyed the instructions of their human handlers and gone rogue in various ways." (Indeed, on September 29th OpenAI cancelled the release of GPT-6.1 Astra over safety concerns.)
As far as the Navier-Stokes result is concerned, there is now a full-blown priority controversy. As events were unfolding, Tristan Buckmaster released a statement of his version of events. We should also note that there's controversy around whether AI really did solve the original Navier-Stokes Millennium problem. And as we were about to publish this article, OpenAI announced the solution of a broad range of other results, saying it consulted "with the independent Advisory Group on Mathematics and Artificial Intelligence at the Institute for Advanced Study to develop best practices, and we have drawn on their advice and public recommendations to inform how we release these results."
The future of maths
Some have suggested that human carelessness carries most of the blame for issues surrounding due credit, and that the problem may eventually go away — perhaps as part of an overhaul of the entire credit system.
But there's also a more fundamental question: what does AI getting good at hard maths mean for the survival of the field? At the moment, AI's attempts at hard problems are prohibitively expensive: OpenAI spent $15 million on the Navier-Stokes problem and we don't how much it, and other companies, may have spent on problems its systems failed to solve. But it's not difficult to imagine models eventually becoming cheaper to run.
"I think there's a bright future where AI working in service to the mathematical community helps us understand the mathematical universe a lot more," says Bradford. "On the other hand there's also a dark future where our understanding ends up being hampered by the influence of AI."
A major concern is what AI developments mean for the next generation of mathematicians. "At the moment the way that young mathematicians demonstrate their understanding and build their careers is by writing papers and proving new theorems," says Bradford. "In a future where AI resources are abundant, papers and proofs of theorems cease to be a certificate of understanding. What now is the process by which young mathematicians are able to demonstrate their credentials?"
If, as a result, research mathematics ceases to appear as a viable career, we may run out of humans who truly understand the ideas behind the results that are being proved. It's a worry that has been expressed by many, including the prominent Cambridge mathematician Timothy Gowers.
A remedy might involve letting go of the centuries-old habit of using problem-solving as a proxy for understanding. Communicating the solutions clearly (something that AI currently appears to be terrible at), digesting and fitting them into the overall landscape, and the building of theories have always been important aspects of mathematics. Indeed the prominent mathematician Terence Tao explored such a re-definition of mathematical goals in an influential talk at the International Congress of Mathematicians (ICM) in July.
But many in the mathematics community are concerned that, at a time when higher education is facing funding pressures, we may not achieve such a shift in time. "One can easily imagine that universities, with all the financial problems they are facing, may be tempted to say, what more need do we have for the human mathematicians that are currently staffing our departments?" says Bradford.
He is not alone in his worries. On September 11, just after the announcement of the Navier-Stokes result, 25 prominent mathematicians, including Tao, issued a statement warning that AI companies flexing their muscles on maths problems is detrimental to maths and the mathematical community. "The goals of the AI companies and the goals of the mathematical community are severely misaligned," the statement reads. "We see these as part of broader alignment issues impacting other scientific and creative professions, as well as the whole of society,"
The declaration has been endorsed by over 8,000 mathematicians and counting, including Bradford. But others argue that criticising AI companies won't put the cat back into the bag. As Gowers put it in a blog post, "Under the circumstances, I think the best we can do is recognise the changes that are coming and try to work out the least unsatisfactory way of dealing with them."
Superhuman mathematics?
A lot hinges on how good AI is going to get at doing all aspects of maths, not just problem-solving. Bradford thinks it's unwise to bet either for or against it developing human, even superhuman, capabilities. In the immediate term, he says, the mathematical community needs to find a consensus on how to deal with the problems at hand: issues surrounding due credit and how to keep the next generation on board.
But if AI does become better at maths than we are, will that spell the death of human mathematics? And would that even matter? That will depend on what we value. "If we decide as a society that human understanding of mathematical ideas still has value, then there is still a role to be played by human mathematicians," says Bradford.
The severe misalignment declaration points out that current mathematical culture is rooted in human interaction. "The mathematical community functions, in many ways, as a miniature version of humanity. It consists of individuals using a wide variety of different approaches, joined by core values." The aim of the endeavour is human understanding of the world. And that, Bradford says, has always been important to us — be it through science, through art, or through mathematics.
About this article
Henry Bradford is a Fellow and College Teaching Officer at Christ's College Cambridge, and a member of the University of Cambridge’s Department of Pure Mathematics and Mathematical Statistics.
Marianne Freiberger is Editor of Plus. She interviewed Bradford in September 2026.