Искусственный интеллект - [101]

Вначале К. Аппелем и В. Хакеном было найдено множество сводимых конфигураций, «размер кольца которых был достаточно мал, чтобы машинное время на доказательство сводимости было в пределах разумного» [10, р. 115]. Это позволило к концу 1972 года составить машинную программу для выполнения специального типа разряжающей процедуры. Прогонки этой программы позволили ее модифицировать при сохранении основной структуры. Это позволило на основе новой разряжающей процедуры построить множество сводимых конфигураций, в результате чего в конце 1976 года ТЧК была доказана (на что потребовалось 1200 часов машинного времени трех ЭВМ).

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

Многие математики исходят из того, что доказательство должно обладать такими характеристиками, как убедительность, обозримость и формальность. Убедительность доказательства - это свидетельство понимания математики как человеческой деятельности. Обозримость - свидетельство возможности проверить (обозреть) его во всей полноте человеком, т.е. обозримость конкретизирует убедительность, связывая процесс доказательства с его субъектом. Традиционно источником убедительности доказательства считается ясность, т.е. возможность проверить его квалифицированным математиком без использования ЭВМ, хотя некоторые доказательства могут быть весьма длинными, и потребовать много сил и времени. Формальность доказательства означает представимость его в виде конечной последовательности формальной теории, удовлетворяющей некоторым условиям, т.е. это вывод заключения из аксиом теории с помощью правил логики. Формализованное^ доказательства, в свою очередь, конкретизирует обозримость, разбивая ее на конечные обозримые модели.

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

Таким образом, не существует системы, в которой любое доказательство может быть формализовано, поэтому формализованность называют локальной характеристикой доказательств, а не глобальной. Но, как было показано Р. Томом, для любого доказательства существует некоторая подходящая формальная система, в которой оно может быть формализовано [11]. Однако все ли формализованные системы обозримы? Существуют формализованные доказательства, которые не могут быть обозримы вследствие ограниченности человеческой жизни. Поэтому возможны формализованные утверждения без обозримого доказательства. На практике же математики обычно приходят к знанию формального доказательства через посредство обозримых доказательств. Убедительность и обозримость могут быть связаны как сопряжения целого и части. Если убедительность - это в известной мере осуществимость доказательства как целого, завершенного, но в котором особо выделены исходный и заключающий его пункты, то обозримость - это осуществимость доказательства в каждом пункте сцепления доказательства. Формализованность же - упрощающая процедура, делающая доказательство более лаконичным и универсально выраженным, а также делающая его доступным для задания ЭВМ.

В какой же мере указанные характеристики применимы к доказательству ТЧК с помощью ЭВМ? Прежде всего, является ли оно убедительным? К. Аппель и В. Хакен подметили любопытную особенность, заключающуюся в том, что признание убедительности доказательства ТЧК с помощью ЭВМ зависит от характера полученного математического образования: математики, получившие образование до появления ЭВМ, к признанию убедительности данного доказательства относятся, как правило, оппозиционно [10].

Является ли доказательство ТЧК обозримым? Отрицание возможности обозримости основывается на том, что ни один математик не в состоянии проверить его шаг за шагом. По мнению некоторых исследователей, доказательство ТЧК может быть признано обозримым лишь в том случае, если применение ЭВМ считать новым методом доказательства. Но тогда само понятие доказательства должно измениться [11]. Отсюда делается вывод, что обозримость сохраняется за традиционным доказательством, но не доказательством с помощью ЭВМ.