Исторически в математике бытовало два очень разных понятия доказательства.
Первое состоит в том, что доказательство — это то, что внушает аудитории (или, по крайней мере, самому доказывающему!) интуитивное ощущение уверенности в том, что результат верен. С этой позиции доказательство — это внутреннее трансформирующее переживание, способ, при помощи которого ваша душа входит в контакт с вечными истинами Платоновых небес.
Второе понятие состоит в том, что доказательство — это всего лишь последовательность символов, подчиняющихся определенным правилам, — или, в более общем плане, если мы хотим довести эту концепцию до ее, на мой взгляд, логического завершения, доказательство есть вычисление. Иными словами, доказательство это физический, механический процесс, такой что если он завершается с определенным результатом, то вам следует признать данную теорему верной. Естественно, вы не можете испытывать большую уверенность в истинности теоремы, чем ваша уверенность в законах, которые управляют работой машины. Но, как хорошо понимали великие логики от Лейбница до Фреге и Гёделя, слабость этой концепции доказательства является одновременно ее силой. Если доказательство представляет собой чисто механический процесс, то в принципе вы можете открывать новые математические истины просто поворотом рубильника, без какого-либо понимания или озарения. (Как, по представлению Лейбница, будут когда-нибудь разрешаться юридические споры: «Джентльмены, давайте посчитаем!»)
Противоречия между двумя концепциями доказательства обострились в 1976 г., когда Кеннет Аппель и Вольфганг Хакен анонсировали доказательство знаменитой теоремы о четырех красках, которая гласит, что любую плоскую карту можно раскрасить при помощи четырех красок так, чтобы никакие две соседние области не оказались окрашены в один цвет. Доказательство, в сущности, состояло из тупого перебора нескольких тысяч случаев, сделанного компьютером; ни один человек не в состоянии охватить это доказательство во всей полноте.
Если теорема о четырех красках была доказана, по существу, методом грубой силы, то как можно быть уверенным, что оно охватило все без исключения возможности? Новый технический вклад, который пришлось здесь внести математикам-людям, состоял именно в том, чтобы свести задачу к конечному числу случаев, точнее, примерно к 2000 вариантов, — которые затем можно было проверить при помощи компьютера. Тот факт, что с тех пор доказательство было проделано еще раз другой группой ученых, которым удалось снизить число случаев с примерно 2000 до примерно 1000, естественно, повышает нашу уверенность в нем.
Далее, люди могут спросить: откуда вы знаете, что компьютер не совершил ошибки? Очевидный ответ: математики-люди тоже совершают ошибки. Я имею в виду, что Роджер Пенроуз любит говорить о непосредственном контакте с Платоновой реальностью, но, откровенно говоря, ситуация, когда ты уверен, что наладил такой контакт, а на следующее утро все твои рассуждения оказываются ошибочными, выбивает из колеи!
Мы знаем, что компьютер не наделал ошибок, потому что мы доверяем законам физики, которые управляют его работой, и верим, что во время расчетов в него не попала какая-нибудь тяжелая космическая частица. Но последние 20 лет вопрос стоит так: а почему мы должны доверять физике? Мы ежедневно доверяем ей в ситуациях, когда речь идет о жизни и смерти, но должны ли мы доверять ей в таком важном деле, как доказательство теоремы о четырех красках? По правде говоря, с определением понятия «доказательство» можно играть в игры сколько угодно, расширяя его до чудовищного уровня, и оставшуюся часть главы мы будем заниматься именно этим.