Skip to main content

Proof as a social machine: will we need people in the age of computers

Venue: Birkbeck Main Building

In the summer of 2014 mathematician Tom Hales announced his proof of the 400 year old Kepler conjecture, a result that says, essentially, that the most efficient way of packing cannon balls (or oranges) into a box is the obvious one. What was remarkable about Hales’s proof was that every step had been written in formal logic and checked line by line by a computer – using software more usually used to show that complex computer programs are free from bugs. Hales had previously announced a proof in 1998, but his paper had been rejected by a top journal because the referees did not feel able to trust the complex calculations involved.

The Oxford mathematician Andrew Wiles, who proved Fermat’s conjecture, famously described mathematical research as being like “stumbling around in the dark” – eventually the light comes on, and you see the way forward, only to move on to the next problem, and more stumbling around in the dark.

Yet mathematicians like Wiles, and Hales, do solve immensely hard problems, ones where computers would even now be able to make very little progress. We’ll try and unpick the challenge of understanding the amazing things human mathematicians do, and how to best harness the combination of human skill and computer power to improve the process of producing mathematics, with people doing what people do best, and the computers taking care of checking all the details.


Professor Ursula Martin CBE joined the University of Oxford as Professor of Computer Science in 2014, holding a joint affiliation between the Mathematical Institute and the Department of Computer Science. Since 2014 her research has been supported by an EPSRC Established Career Fellowship, investigating cultures of mathematics to understand mathematics as a social machine. This has resulted in a highly interdisciplinary portfolio of work, using philosophy, social science and history alongside computer science research in artificial intelligence, argumentation theory and verification.

Prior to this she held a chair of Computer Science in the School of Electronic Engineering and Computer Science at Queen Mary University of London. At Queen Mary she was Vice-Principal for Science and Engineering (2005-2009), and Director of the impactQM project (2009-2012). She was appointed a Commander of the Order of the British Empire in 2012, and a Fellow of the Royal Society of Edinburgh in 2017. She is involved in many activities relating to women in science, and currently serves on the Royal Society's Diversity Committee.

Contact name: