Величайшие математические задачи

На всех этапах анализа были масштабно задействованы компьютеры. Хитрость здесь в том, чтобы для каждой локальной сети выбрать такое представление о мере, которое сделало бы вычисления сравнительно несложными. Геометрически замена плотности на меру выглядит как сооружение своеобразной крыши над гладким ландшафтом, максимум которого ищет исследователь. Крыша состоит из нескольких плоских участков (см. рис. 24). Работать с такими формами значительно легче, чем с гладкими поверхностями, поскольку максимумы располагаются в углах, для нахождения которых достаточно решить куда более простые уравнения. Для этого существуют эффективные методы, известные как линейное программирование. Если крыша построена так, что ее пик совпадает с пиком гладкой поверхности, то более простые расчеты, предназначенные для поисков пика крыши, позволят найти не только его, но и пик гладкой поверхности.

У всякого упрощения есть своя цена, и у этого тоже: чтобы найти пик крыши, приходится решать около 100 000 линейных задач. Впрочем, достаточно длинные расчеты, необходимые для этого, вполне по силам современным компьютерам. Когда Хейлс и Фергюсон подготовили свою работу к публикации, в ней оказалось около 250 страниц математического текста и 3 Гбайт компьютерных файлов.

В 1999 г. Хейлс подал подготовленное доказательство в Annals of Mathematics, и журнал специально для этого случая набрал жюри из 12 экспертов. К 2003 г. оно объявило, что «с уверенностью на 99 %» представленное доказательство верно. Оставшийся 1 % неуверенности касался компьютерных расчетов; многие из них жюри повторило, а также иными способами проверило стратегию и тактику доказательства, но некоторые его аспекты проверить не удалось. После значительной задержки журнал опубликовал работу. Хейлс признал, что такой подход к доказательству, вероятно, никогда не будет признан на 100 % корректным, и в 2003 г. объявил о старте проекта по переформатированию доказательства в такой вид, в котором его сможет проверить компьютер при помощи стандартных программ автоматической проверки доказательств.

Это может показаться чем-то вроде перехода из огня в полымя, но на самом деле все предельно понятно и логично. Доказательства, которые математики публикуют в журналах, призваны убеждать людей. Как я уже говорил в главе 1, доказательство — это своего рода рассказ. Компьютеры не сильны в литературе, зато прекрасно справляются с заданиями, которые нам не по зубам: они способны безошибочно выполнять длинные нудные расчеты. Компьютеры идеально сочетаются с формальным определением доказательства в университетских учебниках: серия логических шагов, каждый из которых вытекает из предыдущих.

Компьютерщики научились использовать эту способность. Чтобы проверить доказательство, заставьте компьютер проанализировать каждый логический шаг. Звучит просто, но на самом деле доказательства в журналах пишут не так. Эти рассказы оставляют за скобками все рутинное или очевидное… Все привыкли к традиционным фразам: «Несложно убедиться, что…», «Используя методы Чизбургера и Чипса, модифицированные так, чтобы учитывать изолированные сингулярности, видим, что…», «Несложный расчет показывает…». Компьютеры (пока) с подобными задачами не справляются. Но люди-то всегда могут переписать доказательство, заполнив все подобные пропуски, и тогда компьютер вполне может проверить каждый его шаг.

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

В последние годы таким образом были проверены доказательства многих ключевых математических теорем. Для этого их нередко требовалось перевести в другую форму, более подходящую для компьютерных манипуляций. Один из последних триумфов — проверка и подтверждение доказательства теоремы Жордана: всякая замкнутая кривая без самопересечений на плоскости делит плоскость на две связные области. Утверждение может показаться очевидным, но пионеры топологии долго не могли строго доказать его. В конце концов это удалось в 1887 г. Камилю Жордану, опубликовавшему доказательство на 80 страницах, но позже его нередко критиковали за необоснованные ограничения. Поэтому слава досталась Освальду Веблену, давшему в 1905 г. более подробное доказательство. Веблен заявил: «[Жорданово] доказательство… не удовлетворяет многих математиков. В нем теорема принимается без доказательства в существенном особом случае, когда речь идет о простом многоугольнике; что же касается дальнейшего изложения, то следует признать по крайней мере, что не все детали в нем приведены».