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

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

В качестве типичного отклика математика на работу Аппеля—Хакена приведем высказывание Фрэнка Бонсалла:

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

Даниэль Коэн зашел еще дальше и назвал доказательство Аппеля—Хакена «компьютерными махинациями». Он заявил, что их «доказательство» не «объясняет».

С этого момента пружина сюжета закручивается еще сильнее, так как в 1975 г. в доказательстве Аппеля—Хакена обнаружилась ошибка. Выявились проблемы с алгоритмом, которые Аппель и Хакен скормили компьютеру. Позднее были внесены исправления и в 1976 г. была опубликована статья [APH2], в которой декларировалось, что задача о четырех красках решена.

Оскар Лэнфорд указал, что для подтверждения компьютерных вычислений как части доказательства недостаточно доказать, что программа верна. Нужно еще понимать, как компьютер округляет числа, как работают операционная система и система распределения времени. Полезно еще знать, как хранятся данные в ЦПУ (чип). Не похоже, что все, кто интенсивно использует компьютеры в своих доказательствах, идут дальше первого пункта в этом списке.

В статье [APH3], опубликованной в 1986 г. в журнале «Mathematical Intelligencer», Аппель и Хакен указывают, что читатель их основной статьи [APH1] 1976 г. должен освоить

50 страниц текста с диаграммами, 85 страниц с дополнительными 2500 диаграммами да еще 400 страниц, в которых тоже есть диаграммы и тысячи отдельных проверок утверждений 24 лемм, сформулированных в основном тексте.

Авторы признают, что их доказательство требует более 1200 часов машинного времени, что в их работе имелись типографские ошибки и опечатки. Все же они выражают уверенность, что читатель поймет, «почему опечатки, тут и там встречающиеся в доказательстве, не влияют на его устойчивость». Некоторые ошибки, найденные уже после публикации, пишут авторы, были «устранены в течение двух недель». К 1981 г. У. Шмидт проверил «около 40%» ключевых 400 страниц и исправил 15 ошибок. В книге [APH4] описана история решения задачи, привлеченные методы и описание всех попыток Аппеля—Хакена. Там же доказано, что любую карту можно раскрасить за полиномиальное время (это понятие обсуждается в разд. 11.7).

Еще много лет после описанных событий на факультете математики университета штата Иллинойс на всех исходящих письмах красовалась одна марка. На ней было написано:

ЧЕТЫРЕХ КРАСОК ДОСТАТОЧНО

Своеобразное выражение триумфа Аппеля, Хакена и их суперкомпьютера.

Но даже в раю бывают неприятности. Один математический авторитет, пожелавший остаться неназванным, утверждает, что в доказательстве Аппеля—Хакена все еще обнаруживаются ошибки. По-видимому, любую найденную ошибку можно исправить. По крайней мере до сих пор так оно и было. Однако поток ошибок не иссякает. Так заслуживает ли работа Аппеля—Хакена названия «доказательство»? Можно ли считать доказательством органическую массу, которая никогда вполне не совершенна и требует постоянной починки? Еще Евклид 2300 лет тому назад считал, что нет!