Кеплер не использовал ни дедуктивное мышление или рассуждение, ни аксиоматический метод, ни стратегии математических доказательств для вывода своих трех законов движения планет. Он просто всматривался в сотни страниц данных Браге о планетах и считал, считал, считал…
Примерно в то же время свою теорию логарифмов разрабатывал Джон Непер (1550–1617). Это замечательный инструмент вычислений, он мог бы резко упростить задачу Кеплера. Но тот не мог понять смысла логарифмов и отказался от них. Он не шел простым путем. Только вообразите себе, что мог бы сделать Кеплер, будь у него компьютер! Правда, он мог бы и от компьютера отказаться просто оттого, что не понял принципа работы процессора.
Мы говорим здесь о Кеплере и Непере потому, что эта история предвосхитила современные споры об использовании компьютеров в математике. Одни утверждают, что компьютер позволяет нам видеть (вычислительно и визуально) вещи, которых мы раньше не могли представить. А другие считают, что все эти вычисления, конечно, очень хороши и полезны, но не составляют математического доказательства. Похоже, что первые смогут снабдить вторых информацией, и так возникнет симбиоз, приводящий к серьезным результатам. Мы обсудим эти соображения в книге.
Давайте вернемся к изменениям, которые произошли в математике за последние тридцать лет и были отчасти обусловлены пришествием высокоскоростных компьютеров. Вот матрикул некоторых компонентов этого процесса.
• В 1974 г. Аппель и Хакен [APH1] объявили, что задача о четырех красках решена. Иначе говоря, получен ответ на вопрос о том, сколько нужно красок, чтобы раскрасить любую карту так, что соседние страны получаются разных цветов. Построенное доказательство потребовало 1200 часов работы суперкомпьютера в университете Иллинойса. Математическое общество было в замешательстве, ведь такое «доказательство» никто не мог изучить или проверить. Или хотя бы понять. До сих пор не существует доказательства теоремы о четырех красках, которое может быть изучено и проверено человеком.
• Со временем люди все более и более свыклись с использованием компьютеров в доказательствах. В первые дни своего существования теория вейвлетов (к примеру) зависела от оценок некоторых постоянных, а их можно было получить только с помощью компьютера. Оригинальное доказательство де Бранжа гипотезы Бибербаха [DEB2] опиралось на результат теории специальных функций, который тоже можно было проверить только на компьютере (позднее обнаружилось, что это результат Аски и Гаспера, который доказан традиционно).
• Развитие новых обучающих средств, таких как программное обеспечение The Geometer’s Sketchpad, многих, включая Филдсовского медалиста Уильяма Тёрстона, навело на мысль, что традиционные доказательства могут уступить дорогу экспериментированию, т. е. проверке тысяч или миллионов частных случаев на компьютере.
Так что приход компьютеров действительно изменил наш взгляд на то, что можно считать доказательством. Ведь смысл в том, чтобы убедить другого человека в том, что какое-то утверждение истинно. Очевидно, есть много разных способов сделать это.
Еще интереснее, возможно, некоторые новые социальные тренды в математике, приводящие к построению нестандартных доказательств (мы подробно обсудим их позднее).
• Одним из грандиозных предприятий математики XX в. стала классификация конечных простых групп. Даниэль Горенштейн из Ратгерского университета дирижировал этим процессом. Сейчас считается, что эта задача решена. Замечательно здесь то, что одна теорема потребовала усилий многих сотен ученых. «Доказательство» здесь — собрание сотен статей и работ, охватывающих период более 150 лет. Сейчас оно включает более 10000 страниц, и его до сих пор подчищают и упорядочивают. Окончательная «запись доказательства» займет несколько томов, и нет никакой уверенности в том, что работающие сейчас эксперты проживут достаточно долго, чтобы увидеть результат своих усилий.
• Решение Томаса Хейлса задачи Кеплера об упаковке сфер во многом (как и решение задачи о четырех красках) опирается на компьютерные вычисления. Особенно интересно, что его доказательство вытеснило более раннее доказательство Ву Йи Хсианга, опирающееся на сферическую тригонометрию, а не на компьютерные вычисления. Хейлс допускает, что его «доказательство» нельзя проверить традиционным путем. Он организовал группу FlySpeck энтузиастов со всего света, чтобы построить процедуру проверки своих компьютерных аргументов.