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.