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

Конечно, остается вопрос эстетики. После того как компьютер открыл новую «математическую истину» — вместе с доказательством, — человек или группа людей должны будут проверить ее и установить ее значимость. Интересна ли она? Полезна ли она? Как она вписывается в контекст предмета? Какие новые двери она открывает?

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

Один из триумфов искусства компьютерных доказательств пришелся как раз на булеву алгебру. Созданная Джорджем Булем в середине XIX в., она представляет собой математическую теорию контуров и переключателей. В одной из стандартных формулировок в этой теории всего пять определений и десять аксиом. Вот они:

Примитивными элементами булевой алгебры являются бинарная операция (мы можем представлять ее себе как объединение) и бинарная операция (мы можем представлять ее себе как пересечение). Кроме того, имеется символ унарной функции , который обозначает дополнение. Перечислим аксиомы булевой алгебры:

В 1930-х гг. Герберт Роббинс предположил, что эти 10 аксиом следуют только из трех довольно простых аксиом:

Несложно показать, что каждая булева алгебра, в соответствии с первоначальными десятью аксиомами (B₁)–(B₅) и ()–(), также является алгеброй Роббинса (т. е. удовлетворяет трем новым аксиомам (R₁)–(R₃)). Но на протяжении 60 лет оставался открытым вопрос о том, является ли каждая алгебра Роббинса булевой. В конце концов, на этот вопрос был получен положительный ответ Уильямом МакКьюном из Аргоннской национальной лаборатории. Он пользовался программой (разработанной в Аргонне) EQP (Equational Theorem Prover — доказыватель теорем-уравнений). Компьютер попросту сочетал аксиомы Роббинса миллионами способов, следуя строгим правилам логики, и обнаружил ту комбинацию, из которой следуют 10 аксиом булевой алгебры. Важно отметить, что после того, как доказательство гипотезы Роббинса нашел компьютер, Аллен Л. Манн [MAN1] построил доказательство на бумаге, которое может прочесть человек.

Компьютеры эффективно использовались для нахождения новых теорем в проективной геометрии и других классических областях математики. Удалось даже открыть некоторые новые теоремы евклидовой геометрии (см. работу [CHO]). Стикель [STI] смог получить результаты в алгебре. Новые теоремы были обнаружены также в теории множеств, теории решеток и в теории колец. Существует мнение, что эти результаты никогда не были обнаружены человеком потому, что люди никогда не были в них заинтересованы. Только время может подтвердить его или опровергнуть. Однако подтверждение гипотезы Роббинса представляет большой интерес для теоретических компьютерных дисциплин и для логики.

Одним из пионеров поиска компьютерных доказательств является Ларри Вос из Аргоннской национальной лаборатории. Он блестяще находит доказательства недоказанных теорем и более короткие версии известных доказательств. Все это он делает с помощью компьютера, зачастую пользуясь программой Otter, созданной МакКьюном.

Один из недавних прорывов — компьютерно порожденное решение задачи SCB в эквивалентном исчислении. Работы Воса включены в многие книги, в частности [WOS1] и [WOS2].

7.5 Как компьютер порождает доказательство нового результата

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

Как было сказано в предыдущем разделе, гипотеза Роббинса в булевой алгебре — выдающийся результат и важнейший новый факт, обнаруженный в результате компьютерного поиска. Следует понимать, что аксиомы булевой алгебры кристально ясные, аккуратные и ладно подогнаны друг к другу как кирпичики. Это система аналитического вывода, которая хорошо поддается новой технологии компьютерного доказательства теорем. Другие области, такие как действительный анализ, дифференциальные уравнения в частных производных и топология малой размерности, опирающиеся на синтетическую аргументацию, на картинки в доказательствах и ad hoc аргументы, неподвластны (по крайней мере на современном уровне знания в области компьютерных доказательств) компьютерному поиску. Некоторые, например Дорон Цайлбергер [ZEI], предрекают, что через 100 лет все доказательства будут порождаться компьютерами. Но при существующем состоянии искусства доказательства, как мы его наблюдаем, такое мнение представляется в лучшем случае чересчур оптимистичным.