Компьютер в доказательстве

Проблема четырёх красок - первая серьёзная математическая теорема, доказательство которой и проверка доказательства были выполнены с помощью компьютера.