Mathematics is undergoing the biggest change in its history

In March 2025, mathematician Daniel Litt made a bet. Despite advances in artificial intelligence in many fields, he thought his topic was safe, betting with a colleague that there was only a 25 percent chance that an AI could write a math paper on the level of the best human mathematicians by 2030. Only a year later, he thinks he was wrong. “I now expect to lose this bet,” he said on his blog.

Mathematicians have been surprised by the rapid improvements in AI’s ability to solve problems and produce proofs. “A few years ago they were virtually useless even for solving high school math problems, and now they can sometimes solve problems that actually appear in a mathematician’s research life,” says Litt, who works at the University of Toronto.

This progress is coming faster than many predicted, with mathematicians warning that their profession is experiencing one of the most rapid evolutions the field has ever seen. “We are running out of places to hide,” Jeremy Avigad of Carnegie Mellon University in Pennsylvania wrote in a recent essay. “We must accept the fact that AI will soon be able to prove theorems better than us. »

It is not a single event that causes such reactions, but the constant mathematical progress demonstrated by AI. Last year, companies like OpenAI and Google DeepMind won gold medals at the International Mathematical Olympiad, an elite competition for high school students that many experts had previously considered beyond the scope of AI tools. In January, mathematicians began using similar tools to solve long-standing problems posed by Hungarian mathematician Paul Erdős.

Now, in two separate developments, AI has begun to tackle more complex mathematics, solving real research problems and helping to automatically verify cutting-edge proofs, which could traditionally require a huge amount of work for teams of mathematicians.

In February, Nikhil Srivastava of the University of California, Berkeley and his colleagues launched the First Proof project with the aim of finding a more realistic benchmark for testing AI’s mathematical abilities. The first phase of the project included 10 problems that the researchers had to solve as part of their work, from very different mathematical fields.

“These were natural problems in our daily research,” says Srivastava. “They came from a typical distribution of difficulty. They weren’t very difficult, but they weren’t routine either. There was definitely a range.”

Proof of Progress

Once the problems were made public, the solutions began to flow. Researchers from tech companies including OpenAI and Google DeepMind were among those who attempted to solve the problems in the early evidence with their own AI models. OpenAI claims to have answered half of the problems correctly, according to “expert feedback”, while Google DeepMind received a score of 6 out of 10, according to the mathematicians consulted for each problem.

“Things have changed so quickly,” says Thang Luong of Google DeepMind. “For us, AI has now really become a serious collaborator, either to produce serious research work, or, in the case of First Proof, it can also propose a solution on its own.”

Google’s math AI tool, called Aletheia, uses a compute-intensive version of its Gemini AI chatbot, combined with a verification algorithm to look for flaws in possible solutions. It can then iteratively produce improvements itself until it arrives at an answer. Google hasn’t publicly disclosed how many iterations Aletheia needed to fix these problems, making it difficult to gauge its quality, but mathematicians are still impressed.

Not all problems have been unanimously agreed to be resolved. For example, for problem 8, which concerns a niche area of ​​geometry, only five of the seven experts surveyed by Google agreed that the proposed solution was correct. Ivan Smith of the University of Cambridge, who was not involved in Google’s efforts, says AI appears to be taking a common-sense approach to this problem and is showing good progress. “If it was a doctoral student coming back with their thoughts, that would be encouraging and build confidence in the veracity of the result,” says Smith.

This highlights a problem with AI-generated evidence: verifying it is hard work. It would be easy to find ourselves in a situation where AI can generate evidence faster than humans can verify it. If a theorem is proven by an AI, but no one is there to verify it, has it been proven? AI can also help here.

Technology is rapidly improving to translate handwritten natural language evidence, like the problems posed in First Proof, into a format that can be verified by a computer, a process called formalization.

AI company Math, Inc. recently surprised mathematicians by announcing that its AI tool, called Gauss, had formalized a prize-winning proof and verified that it was correct. The proof concerned how many spheres could be packed into a space and was the subject of Maryna Viazovska’s 2022 Fields Medal, often called the Nobel Prize in Mathematics.

The effort to formalize Viazovska’s work began with a small group of mathematicians in late 2024, working separately from Math. Inc, which hoped to manually translate the problem into computer code. They first looked at Viazovska’s spherical packing solution in eight dimensions. While they were making steady progress, Math, Inc., which then assisted the researchers, announced that it already had a complete proof, then a more general version of a result for 24 dimensions.

Bhavik Mehta of Imperial College London and his colleagues had initially outlined a rough plan for how to formalize the work, and had also proposed important mathematical definitions. Without this, the AI ​​would not have been able to complete its proofs, says Mehta.

“We had made all the parts, but we hadn’t written the instruction manual on how to put them together,” says Chris Birkbeck of the University of East Anglia, UK, who is also part of the team.

A new style of mathematician

The final proof was about 200,000 lines of code, which represents about 10% of all formalized mathematics in existence. Although this code is likely to be about 10 times longer than what a human would have produced to accomplish the same task, it is nonetheless a huge achievement, says Johan Commelin of Utrecht University in the Netherlands. “It’s a big deal. It’s Fields Medal work, and it’s being self-officialized.”

Similar efforts should now be possible in a large number of other fields, Commelin believes, which could transform the way mathematics is practiced. “The future we all think about is that we will have tools that automatically formalize new research and mathematics papers and report whether there are errors or not,” Commelin says. “This will have huge implications, for example, for peer review and refereeing work. »

Faced with a future in which an increasing share of mathematics will be performed by AI, some mathematicians, like Avigad, are sounding the alarm about the harmful effects this could have on our ability to practice and invent new mathematics.

Using machines to solve the kinds of problems posed in First Proof can produce real-world evidence, says Anna Marie Bohmann of Vanderbilt University in Tennessee, but we’re losing “the opportunity to learn,” she says. “Struggling to create and formulate new ideas and solve new problems is one of the primary ways that mathematics students and professionals consolidate their knowledge. »

Tony Feng, a member of the Aletheia team at Google DeepMind, shares the same sentiment and is cautious about using the tool itself. “Often I feel like I should do my own homework and go through the process of building my own intuition.”

Even formalizing proofs can generate important insights, Mehta says, and he and his colleagues will now have to untangle AI’s 200,000 lines of evidence to determine what might be useful for other projects.

But mathematicians still hope they will have a place in an increasingly machine-driven future. Looking to history, Commelin says that manual calculations were once an important part of the mathematician’s profession, but are now done automatically. “I think similar things will happen here, where we will radically change what we do, but in 10 or 20 years we will still recognize what we do as mathematics, in a new style.”