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

Вряд ли что-то может сильнее утвердить нас в результате, чем другое независимое доказательство. Пол Сеймур и его группа в Принстонском университете нашли другую дорогу для атаки на задачу (см. [RSST] и [SEY]). И не так давно (2004 г.) Гонтье использовал компьютерного «математического помощника» для проверки доказательства, построенного в 1996 г.[78]  Новое доказательство Сеймуа и др. тоже вовсю опирается на мощь компьютера, но в наши дни компьютеры гораздо быстрее и мощнее, чем во времена Аппеля и Хакена; да и сам алгоритм Сеймура кажется значительно более устойчивым, чем старый алгоритм начала 1970-х. В недавней статье [CAH] предлагается подход к задаче о четырех красках, который не опирается на компьютерные мощности.

Но все еще никто не может проверить доказательство Сеймура в традиционном смысле: «проверить человеком». Компьютеры по-прежнему выполняют миллионы операций, и не в человеческих силах сделать столько же вручную, да, по правде говоря, никому и не хочется. В сухом остатке мы имеем вот что: на протяжении последних двадцати лет, с момента появления оригинального доказательства Аппеля—Хакена и до решения Сеймура, мы как ученое сообщество стали более терпимо относиться к компьютерным доказательствам. Конечно же, все еще остаются сомнения и беспокойство, но все же эта новая методика входит в обиход. Компьютерных доказательств вокруг уже много (некоторые мы еще обсудим в этой книге), так что большая часть математического сообщества принимает их или по крайней мере относится к ним толерантно[79].

На самом-то деле математикам по-прежнему больше всего привычно и удобно традиционное, самодостаточное доказательство, которое состоит из точной последовательности шагов, записанной на бумаге. Мы все еще надеемся, что однажды такое доказательство появится и для задачи о четырех красках. Именно традиционное, в духе Евклида, доказательство дает нам понимание, озарение и чувство завершенности, к которому стремится каждый настоящий ученый. А пока мы живем с компьютерным доказательством теоремы о четырех красках.

Спустя тридцать лет к доказательству Аппеля—Хакена этой теоремы легко относиться по-философски. Как и в отношении доказательства Хэйлса гипотезы Кеплера (его мы тоже обсуждаем в этой книге), беспокоит лишь то, что в этих доказательствах недостает чувства завершенности, которое мы обычно ассоциируем с математическим доказательством. Обычно мы посвящаем несколько часов (или несколько дней или даже недель) поглощению и усваиванию математического доказательства. В таком процессе наша цель — узнать что-то новое[80]. Конечный результат — новое понимание и ясное ощущение того, что нечто выполнено и стало своим. А от этих новомодных компьютерных доказательство ничего такого не дождешься. Точно так же доказательство Григорием Перельманом гипотезы Пуанкаре и классификация конечных простых групп тоже не дают чувства завершенности. А ведь в этих двух случаях компьютеры не играют роли. На сцену выступают сложности с социологией профессии и предмета. Эти доказательства мы тоже обсудим на страницах этой книги.

К настоящему расколу, говорит Роберт Штрихартц [STR], приводят стремление к знанию и стремление к уверенности. Традиционно математики гордятся несокрушимым абсолютом своих результатов. В этом ценность нашего подхода к доказательству, установленного еще Евклидом. Но сейчас есть столько новых достижений, подрывающих старую систему ценностей. И к тому же столько новых потребностей общества: теоретическая вычислительная и инженерная математика и даже современная прикладная математика требуют определенной информации и идентифицируемых методов. Нужда в рабочем инструменте часто бывает намного сильнее нужды быть уверенным, что инструмент выдержит проверку строгими правилами логики. В результате может оказаться, что нам придется пересмотреть основания нашей науки. Практика математики в 2100 г. может весьма отличаться от современной.

Дорон Зельбергер — остроумный и уважаемый математик — поставил следующий вопрос. Допустим, некто заявляет: «Вот доказательство гипотезы Гольдбаха (мы обсуждаем ее в этой книге); оно истинно с 99-процентной степенью уверенности. Если мне выделят грант на $10 млрд, я построю доказательство, верное на все 100 процентов». И что в таком случае делать?

Никто — даже Билл Гейтс — не заплатит $10 млрд за окончательное решение гипотезы Гольдбаха. Она просто того не стоит. Что же, нам придется научиться жить с 99-процентным доказательством? Или мы будем считать задачу нерешенной? На такие вопросы до сих пор нет ясного ответа.

Глава 7. Доказательства, построенные компьютером

Автоматическое доказательство теорем все еще остается примитивным искусством, годным только на самые рудиментарные аргументы.

— Артур Джаффе