Век информатики вносит свои коррективы и в представления о доказательствах. Возникают, например, случаи, когда доказательство требует перебора столь большого числа вариантов, что этот перебор делается недоступным человеку, а машине доступен. Допустим, машина перебрала все требуемые варианты и перебор привёл к нужным результатам. Можем ли мы считать, что получили доказательство? А что если машина дала так называемый сбой? (Но ведь и человек может ошибаться!) Кроме того, необходима гарантия, что сама программа (работы машины) составлена правильно; правильность программы требует особого доказательства, и теория таких доказательств образует специальный раздел теоретического программирования.

Реально компьютер был привлечён для решения проблемы четырёх красок. По простоте формулировки эта проблема, состоящая в доказательстве гипотезы четырёх красок, мало уступает проблеме Ферма (состоящей в доказательстве гипотезы Ферма), а по естественности постановки (и прикладному значению) её превосходит. Вот формулировка этой гипотезы в Большой Советской Энциклопедии (изд. 3-е, том 29, статья «Четырёх красок задача»): Четырёх различных красок достаточно для того, чтобы раскрасить любую карту так, чтобы никакие две области, имеющие общий участок границы, не были окрашены в один и тот же цвет. Проблема четырёх красок возникла в картографической среде: впервые наблюдение о достаточности четырёх красок было сделано в 1852 г. при составлении карты графств Англии. Обнаружилось, что гипотеза четырёх красок подтверждается во всех известных частных случаях. Сравнительно просто удаётся доказать (и это было сделано в 1890 г.), что для любой мыслимой карты достаточно пяти красок. Попытки же доказать аналогичное утверждение для четырёх красок долгое время (в течение ста лет) были безуспешны.

В 1976 г. Аппелем и Хакеном было анонсировано [17], а в 1977 г. изложено [18, 19] решение проблемы, основанное на сведéнии решения к большому числу частных случаев, рассмотрение которых можно поручить машине. Машина всё проверила, и таким образом было получено доказательство того, что всякую карту можно раскрасить четырьмя красками так, как нужно.

Казалось бы, проблема закрыта. Однако всё не так просто. Доказательство обладало двумя неприятными особенностями. Во-первых, рассуждения авторов были столь длинны и сложны, что никому не удавалось проверить их во всей полноте. Во-вторых, существенная часть доказательств состояла в использовании компьютера; именно компьютер, а не человек проверял, обладает ли каждая из почти двух тысяч специально отобранных карт некоторым требуемым качеством. Первая особенность была впоследствии устранена (если не полностью, то в очень большой степени) другими авторами, значительно упростившими первоначальные рассуждения Аппеля и Хакена. А вот избежать того, что в истинности большого числа фактов удостоверяется не человек, а компьютер, не удалось. А что если компьютер ошибся? Ведь такое иногда случается. Поэтому утверждение, что проблема четырёх красок решена, у многих вызывает сомнение.