Апология математики (сборник статей)

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

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

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

Сами Аппель и Хакен высказывают такие мысли по поводу своего доказательства: «При доказательстве было осуществлено беспрецедентное применение компьютеров. Дело в том, что используемые в доказательстве вычисления делают его более длинным, чем традиционно считается допустимым. На самом деле правильность предложенного доказательства вообще не может быть проверена без помощи компьютера. Более того, некоторые из решающих идей доказательства материализовались посредством компьютерных экспериментов. Не исключено, конечно, что в один прекрасный день появится короткое доказательство теоремы о четырёх красках… Вместе с тем не исключено, что такое короткое доказательство вообще невозможно. В этом последнем случае возникает новый и интересный тип теорем, для которых не существует доказательств традиционного типа» [20].