Светлый фон
Комментарий. сводимой неизбежным

Что же касается авторов обсуждаемого доказательства, то они отдавали себе отчёт в сложности его восприятия. В статье [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 были случайно обнаружены спустя полгода после начала его коммерческих продаж – кстати, математиком, специалистом по теории чисел). По-видимому, единственный способ проверки компьютерных результатов – написать другую программу и для другого типа компьютера. Это, конечно, совсем не похоже на стандартный идеал дедуктивных рассуждений, но именно так осуществляется проверка утверждений во всех экспериментальных науках. Из которых математика, стало быть, исключена напрасно.