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

Комментарий. Остановимся на ситуации с доказательством Аппеля и Хакена чуть подробнее. Основная идея этих авторов связана со следующими представлениями. Прежде всего авторы переходят от раскраски областей карты к раскраске вершин плоского графа, причём такого, который представляет собою триангуляцию. Далее они называют конфигурацией любой подграф, образованный циклом и внутренностью этого цикла. Конфигурация называется сводимой, если некоторыми стандартными методами можно доказать, что она не может быть вложена в минимальный контрпример к гипотезе четырёх красок. Множество конфигураций называется неизбежным, если каждая плоская триангуляция содержит как подграф одну из конфигураций множества. Из определений немедленно следует, что для решения (положительного) проблемы четырёх красок достаточно предъявить неизбежное множество сводимых конфигураций. Авторы предъявляют в явном виде 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 часов компьютерного времени, а при проверке вручную потребовалось бы гораздо больше. Статьи устрашающи по стилю и длине, и немногие математики прочли их сколько-нибудь подробно.