Maths nerds, get ready: an AI is about to write its own proofs

It might come as a surprise to some people that this prediction hasn’t already come to pass. Given that mathematics is a subject of logic and precision, it would seem to be perfect territory for a computer. However, in 2021, we will see the first truly creative proof of a mathematical theorem by an artificial intelligence (AI). As a mathematician, this fills me with excitement and anxiety in equal measure. Excitement for the new insights that AI might give the mathematical community; anxiety that we human mathematicians might soon become obsolete. But part of this belief is based on a misconception about what a mathematician does.If I were simply sitting in my office in Oxford doing long division to a lot of decimal places, computers would almost certainly have put me out of a job by now. But mathematicians are not merely calculators. We are storytellers, weaving together logical tales that take our readers on a strange journey – one with twists and turns, surprises and drama. Our characters are numbers and geometries. Our proofs are our narratives. We are not trying to prove every true statement about these numbers and geometries. Rather, we are making choices about the stories we tell.This is why I think that the challenge of AI coming up with a proof that will excite mathematicians is a much harder task than many might think. It will have to learn about our emotional world and to understand the proofs we care about. That is much more complex than simply bashing out equations that follow logically one from another.It’s not to say that there haven’t already been proofs that have exploited the computer as an essential partner in exploring mathematically deeper than the human mind can manage. One of the first was the proof that four colours suffice to cover any map, so no two countries with a common border are coloured the same. Once proved in 1976, a computer was used to check 1,834 maps that happened to be the building blocks of all maps. The computer was used like a telescope, allowing us to look further than the naked human eye could see.More recently, techniques of machine learning have been used to gain an understanding from a database of successful proofs to generate more proofs. But although the proofs are new, they do not pass the test of exciting the mathematical mind. It’s the same for powerful algorithms, which can generate convincing short-form text, but are a long way from writing a novel.But in 2021 I think we will see – or at least be close to – an algorithm with the ability to write its first mathematical story. Storytelling through the written word is based on millions of years of human evolution, and it takes a human many years to reach the maturity to write a novel. But mathematics is a much younger evolutionary development. A person immersed in the mathematical world can reach maturity quite quickly, which is why one sees mathematical breakthroughs made by young minds. This is why I think that it won’t take long for an AI to understand the quality of the proofs we love and celebrate, before it too will be writing proofs. Perhaps, given its internal architecture, these may be mathematical theorems about networks – a subject that deserves its place on the shelves of the mathematical libraries we humans have been filling for centuries. Marcus du Sautoy is the Simonyi professor for the public understanding of science and professor of mathematics at the University of Oxford and author of The Creativity Code: How AI is Learning to Write, Paint and Think WIRED WORLD 2021 The WIRED World in 2021 is an unmissable briefing on the ideas, trends, technologies, people and companies that will shape the coming year. Buy it now