Искусственный интеллект

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

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

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

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

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

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

Наконец, является ли доказательство ТЧК формализованным. Оно убедительно, формализовано, но необозримо. Существенное различие между доказательством ТЧК и традиционным заключается в том, что первое требует обращения к ЭВМ для заполнения бреши в доказательстве, которое в остальных отношениях традиционно [11]. Иными словами, доказательство ТЧК осуществлено на основаниях, часто являющихся эмпирическими. Поэтому применение ЭВМ в математике вводит эмпирические эксперименты в математику. Доказательство с помощью ЭВМ не является традиционным, т.е. это не априорный вывод утверждения из посылок, поскольку используются данные эксперимента. А это делает доказательство ТЧК первым доказательством a posteriori, что снова поднимает проблему отличия математики от естественных наук.

Таким образом, принятие тезиса о том, что положения теоретической математики могут быть установлены с помощью эмпирического доказательства, вводит, по мнению ряда авторов, в математику эмпирические методы, что имеет весьма серьезные последствия для философии математики, в частности влечет необходимость пересмотра или уточнения ряда положений, таких как: 1. все математические теоремы известны a priori; 2. математика (в противоположность естественным наукам) не имеет эмпирического содержания; 3. математика полагается только на доказательства, тогда как в естественных науках ставится эксперимент; 4. математические теоремы определены в такой степени, которой не может соответствовать ни одна теорема естественных наук [11].

Вопрос, следовательно, упирается в надежность работы ЭВМ. Правильность результатов математического эксперимента в рамках той или иной теории оказывается зависимым от того, насколько правильно ЭВМ осуществляет свои операции. А это определяется правильностью конструкции ЭВМ, работы ее элементов, воздействием внешних условий и т.д., т.е. в конечном счете - правильностью определенных положений естественных наук и технических расчетов. А это означает, что зависимость математики от естественных и технических наук становится все более важной. По словам Н. Бурбаки, математики всегда были уверены, что они доказывают «истины» или «истинные высказывания» [2]. Вопрос, таким образом, в том, аналогичны ли эти «истины» тем результатам, которые получены с помощью ЭВМ. Если принять, что использование ЭВМ в математических доказательствах обосновано и что ТЧК доказана, то последняя должна быть признана математической истиной. А это с необходимостью ведет к переоценке роли формального доказательства в философии математики. Этот вывод, конечно, не ставит под сомнение все то, что связано со статусом формальной теории как ветви математической логики. Однако, начиная с доказательства ТЧК, формальные доказательства оказываются не единственной исследовательской программой в математике. Но все дело в том, готовы ли математики признать математикой результаты, подобные ТЧК, а метод доказательства ТЧК включить в методологию математики.