AI is getting better at handling mathematical research
lucadp/Getty Images
Is an artificial intelligence revolution about to transform mathematics? Some prominent mathematicians think so, thanks to automated tools that can help write proofs suddenly showing impressive leaps in capability, with the potential to change the way maths research is done.
Around 100 of the world’s top mathematicians gathered at the University of Cambridge in June for a conference whose theme was based on whether computers might help mathematicians resolve some long-standing problems over how to check that their proofs were correct. This process, known as formalisation, doesn’t necessarily have to involve artificial intelligence, and indeed a similar meeting held at Cambridge in 2017 made no mention of AI.
But eight years later, AI has come on by leaps and bounds, most notably with the success of large language models powering tools like ChatGPT. This has attracted new interest to the question of how AI might affect mathematics, from automatically translating human-written proofs into a formal, computer-checkable language, to constructing proofs themselves.
“It’s a little bit overwhelming,” says Jeremy Avigad at Carnegie Mellon University in Pennsylvania, who helped organise the meeting. “It’s nice; I’ve been doing this for a long time and it used to be kind of a fringe, niche thing. All of a sudden, I find myself popular.”
Two of the talks were put on by Google DeepMind, which last year made headlines when its AI system, AlphaProof, achieved a silver medal score at the International Mathematical Olympiad (IMO), a prestigious competition for young mathematicians and a long-standing target for AI systems. “If you talk to mathematicians and ask them about the [AlphaProof] IMO results, you would have had different reactions. I think most would say that these are pretty hard high school problems, but maybe some other mathematicians would call them trivial,” says Thomas Hubert, a research engineer at DeepMind.
Hubert and his team showed that AlphaProof could go beyond the IMO competition, to aid in formalising a small part of the prime number theorem, an important result in number theory. The mathematics had already been converted to Lean, a programming language, but AlphaProof was able to prove the theorem and then check it was correct. “I wanted to do a demo of how AlphaProof could be used in real life,” says Hubert.
Morph Labs, a US-based AI startup, also demonstrated an AI tool called Trinity, which is designed to translate proofs completely automatically, starting from the handwritten mathematical notation and generating a fully formalised and checked proof in Lean. Bhavik Mehta at Imperial College London, who has consulted with Morph Labs, showed an example of Trinity proving a theorem relating to the ABC conjecture, which infamously remains the subject of intense debate about whether it is true or not – something that formalisation could address.
Though this proof was only a tiny building block of the entire proof needed for the ABC conjecture, and Trinity required a slightly more detailed version of the handwritten proof than the original paper, many people were surprised at how much correct mathematical code was generated by the tool.
“The difference between what Morph did and what had gone before was that they took an entire maths paper, albeit one from 1962 that was only four pages long, a human [then] broke the argument down into small pieces and then a machine just translated the entire thing into Lean,” says Kevin Buzzard at Imperial College London. “I’m not sure we’ve seen anything like that before.”
However, it still isn’t clear how this will work for other areas of mathematics, says Mehta. “This was essentially the first attempt, and the first attempt worked, maybe it got lucky.”
Christian Szegedy at Morph Labs claims that once the tool is fully up and running, it will quickly progress. “Once a feedback loop is established and we don’t need the amount of hand-holding that this theorem needed… then it becomes basically a chain reaction and we can do all of mathematics at once,” he says.
Tools like these are already at the point that they could be incredibly helpful to mathematicians, says Timothy Gowers at the University of Cambridge. “It will just take some work to create them, and there seem to be a lot of people who are keen to do precisely that, so I think that over the next few, and I really mean few, anything from one to five years, there will have been changes to how we do maths that will rival in importance the changes to mathematical practice brought about by email, LaTeX [the standardised maths notation], arXiv [an online paper repository] and Google.”
But not all mathematicians agree that the Morph Labs paper was so impressive. Rodrigo Ochigame at Leiden University in the Netherlands cautions that we don’t know the full details of the work. “They posted only a single, possibly cherry-picked, output of their system without writing a paper or sharing basic information about their methods. They didn’t even say if they tested their system on any other theorems,” he says. “When asked by the audience about the amount of compute used by the model, they repeatedly declined to answer, making it difficult to assess the significance of their result.”
And scepticism remains about just how useful AI tools can be. Most mathematicians still work without the use of automated tools, and it is unclear whether they will change their minds as the tools improve, says Minhyong Kim at the International Centre for Mathematical Sciences in the UK. “Mathematics and mathematicians are incredibly diverse in their inclinations. I imagine some people will end up using AI tools very effectively and creatively, while some will try to maintain a distance.”
“People underestimate the complexity, creativity and subtlety of mathematical research,” says Ochigame, which is why so much research is still done using pen, paper and deep thought. “There is a huge gap between high school math competitions, such as the IMO, and cutting-edge research,” he says.
Topics:
