|Scheme:||Royal Society Research Professorship|
|Dates:||Oct 2009 - Sep 2014|
This researcher's grant funding has now finished. The information on this page may be out of date.
University of Cambridge
I am currently working in two areas, one mathematical and one "metamathematical" (meaning that it is about the processes of doing mathematics). The mathematical area is known as combinatorics. It studies discrete (as opposed to continuous) structures, such as networks or sets of numbers. Combinatorial questions arise in many contexts, both in the real world and within mathematics. For example, networks arise in contexts as diverse as the internet, design of electronic circuits, traffic flow, timetabling, and assigning radio frequencies. Combinatorics also has intimate connections with theoretical computer science. One of my favourite problems is the famous P versus NP problem, which asks, roughly speaking, whether finding answers to mathematical questions is as easy as checking whether answers are correct once they have been found. (The latter sounds much easier, and indeed most experts believe that it is easier. But it turns out to be extraordinarily difficult to prove this.) The metamathematical side of my research belongs at the interface between mathematics and artificial intelligence. I am working in the area of automatic theorem proving: that is, trying to write computer programs that can solve mathematical problems. Some people believe that mathematics requires a characteristically human intelligence -- not for the routine calculational tasks but for the deeper insights that go into proving a complex theorem. I strongly believe that one day all this will be automated, and as a result I find it a fascinating and challenging problem to understand what is going on in the brains of people like me when we do research. With a colleague, Mohan Ganesalingam, I have written a program that solves some easy problems. Over the next few years we intend to develop it so that it will solve harder ones and begin to show what computers are capable of. Our ultimate aim, which is a long way off, would be to put ourselves out of business!