Durante dois mil anos, uma prova matemática foi um texto escrito para ser lido por pessoas. Ela podia pular passos “evidentes”, apoiar-se num desenho, usar convenções da comunidade. O leitor completava o resto. Nos últimos cinquenta anos, apareceu um leitor que não completa nada: o computador. As quatro cores Quantas cores bastam para pintar qualquer mapa de modo que países vizinhos tenham cores diferentes? A resposta, quatro, foi conjecturada em 1852 e resistiu mais de um século. Em 1976, Kenneth Appel e Wolfgang Haken, da Universidade de Illinois, a demonstraram reduzindo o problema a quase dois mil casos que um computador verificou um por um, em mais de mil horas de máquina.