Статья 367

Ньоэлла, З. Саймона, Д. Шоу. С помощью программы заново доказаны теоремы одного из разделов математической логики - исчисления высказываний, содержащихся в книге Б. Рассела и А. Уайтхеда. В дальнейшем на ЭВМ с большим быстродействием удалось вывести все теоремы. Достижения неоспоримы, но ведь передоказаны уже доказанные теоремы. А существуют ли теоремы, впервые полученные при помощи ЭВМ. Да, существуют, и таких примеров довольно много. Один из самых известных - решение знаменитой проблемы четырех красок.
Немногим более десяти лет назад было опубликовано сообщение о том, что так называемая проблема четырех красок была успешно решена К. Аппелем и В. Хакеном. Проблема заключается в следующем допускает ли каждая карта такую раскраску, что любая страна на этой карте будет иметь один из четырех цветов и никакие две страны, имеющие общую границу, не будут окрашены одинаково.