Изменчивая природа математического доказательства. Доказать нельзя поверить

В 1880 г. математик П. Тайт предложил другое решение задачи о четырех красках. Изъян в нем обнаружил Дж. Петерсен, это случилось в 1891 г. И опять для выявления ошибки потребовалось 11 лет!

История задачи о четырех красках пространна и любопытна. Великий американский математик Дж. Биркгофф разбирался в основах этой задачи, и это позволило Филиппу Франклину (1898–1965) в 1922 г. доказать, что гипотеза о четырех красках верна для карт, изображающих не более 25 стран. Немецкий математик Г. Хисч смог значительно продвинуться в решении, введя методы приведения и удаления краски, которыми и воспользовались Аппель и Хакен в 1977 г. Уолтер Стромквист в 1975 г. защитил докторскую диссертацию [STR1] в Гарварде. Он доказал, что четырех красок достаточно для любой карты, на которой не более 100 стран (см. [STR2]). Особенно впечатляет, что в 1970 г. Рингель и Янгс смогли доказать, что оценки Хивуда для хроматического числа произвольной поверхности точны. Так что хроматическое число тора действительно равно 7. Хроматическое число «супертора» с двумя дырками равно 8. И так далее. Но доказательство Рингеля-Янгса неприменимо к сфере. Они не смогли улучшить результат Хивуда: для раскраски сферы всегда достаточно пяти цветов.

И вот в 1974 г. случился прорыв. Заняв 1200 часов работы суперкомпьютера университета в Иллинойсе, Кеннет Аппель и Вольфганг Хакен показали, что для раскраски любой карты на сфере достаточно четырех цветов. Их метод заключался в том, чтобы выделить 633 основных конфигураций карт (все остальные к ним сводятся) и доказать, что каждая из этих конфигураций сводима в смысле, предложенном Хисчем. Однако число основных конфигураций оказалось очень велико, а число требующихся операций приведения превышает все мыслимые человеческие способности к счету. Логика построений была крайне запутана и сложна. На сцену вышел компьютер.

В те времена машинное время было дорого и не вполне доступно, так что Аппель и Хакен не могли получить для себя цельный кусок в 1200 часов непрерывной работы компьютера. Вычисления проводились по ночам, вне расписания, если выдавались свободные окошки. Более того, Аппель и Хакен не были уверены, что вычисления когда-либо будут закончены. Они решили так:

• если компьютер закончит работу, то он проверит все случаи и задача о четырех красках будет решена;

• если компьютер не закончит работу, то никакого вывода будет сделать нельзя.

Что ж, работа компьютера завершилась. А споры, сплетни и раздрай в математическом сообществе — нет[77]. Разве это доказательство? Компьютер проделал десятки миллионов операций, и никому не под силу проверить их все. К 1974 г. наше понимание того, что такое доказательство, было сформировано двумя тысячами лет развития: доказательство — это цепочка шагов, которые один человек записывает на бумаге, а другой может их все проверить. Некоторые доказательства были длинными и сложными (например, в середине 1960-х гг. доказательство знаменитой теоремы об индексе Атьи—Зингера состояло из четырех больших статей в журнале «Анналы математики» и опиралось на огромное количество математических фактов из других источников). Однако их все и всегда мог проверить один человек или несколько. «Доказательство» Аппеля и Хакена было совсем другой природы. Оно требовало доверия к компьютеру и алгоритму, который компьютером выполнялся. У всех в ушах звучала старая песня IBM «мусор на входе — мусор на выходе».

Даже если принять идею компьютерного доказательства, все равно оставались поводы для беспокойства. Раз человек не может наверняка проверить вычисления компьютера, как можно быть уверенным, что компьютер не допустил ошибок? Как можно быть уверенным, что нет ошибок в коде, или в конструкции центрального процессора, или что в вычисления не вкрались квантово-механические ошибки? Ведь известно, что компьютерные ошибки приводили к чудовищным последствиям. Например, к взрыву ракеты Ариан-5 через 40 секунд после старта с Куру, французская Гвиана, в 1996 г. Сейчас известно, что взрыв произошел из-за ошибки в программном обеспечении. А именно выражающее горизонтальную составляющую скорости ракеты относительно платформы 64-битовое число с плавающей точкой конвертировалось в 16-битовое целое со знаком. Ракета и груз стоили $500 млн, а общие затраты на проект приближались к $7 млрд. К счастью, ракета была беспилотной. Хорошо известно, что в октябре 1994 г. баг в чипе компьютера Pentium FDIV из-за ошибки в округлении стал большой проблемой для многих владельцев компьютеров (включая автора этой книги). Баг был обнаружен Томасом Найсли из Линчбурга, он как раз разрабатывал программу перечисления простых чисел, троек и четверок простых чисел. Найсли выяснил — после объемистой переписки с Интел — что компании было известно о проблеме еще с мая 1994 г. После значительного давления со стороны общественности компания Интел отозвала чип и бесплатно заменила дефектные чипы на новые. Ошибка компании оценивается приблизительно в $500 млн.

Конечная математика