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

Размышляя о роли компьютеров в математике, уместно напомнить известную историю. Тихо Браге (1546–1601) был одним из величайших астрономов Возрождения. Он разработал научную процедуру, которая позволила ему создать обширную базу данных о движении планет. Его даровитый ученик Иоганн Кеплер (1571–1630) страстно желал получить доступ к этим данным, поскольку у него были идеи о том, как сформулировать математические законы, описывающие движение планет. И Браге, и Кеплер были целеустремленными людьми, однако их взгляды на очень многие вещи разнились. Браге опасался, что Кеплер воспользуется данными, чтобы подтвердить теорию Коперника о Солнечной системе (а именно, что в центре системы находится вовсе не Земля, а Солнце, — это представление противоречило христианской догме). Пока Браге был жив, Кеплер так и не получил доступа к его расчетам.

Однако в эту историю странным образом вмешалось провидение. Спонсор Тихо Браге передал ему остров, где тот построил обсерваторию и работал в ней. Поэтому Браге приходилось выполнять некоторые социальные обязанности — выказывать свою признательность и сообщать о достижениях. На одном приеме Браге выпил так много пива, что его мочевой пузырь лопнул, и он умер. Кеплер вступил с семьей Браге в торг за данные, которые ему были так нужны. Течение научной истории изменилось навсегда.

Кеплер не использовал ни дедуктивное мышление или рассуждение, ни аксиоматический метод, ни стратегии математических доказательств для вывода своих трех законов движения планет. Он просто всматривался в сотни страниц данных Браге о планетах и считал, считал, считал…

Примерно в то же время свою теорию логарифмов разрабатывал Джон Непер (1550–1617). Это замечательный инструмент вычислений, он мог бы резко упростить задачу Кеплера. Но тот не мог понять смысла логарифмов и отказался от них. Он не шел простым путем. Только вообразите себе, что мог бы сделать Кеплер, будь у него компьютер! Правда, он мог бы и от компьютера отказаться просто оттого, что не понял принципа работы процессора.

Мы говорим здесь о Кеплере и Непере потому, что эта история предвосхитила современные споры об использовании компьютеров в математике. Одни утверждают, что компьютер позволяет нам видеть (вычислительно и визуально) вещи, которых мы раньше не могли представить. А другие считают, что все эти вычисления, конечно, очень хороши и полезны, но не составляют математического доказательства. Похоже, что первые смогут снабдить вторых информацией, и так возникнет симбиоз, приводящий к серьезным результатам. Мы обсудим эти соображения в книге.

Давайте вернемся к изменениям, которые произошли в математике за последние тридцать лет и были отчасти обусловлены пришествием высокоскоростных компьютеров. Вот матрикул некоторых компонентов этого процесса.

• В 1974 г. Аппель и Хакен [APH1] объявили, что задача о четырех красках решена. Иначе говоря, получен ответ на вопрос о том, сколько нужно красок, чтобы раскрасить любую карту так, что соседние страны получаются разных цветов. Построенное доказательство потребовало 1200 часов работы суперкомпьютера в университете Иллинойса. Математическое общество было в замешательстве, ведь такое «доказательство» никто не мог изучить или проверить. Или хотя бы понять. До сих пор не существует доказательства теоремы о четырех красках, которое может быть изучено и проверено человеком.

• Со временем люди все более и более свыклись с использованием компьютеров в доказательствах. В первые дни своего существования теория вейвлетов (к примеру) зависела от оценок некоторых постоянных, а их можно было получить только с помощью компьютера. Оригинальное доказательство де Бранжа гипотезы Бибербаха [DEB2] опиралось на результат теории специальных функций, который тоже можно было проверить только на компьютере (позднее обнаружилось, что это результат Аски и Гаспера, который доказан традиционно).

• Развитие новых обучающих средств, таких как программное обеспечение The Geometer’s Sketchpad, многих, включая Филдсовского медалиста Уильяма Тёрстона, навело на мысль, что традиционные доказательства могут уступить дорогу экспериментированию, т. е. проверке тысяч или миллионов частных случаев на компьютере.

Так что приход компьютеров действительно изменил наш взгляд на то, что можно считать доказательством. Ведь смысл в том, чтобы убедить другого человека в том, что какое-то утверждение истинно. Очевидно, есть много разных способов сделать это.

Еще интереснее, возможно, некоторые новые социальные тренды в математике, приводящие к построению нестандартных доказательств (мы подробно обсудим их позднее).