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

Следует еще заметить, что важная компьютерная программа — это не фиксированная неизменная единица; это растущий и изменчивый организм. Компьютерные программы — для банков, производства, университетов, правительства — постоянно модифицируются и обновляются. И проверка модифицированной программы ничуть не легче проверки фиксированной. Все проблемы сохраняются. Проверки не переносятся с объекта на объект, и большая проверка не составляется очевидным образом из меньших. Так что роль проверки становится не такой простой. Интересное обсуждение некоторых из этих идей можно найти в статьях [MAK], [KOL], [FET] и [DLP].

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

7.4 Как компьютер может исследовать набор аксиом для получения утверждений и доказательств новых теорем

Майкл Атья в работе [ATI2] опять дает нам пищу для размышлений:

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

Современные языки программирования высокого уровня позволяют вносить в компьютер определения и аксиомы логических систем. Причем имеются в виду не просто слова, которые передают идеи. Машине можно передать информацию о связях между идеями. При этом допустимы правила логики и так далее. Язык программирования (скажем, Otter) может обладать специальным синтаксисом для введения такой информации. С такими данными компьютер может искать допустимые цепочки аналитической индукции (следуя встроенным правилам логики и опираясь только на запрограммированные аксиомы) и приводить к новым истинным утверждениям или теоремам. Такое программное обеспечение для доказательства теорем может работать в двух режимах:

• в интерактивном, когда машина периодически останавливается, чтобы пользователь мог ввести дальнейшие инструкции;

• в пакетном, когда машина выполняет всю работу за раз и в конце выдает результат.

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

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

Булева алгебра

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

Таким образом, эта область не вполне поддается компьютерным доказательствам, и они обошли ее стороной[90].

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