The Hitchhiker’s Guide to the Galaxy says 42 is the answer. But what is the question?
Professor Kevin Buzzard asks: how do we teach AI to prove mathematical theorems?
A lot of people think mathematics is easy for computers, because they can calculate pi to a million decimal places or add up numbers super quickly. And yes, computers are extremely good at calculation – they can do it better and more reliably than humans and they’ve been doing that for decades.
But proving mathematical theorems is a different challenge. It’s very easy to teach AI the axioms – or basic assumptions – of mathematics. If you can get the computer to do them all in exactly the right order, then you’ll get to the proofs you want. But working out the right order, when you have almost infinite possibilities, is surprisingly tricky. Humans are really good at it because humans have some insight that AI doesn’t have yet. Mathematics is an art, as well as a science.
I’ve been given a five-year grant to give AI some of the tools to tackle mathematical theorems. We take an existing proof – such as Fermat’s Last Theorem, first proposed in 1637 and proved by Andrew Wiles in 1994 – and teach it to the computer. With the help of – hopefully – lots of citizen mathematicians around the world, I’ll be translating that human proof into a language that computers understand. At the end of the project we’re going to have this gigantic database – the complete proof of this extremely hard theorem down to the axioms. The AI will be able to look at it and say: that’s what a complicated mathematical proof looks like; that’s maybe how I should start thinking about mathematics.
The potential applications are exciting. If we can teach computers how to do this stuff, and get mathematicians using these systems, then mathematicians are less likely to make mistakes. Mistakes are problematic because mathematics builds on other mathematics. The step after that is teaching AI to prove theorems by themselves. I want to get to the point where computers are better than humans at it. Then I can retire, because we’ll just let computers solve all the hard problems.
Professor Kevin Buzzard is Professor of Pure Mathematics in the Department of Mathematics, Faculty of Natural Sciences