Великая Теорема Ферма

В июне 1976 года, затратив 1200 часов машинного времени, Хакен и Аппель заявили во всеуслышание, что им удалось проанализировать все 1482 карты и для раскрашивания ни одной из них не требуется более четырех красок. Проблема четырех красок Гатри была наконец решена. Следует особенно подчеркнуть, что решение проблемы четырех красок стало первым математическим доказательством, в котором роль компьютера не сводилась к ускорению вычислений, — компьютер привнес в решение проблемы нечто гораздо большее: его роль была столь значительной, что без компьютера получить доказательство было бы невозможно. Решение проблемы четырех красок с помощью компьютера было выдающимся достижением, но в то же время оно вызвало у математического сообщества чувство тревоги, так как проверка доказательства в традиционном смысле не представлялась возможной.

Прежде, чем опубликовать решение Хакена и Аппеля на страницах «Illinois Journal of Mathematics», редакторам было необходимо подвергнуть его тщательному рецензированию в каком-то не известном ранее смысле. Традиционное рецензирование было невозможно, поэтому было решено ввести программу Хакена и Аппеля в независимый компьютер с тем, чтобы убедиться, что результат останется тем же.

Такое нестандартное рецензирование привело в ярость некоторых математиков, утверждавших, будто компьютерная поверка неадекватна, так как не дает гарантии от внезапного отказа в недрах компьютера, который может стать причиной сбоя в логике. X.П.Ф. Суиннертон-Дайер высказал следующее замечание по поводу компьютерных доказательств: «Когда теорема доказана с помощью компьютера, невозможно изложить доказательство в соответствии с традиционным критерием — так, чтобы достаточно терпеливый читатель смог шаг за шагом повторить доказательство и убедиться в том, что оно верно. Даже если бы кто-нибудь взял на себя труд распечатать все программы и все данные, использованные в доказательстве, нельзя быть уверенным в абсолютно правильной работе компьютера. Кроме того, у любого современного компьютера по каким-то неясным причинам могут быть слабые места как в программном обеспечении, так и в электронном оборудовании, которые могут приводить к сбоям так редко, что остаются необнаруженными на протяжении нескольких лет, и поэтому в работе каждого компьютера могут быть незамеченные ошибки».

До какой-то степени поведение математического сообщества, предпочитавшего избегать компьютеров вместо того, чтобы их использовать, можно рассматривать как своего рода паранойю. Джозеф Келлер как-то заметил, что в его университете (Стэнфорде) математический факультет имел меньше компьютеров, чем любой другой факультет, в том числе факультет французской литературы. Те математики, которые отказались признать работу Хакена и Аппеля, не могли отрицать, что все математики соглашались принимать традиционные доказательства, даже если они сами не проверяли их. В случае доказательства Великой теоремы Ферма, представленного Уайлсом, менее 10 % специалистов по теории чисел полностью понимали его рассуждения, но все 100 % сочли, что доказательство правильное. Те, кто не смог до конца понять все тонкости доказательства, приняли его потому, что доказательство признали другие—те, кто все понял, шаг за шагом проследил весь ход доказательства и проверил каждую деталь.

Еще более ярким примером может служить так называемое доказательство классификации конечных простых групп, состоящее из 500 отдельных работ, написанных более чем сотней математиков. Говорят, что полностью разобрался в этом доказательстве (общим объемом в 15000 страниц) один-единственный человек на свете — скончавшийся в 1992 году Дэниэл Горенстейн. Тем не менее, математическое сообщество в целом могло быть спокойным: каждый фрагмент доказательства был изучен группой специалистов, и каждая строка из 15000 страниц была десятки раз проверена и перепроверена. Что же касается проблемы четырех красок, то с ней дело обстояло иначе: она никем не была и не будет полностью проверена.

За двадцать лет, прошедших с тех пор, как Хакен и Аппель сообщили о доказательстве теоремы о четырех красках, компьютеры неоднократно использовались для решения других, менее известных, но столь же важных проблем. В математике — области, не ведавшей ранее вмешательства столь современной технологии, как компьютеры, — все больше и больше специалистов неохотно осваивали использование кремниевой логики и разделяли мнение Вольфганга Хакена: «Всякий, в любом месте доказательства, может полностью вникнуть в детали и проверить их. То, что компьютер может за несколько часов «просмотреть» столько деталей, сколько человек не сможет просмотреть за всю свою жизнь, не меняет в принципе представление о математическом доказательстве. Меняется не теория, а практика математического доказательства».