Computers and Proof
In the final session of the Virtual HLF, as part of a discussion on the topic ‘Where can computer science and mathematics interact fruitfully?’, the conversation turned to the question of proof. In the words of Fields medalist Efim Zelmanov, “What distinguishes mathematics from all other scientists is proof as the criterion of truth,” and he wondered how the computer scientists present view this cornerstone of mathematics: the idea of mathematical proof.
Of course, computers are often used in mathematics, especially in applied maths, since often many complex calculations are needed to model real-world systems; even some pure mathematical concepts, like large detailed algebraic structures, require a bit of computer assistance in order to crunch through the calculations needed to understand huge group structures.
Many of the well-known examples of computer proofs merely employ computers in checking lots of possibilities. The most famous is probably the Four Colour theorem – this states that for any way of dividing up a flat plane into regions (like a map), there’s always a way to colour them all in using four or fewer colours, so that any two regions that touch along an edge are different colours. It was conjectured back in the 1850s, but it continued to vex mathematicians (and mapmakers) until the 1970s.
The proof involved creating a collection of thousands of smaller regions of map which could be combined to create any map, then checking that all of these could be coloured using four colours. The proof involved a huge amount of computation, checking each combination, and for some at the time, it was seen as less of a formal proof than something done by hand – since what if the computer had made an error, and we didn’t know?
The program written to check all the cases could be seen as a computerised form of proof – given that the mathematicians writing it had proven that if this program ends with a particular result, the theorem must be true. Similar proofs have been made for other problems involving large amounts of checking, including one that shows the game of Connect Four can always be won by the first player.
But can computers contribute to mathematical proof in a way that’s not just performing calculations you’re too busy (or have too annoyingly finite a lifetime) to work out by hand? Since all of maths is built on simple ideas like logic and set theory, some types of proof can be boiled down into a simple succession of logical statements – if this then that, or for all things of this form, this is true. Formal logic, which dates back to Aristotle, underpins a lot of mathematical thinking.
Mathematicians and philosophers Bertrand Russell and Alfred North Whitehead wrote Principia Mathematica, published in 1910-1913, in which they formalised Frege’s propositional calculus to really boil maths down to its simplest statements and axioms. Principia included a proof that 1+1=2 which took over 200 pages! – a consequence of making no assumptions and really digging into what exactly we mean by 1, 2, plus and equals.
Since computers became widely available, mathematicians have made use of them in their work, and as early as the 1950s people tried to build computer systems that could compute proofs in formal logic terms. Logic Theorist was a computer program written in 1956 by Allen Newell, Herbert A. Simon and Cliff Shaw, which could prove 38 of the first 52 theorems in Principia, including some proofs considered more elegant than Russell’s original proofs by hand.
And this is the real problem – if something’s been proved by a computer, is it necessarily going to be an elegant, concise proof or might it just be cold, hard logic? The panellists had differing views on this – mathematician and Fields medalist Alessio Figalli says that a proof is still a proof, but that he doesn’t necessarily find computer proofs beautiful.
On the other hand, computer scientist and Nevanlinna Prize winner Madhu Sudan is happy with computer proofs, and says that finding an elegant mathematically satisfying proof as well is a bonus, even if those two things aren’t always the same. When Bertrand Russell was presented with a computer version of his laborious long-hand proof, he was said to have responded with delight – a logical (pun intended) response for someone whose goal is to see beautiful mathematics exist in the world, regardless of how it’s created.
So if computers can prove our results for us now, do we even need mathematicians any more? Of course we do. There are limitations on the kinds of results that can be proved this way, and a lot of work goes into specifying the problem and setting up the computer proving tools. Plus, who would drink all the coffee?
Alessio Figalli sees another benefit to going the long way round: “It’s good that there is no shortcut,” he says, explaining how working through a problem yourself rather than relying on a computer to solve it helps you to learn, and that if all mathematicians just fed their questions into a machine we might lose sight of the bigger picture. “The purpose of a proof is understanding,” added Efim Zelmanov.