For two thousand years, a mathematical proof was a text written to be read by people. It could skip “obvious” steps, lean on a drawing, use the conventions of the community. The reader filled in the rest. In the last fifty years a reader has appeared that fills in nothing: the computer. The four colours How many colours are enough to colour any map so that neighbouring countries have different colours? The answer, four, was conjectured in 1852 and resisted for over a century. In 1976 Kenneth Appel and Wolfgang Haken, of the University of Illinois, proved it by reducing the problem to almost two thousand cases that a computer checked one by one, in more than a thousand hours of machine time.