“Exponentially exploding,” mathematician Thomas Bloom told me by phone, describing the flood of new results in his field. Little did he know that hours later, OpenAI was going to post 722 mathematical manuscripts an unreleased AI model had produced.
The firehose of new work lends new urgency to the question: How is AI changing mathematical discovery? In their race for headline-grabbing breakthroughs, AI companies typically do not disclose their methods and data. That competition among AI companies threatens to overwhelm human collaboration and understanding.
This tension had been playing out in miniature on a website Bloom runs that tracks progress on more than 1,000 problems originally posed and collected by Paul Erdős, one of the 20th century’s most prolific mathematicians. Here, people used to collaborate to discuss open problems, or ones for which the best solution either hasn’t been found or isn’t known to the greater math community. But increasingly, visitors were competing to close open problems with AI proofs that they often didn’t understand. Bloom, a mathematician at the University of Manchester in England, doesn’t want to spend his days refereeing AI-generated work. So, soon after we spoke, and before he knew that OpenAI would be announcing its latest results, Bloom posted that he’d no longer tag problems as open or solved, and he also closed comments.
It’s definitely exciting that AI can tackle so many open problems so quickly. But can it help mathematicians understand the answers and build on them?
Just two days after OpenAI’s deluge of results, the peer-reviewed edition of a Google DeepMind study became public. First reported in a preprint earlier this year, it offers an inside look at how one AI system tackles open math problems. The system called AlphaProof Nexus solved 9 Erdős problems and made a number of other interesting mathematical advances, researchers report October 8 in Science.
The report includes a detailed description of how the results were obtained. Plus, human mathematicians vetted many of the proofs. That’s “quite different” from how OpenAI and Anthropic are handling their math results, Bloom says.
“The ultimate objective of any AI for math research,” says research scientist and study co-author Swarat Chaudhuri of Google DeepMind in London, should be “to advance mathematics as done by human mathematicians.”
A look inside an AI math machine
In the recently published study Chaudhuri and his colleagues tested different configurations of their system. To tackle a collection of 353 open Erdős problems, they used multiple agents powered by the Gemini language model. These could call on AlphaProof, an AI model specially trained to do math, and the inspiration for the name of the overall system, for difficult steps. The agents also relied on Lean, math software that identifies steps that remain unproven, to check their logic. The agents shared their work, circulating promising proof attempts and discarding ones that weren’t going well.
The team also tested a simpler setup on the nine problems the full system solved. Independent Gemini agents worked through proofs using Lean’s feedback, without sharing attempts or consulting AlphaProof. That setup solved all nine, too. It was cheaper—using fewer computing resources—than the full system on easy problems and more expensive on the two toughest ones. The team did not establish whether the simpler setup would solve any of the problems the full system had missed.
The fact that the simpler setup could solve the same nine problems as the full system surprised Chaudhuri. It suggests that increasingly capable language models can tackle research mathematics with relatively simple checking tools.
But computer-checking comes with a caveat. Lean checks only the statement it’s given, as it is written in its code. And a mathematical statement may be incorrectly translated to or from Lean code. An October 6 preprint shows why this translation matters. In the paper, the researchers pinpoint mismatches between parts of OpenAI’s written Navier–Stokes proof and its Lean counterpart. The mismatches do not mean the written proof is wrong, the team writes, but they note that a valid Lean proof does not automatically validate an AI-generated math paper.
That’s why the vetting human mathematicians did for the DeepMind publication is so important. “The human mathematician has to really think through the problem and set goals for the system,” Chaudhuri says. And even if the system failed to finish a proof, its checked steps helped mathematicians focus on the remaining gaps. “Math is ultimately a human art,” Chaudhuri says. “The system enhances the human user’s insights, and the human user is able to guide the system with new ideas.”
With math ability comes responsibility
The mathematical results that the AlphaProof Nexus system achieved are “not really at the top level of importance,” says Bloom, who wasn’t involved with the work. But that underscores the team’s more measured approach. Google DeepMind, he says, is “trying to be more responsible with the science,” while companies like OpenAI are using math to showcase their software. OpenAI’s papers and accompanying Lean proofs were entirely AI-generated, leaving it up to the math community to work out what’s useful or useless.
OpenAI says they worked with an independent advisory group to develop best practices on how to share their AI math results. But that group has said their advice was to not test unreleased AI models on advanced math, guidance the company clearly ignored.
The company’s fast-moving, competitive approach continues to alienate mathematicians such as Bryna Kra of Northwestern University in Evanston, Ill. She says the company made some improvements in their efforts to cite past literature. And she’s excited about AI’s potential to solve important problems in math. But there is widespread concern, she says, that AI models have accessed people’s unpublished work. “We had a healthy, collaborative, sharing culture that is being destroyed,” she says. “Now, people are wary of sharing their ideas.”
Not all mathematicians feel this way about AI. The technology is “making math more accessible,” says Andrew Turner, who wonders why a small group of mathematicians should get to decide how we solve problems. Turner, who studied math and physics and is Now CTO of the company Plasma AI, based in New York City thinks “math is becoming engineering.” And doing math with machines will allow people to “answer questions previously unfathomable.”
A few days after Bloom shut down the competition on his website, Plasma AI announced a new website to track progress on Erdős problems. They will welcome AI results.
Bloom doesn’t see math as a Silicon Valley–esque move-fast-and-break-things competition. I agree, and hope that curious people will continue to explore problems they care about, with AI helping rather than taking over. At the end of his post announcing the changes to his website, Bloom wrote something that makes me tear up every time I read it. I hope everyone, even the most enthusiastic AI users, can find the time for this type of work: “Be confused, be stuck, be inspired. Find a messy proof, then find a better one,” he wrote. “Get tired, get hungry, get into a flow state. Argue, laugh, give up, drink some coffee and attack it again. Be human. Let your brain be open.”
