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

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

Комментарий. Остановимся на ситуации с доказательством Аппеля и Хакена чуть подробнее. Основная идея этих авторов связана со следующими представлениями. Прежде всего авторы переходят от раскраски областей карты к раскраске вершин плоского графа, причём такого, который представляет собою триангуляцию. Далее они называют конфигурацией любой подграф, образованный циклом и внутренностью этого цикла. Конфигурация называется сводимой, если некоторыми стандартными методами можно доказать, что она не может быть вложена в минимальный контрпример к гипотезе четырёх красок. Множество конфигураций называется неизбежным, если каждая плоская триангуляция содержит как подграф одну из конфигураций множества. Из определений немедленно следует, что для решения (положительного) проблемы четырёх красок достаточно предъявить неизбежное множество сводимых конфигураций. Авторы предъявляют в явном виде 1834 сводимые конфигурации, образующие неизбежное множество [19, с. 505–567]. Длина цикла в каждой из этих конфигураций – 14 или менее того. И для поиска неизбежного множества, и для доказательства сводимости его членов использовался компьютер. Однако если в первом случае (построение множества) компьютер выполнял вспомогательные функции, поскольку само доказательство неизбежности найденного (теперь уже не важно, каким способом) множества не опирается на машинные вычисления, то во втором случае (проверка сводимости) использование компьютера являлось существенным компонентом доказательства, и на каждую конфигурацию ушло примерно 10 минут машинного времени такой проверки. Оценивая доказательство Аппеля и Хакена, авторы обзора [24] указывают, что для доказательства понадобилось четыре года и 1200 часов машинного времени и что текст его занимает 139 страниц, в том числе 99 страниц рисунков, в среднем более 30 рисунков на страницу. Они отмечают также, что «существенно переборный характер доказательства затрудняет его проверку (по оценке Аппеля, проверка всех деталей требует 300 часов машинного времени)». Названные 300 часов относятся, по-видимому, к проверке сводимости. Однако, как мы уже отмечали, сомнения вызывает как раз немашинная часть – проверка неизбежности предъявленного множества конфигураций. Дело в том, что непосредственно в тексте статей [18] и [19] эта проверка исчерпывающим образом не проводится. В статье [18, с. 460], в подстрочном примечании, сообщено, что детали доказательства неизбежности предъявленного множества (более точно, детали доказательства лежащей в основе этой неизбежности так называемой теоремы о разрежении) содержатся на микрофишах[167], образующих специальное приложение к журналу. Автор этих строк, изучавший журнал в библиотеке, указанного приложения, однако, не обнаружил.

Что же касается авторов обсуждаемого доказательства, то они отдавали себе отчёт в сложности его восприятия. В статье [33, с. 852] приводится следующая цитата из неназванной статьи Аппеля и Хакена 1986 г. (перевод даётся по статье [34, с. 95]):

Читатель должен разобраться в 50 страницах текста и диаграмм, 85 страницах с почти 2500 дополнительными диаграммами, 400 страницах микрофишей, содержащих ещё диаграммы, а также тысячи отдельных проверок утверждений, сделанных в 24 леммах основного текста. Вдобавок читатель узнаёт, что проверка некоторых фактов потребовала 1200 часов компьютерного времени, а при проверке вручную потребовалось бы гораздо больше. Статьи устрашающи по стилю и длине, и немногие математики прочли их сколько-нибудь подробно.

Доказательство Аппеля и Хакена продолжало вызывать сомнения до конца XX в. Вот что пишет Робин Томас, автор упомянутой статьи [33]:

[…] Трудности с доказательством Аппеля и Хакена можно уложить в два пункта:

1. Часть доказательства основана на использовании компьютера и не может быть проверена вручную;

2. Даже та часть, для которой ручная проверка предполагается возможной, не подвергалась, насколько мне известно, независимой проверке.

Далее Р. Томас указывает, что он и трое его коллег (N. Robertson, D. P. Sanders, P. Seymour) пытались проверить доказательство Аппеля и Хакена, но вскоре сдались и поняли, что разумнее разработать собственное доказательство. Что они и сделали. Доказательство четырёх авторов следует основным идеям Аппеля и Хакена и не устраняет трудности (1), но в значительной мере ликвидирует трудность (2), будучи гораздо более проверяемым в своей некомпьютерной части. Тем не менее и это новое доказательство вызывает скептицизм. Вот что пишет о нём А. В. Самохин, завершая свою статью [34]:

Компьютерная часть всё ещё остаётся скорее предметом веры. Ведь даже проверка распечаток всех программ и всех входных данных не может гарантировать от случайных сбоев или даже от скрытых пороков электроники (вспомним, что ошибки при выполнении деления у первой версии процессора Pentium были случайно обнаружены спустя полгода после начала его коммерческих продаж – кстати, математиком, специалистом по теории чисел). По-видимому, единственный способ проверки компьютерных результатов – написать другую программу и для другого типа компьютера. Это, конечно, совсем не похоже на стандартный идеал дедуктивных рассуждений, но именно так осуществляется проверка утверждений во всех экспериментальных науках. Из которых математика, стало быть, исключена напрасно.

Создаётся впечатление, что с развитием математики (и появлением всё более и более сложных и длинных доказательств) доказательства теряют своё главное свойство – свойство убедительности. Непонятно, что же тогда остаётся от доказательства, ведь убедительность является их свойством по определению. Кроме того, с усложнением доказательства возрастает элемент его субъективности. Конечно, формальное доказательство объективно. Но, во-первых, формальными доказательствами обладают не сами суждения, а их выражения, записи в формализованных языках. Во-вторых, проверка утверждения, что данный текст является формальным доказательством, хотя и осуществляется алгоритмически, может при объёмистом тексте вызвать значительные практические трудности.

Большие доказательства начинают жить по каким-то своим макроскопическим законам. При чрезмерном возрастании объёма доказательства расплывается само представление о доказательстве, подобно тому как в «большом» расплывается понятие о натуральном числе (ещё раз отсылаем читателя к статье П. К. Рашевского [16]).

Получается, что, хотя все доказательства должны по определению быть убедительными, одни из них убедительнее других, т. е. как бы являются доказательствами в большей степени, чем другие. Возникает нечто вроде градации доказательств по степени доказательности – явление, которое, конечно, в корне противоречит первоначальным представлениям об одинаковой непреложности всех доказательств.