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

Естественно — даже для профессиональных математиков — впасть в ловушку мышления: «Раз уж компьютер говорит, что это верно, значит, это верно». Мы встречаем студентов, которые так относятся к своим калькуляторам. Когда мы пытаемся ввести работу на компьютере на уроки математики в школе, некоторые ученики получают горы мусора на выходе — и притом полагают, что все это разумные вещи, ведь их же вывела машина. Встречаются и ученые, которые вычисляют на компьютере бессмыслицу, а затем воображают, что это и есть математическое исследование. Это пример того, как некоторые путают обратное утверждение с контрапозицией (разд. 1.3). Если какое-либо утверждение истинно, то верно запрограммированный компьютер подтвердит его истинность. Однако, если машина утверждает, что что-то истинно, отсюда вовсе не следует истинность такого утверждения. Вовсе нет, и старая присказка IBM «мусор на входе — мусор на выходе» как нельзя более верна в таком контексте.

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

7.3 Доказательство теорем и проверка программ

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

Компьютерщики-теоретики имеют дело с точностью и надежностью своих программ. Здесь под «компьютерной программой» мы понимаем список команд, записанных компьютерным кодом, основанным на английском языке, которые компьютер должен выполнять. Некоторые компьютерные программы коротки: скажем, чтобы задать очень сложное множество Мандельброта, достаточно 20 строк кода. Некоторые программы головоломно сложны. Компьютерный код для Windows Vista превышает 100 миллионов строк. Компьютерные специалисты заботятся о формальной проверке программ, и это очень глубокий философский вопрос. Некоторые полагают, что компьютерные дисциплины должны больше напоминать математику; проверка программы должна быть сродни доказательству теоремы. Именно так следует гарантировать надежность работы. Эту точку зрения можно углубить: лучше всего было бы, если проверка программ осуществлялась автоматически — без вмешательства человека, одним нажатием кнопки.

На самом деле это неосуществимо сегодня и вряд ли будет осуществимо в будущем. Формальную проверку проводит человек, который сидит и проверяет логику компьютерной программы — просто размышляя. Это утомительная напряженная работа. От нее не получают удовольствия, и мало кто ее ценит. Математик, открывший новое доказательство новой теоремы, старается поделиться им с коллегами, прочитать о нем лекцию, записать и опубликовать его. И наоборот, никто не «делится» проверкой компьютерной программы, никто не читает об этом лекции и не публикует результатов.

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

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

Проверка — не послание, она не служит предметом коммуникации, у нее нет содержания. Нет и не будет социологической структуры, которая поддержит создание и приятие проверки. Ее результатам или верят или нет. Проверку нельзя принять, обобщить, использовать где-то еще, найти ее связь с другими дисциплинами или присвоить сообществом ученых. Формальная проверка программ не вызревает в нас, как доказательство. Она просто слепое орудие.