Доказательство конкретных утверждений с использованием компьютера может быть реализовано разными путями: с помощью систем искусственного интеллекта; построением контрпримеров (опровержение утверждений); полным перебором и проверкой правильности всех возможных случаев, возникающих при рассмотрении утверждения; синтетическим методом, то есть проверкой правильности части возможных случаев и сведением остальных случаев к ранее разобранным.

Искусственный интеллект. Специальные программные комплексы, называемые системами искусственного интеллекта, используют разные формы представления знаний и оперируют знаниями. Среди многочисленных применений подобных систем можно назвать и автоматическое доказательство теорем. Нелишне напомнить, что первые такие программы были написаны еще в 1957 году, спустя всего лишь 10 лет после появления компьютеров. Вначале они были достаточно просты, но затем все более и более усложнялись. Уровень старшеклассника средних способностей был ими быстро превзойден, но уровень хорошего математика не достигнут и поныне [45].

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

не имеет натуральных решений. Но в 1966 году Л.Лендер и Т.Паркин [7, c.101-103] с помощью компьютера для n=5 нашли опровергающий пример. И выглядит он так:

27⁵ + 84⁵ + 110⁵ + 133⁵ = 144⁵.

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

Синтетический метод. При использовании данного метода проверке правильности подвергается некоторое конечное, но обычно большое число возможных случаев, возникающих при рассмотрении утверждения, а затем показывается, что все остальные случаи тем или иным способом сводятся к ранее проверенным. Первая часть этой процедуры выполняется компьютером, а вторая - человеком. Разумеется, на человека ложится и все связанное с планированием работы, а также написанием соответствующих программ вычислений.

Один из наиболее ярких примеров использования синтетического метода для доказательства утверждений продемонстрировали в 1976 году К.Аппель и В.Хейкен [1, c.711-712; 2, c.108-121]. С помощью компьютера они решили знаменитую проблему топологии о четырех красках, которая не давалась математикам на протяжении более века. Было доказано, что любую карту можно раскрасить четырьмя цветами так, что никакие две области, имеющие общий участок границы, не будут окрашены одним цветом. Заметим, что в более слабой формулировке для пяти красок эта проблема была положительно решена в 1890 году, но понадобилось еще почти столетие и появление компьютера для её полного и окончательного решения. Найдено оно было примерно так. Компьютером было выделено около 1800 типовых карт, для раскраски которых достаточно четырех красок. Далее было установлено, что:

Из этих утверждений и вытекает, что для раскраски любой карты достаточно четырех красок.

Проводить детальное обсуждение решения проблемы о четырех красках из-за сложности соответствующей области знания мы не будем. Но для более ясного представления о сути обсуждаемого синтетического метода, существенно опирающегося при доказательстве утверждений на оба компонента в связке “человек + компьютер”, рассмотрим и достаточно подробно разберем решение нескольких более простых задач.