The Rise of Chatbots: How Mathematicians Use AI

Original Author: Davide Castelvecchi

As the enthusiasm for chatbots reaches unprecedented heights, mathematicians are also exploring how artificial intelligence (AI) can assist their work. Researchers state that whether it’s verifying human-written proofs or proposing solutions to different problems, automation is changing mathematics—and not just in the computational realm.

Andrew Granville, a number theorist at the University of Montreal, said, “We are talking about a very specific question here: Will machines change mathematics?” A recent seminar at UCLA explored this question, hoping to bridge the gap between mathematicians and computer scientists. “Most mathematicians completely do not see the opportunities.” said Marijn Heule, a computer scientist at Carnegie Mellon University and one of the event’s organizers.

The Fields Medal (Fields Medal) is the highest honor in mathematics. In October, Akshay Venkatesh, a Fields Medalist and a researcher at the Institute for Advanced Study in Princeton, opened a dialogue on how computers will change mathematics at a seminar held in his name. Two other Fields Medalists—Timothy Gowers from the Collège de France and Terence Tao from UCLA—also led discussions in this debate.

Kevin Buzzard, a mathematician at Imperial College, said, “The fact that we can attract Fields Medalists and world-class mathematicians to join us shows that this field is heating up in unprecedented ways.”

One topic of debate is which types of automation tools are more practical. AI mainly falls into two categories. One type is “symbolic AI,” which requires programmers to embed logical rules or computations into the code. “This is what people think of as ‘reliable and traditional AI’,” said Leonardo de Moura from Microsoft Research in Washington.

The other type of AI is based on artificial neural networks, which have achieved great success over the past decade. For this type of AI, computers need to start from scratch, learning patterns by digesting vast amounts of data. This approach is called machine learning, which underlies both “large language models” (including chatbots like ChatGPT) and systems capable of defeating human players in complex games or predicting protein folding. Symbolic AI is itself very rigorous, while neural networks can only make statistical guesses, and their operation is mysterious and unknown.

De Moura has made some early progress in mathematics with symbolic AI by building a system called Lean. This is an interactive software tool that requires researchers to write out each logical step for every problem, down to the most basic details, while ensuring that it is mathematically correct. Two years ago, a team of mathematicians successfully translated a crucial but difficult-to-understand proof—so complex that even its author was unsure—into the language used by Lean, ultimately confirming that the proof was correct.

The team stated that this process helped them understand the proof, and even helped them find ways to simplify it. “I think this is more exciting than verifying results,” de Moura said, “Even in exaggerated dreams, we wouldn’t dare to think this.”

In addition to making independent research easier, such “proof assistants” can also eliminate what de Moura calls the “trust bottleneck,” changing collaboration among mathematicians. “If we collaborate, I might not trust the part you did. But ‘proof assistants’ can show collaborators that they can completely trust the work you’re responsible for.”

The other extreme is chatbot-style, large language models based on neural networks. At Google in Mountain View, former physicist Ethan Dyer and his team developed a chatbot called Minerva specifically for solving mathematical problems. Essentially, Minerva is a super-intelligent version of the auto-complete feature in messaging apps: by training on mathematical papers from the arXiv database, it has learned to write out detailed steps for solving problems in a way similar to how some apps predict words and sentences. Lean communicates in a way similar to computer code, but unlike Lean, Minerva can understand problems and provide answers in conversational English. De Moura said, “Being able to automate the solution of some of these problems is itself an achievement.”

Minerva not only demonstrates the capabilities of this approach but also exposes its potential limitations. For example, it can accurately factor integers into prime numbers—numbers that cannot be divided by smaller primes. However, if the numbers exceed a certain size, it will start to make mistakes, indicating that it has not yet “understood” the general method involved.

Of course, Minerva’s neural network seems to be able to grasp some universal techniques, not just statistical patterns, and the Google team is trying to understand how it does this. Dyer said, “Ultimately, we want a model that can brainstorm with you.” He said, this model could also be useful for non-mathematicians who need to extract information from specialized literature. By learning from textbooks and connecting with specialized mathematical software, Minerva’s skills could also be expanded.

Dyer stated that the motivation behind launching the Minerva project was to see how far machine learning methods could go; a powerful automation tool that assists mathematicians might combine symbolic AI techniques with neural networks.

In the long run, will AI programs always play a supporting role? Or can they also conduct independent mathematical research? The ability of AI to generate correct mathematical propositions and proofs may become stronger, but some researchers worry that the vast majority of these propositions or proofs will be uninteresting or incomprehensible. At a seminar last October, Gowers suggested that researchers might find ways to teach computers some objective standards of mathematical relevance, such as whether a small proposition can represent many special cases, or even connect various branches of mathematics. He said, “To take theorem proving to the next level, computers must learn to distinguish what is interesting and worth proving.” If computers can do this, the future status of humans in this field becomes uncertain.

Erika Abraham, a computer scientist at RWTH Aachen University, is more optimistic about the future of human mathematicians. “The intelligence of AI systems can only reach the level we program them to,” she said, “It’s not the computer that’s intelligent, but the person programming or training it.”

Melanie Mitchell, a computer scientist and cognitive scientist at the Santa Fe Institute, stated that mathematicians will not lose their jobs for now unless a major flaw in AI can be overcome—namely, they still cannot extract abstract concepts from concrete information. “AI systems may prove theorems, but you first need to propose the interesting abstract mathematical concepts behind those theorems, which is much harder than proving theorems.”