in 1976, Kenneth Appel and Wolfgang Haken used a computer to prove the famous ‘four-colour conjecture’ (that using only four different colours, any map drawn in a plane can be coloured so that no two adjacent regions have the same colour). The program required hundreds of hours of computer time, which meant that the steps of the proof, if written down, could not have been read, let alone recognized as self-evident, by a human being in many lifetimes. ‘Should we take the computer’s word for it that the four-colour conjecture is proved?’, the sceptics wondered – though it had never occurred to
...more
