 The past decades have witnessed the first occurrences of mathematical proofs in which computers appear to play an essential role. The four-colour theorem is one example. It says that for every map, only four colours are needed to colour countries in such a way that no two countries that have a common border receive the same color. This theorem was proved in 1976 (Appel et al. 1977). But the proof distinguishes many cases which were verified by a computer. These computer verifications are too long to be double-checked by humans. The proof of the four colour theorem gave rise to a debate about the question to what extent computer-assisted proofs count as proofs in the true sense of the word.