Доказательство теоремы о четырёх красках с помощью компьютера, предложенное Кеннетом Аппелем и Вольфгангом Хакеном в 1976 году, вызвало сомнения у математического сообщества из-за того, что его невозможно было проверить вручную. 24

Учёные не были готовы отдать логические рассуждения машине и считали, что доказательство должно быть понятным и проверяемым исключительно человеком. 3

Чтобы развеять оставшиеся сомнения, в 1997 году Робертсон, Сандерс, Сеймур и Томас опубликовали более простое доказательство, использующее аналогичные идеи, но по-прежнему проделанное с помощью компьютера. 24