Тезисы доклада Н.А. Вавилова
ЧТО ДОКАЗЫВАЕТ МАТЕМАТИЧЕСКОЕ ДОКАЗАТЕЛЬСТВО?
В последнее время все чаще обсуждается вопрос об
изменении статуса доказательства и уменьшении нашей уверенности
в справедливости результатов. Критика и скептицизм подобного
рода наиболее энергично, часто и агрессивно озвучиваются
в двух следующих направлениях.
--- Сомнения в надежности доказательств, выполненных с
помощью компьютера.
--- Сомнения в надежности исключительно длинных и сложных
доказательств.
Однако я склонен верить, что статус трудных современных
результатов --- и их доказательств! --- мало отличается от
статуса трудных математических результатов предшествующих
веков. Я готов проиллюстрировать многочисленными историческими
примерами, что фактические математические доказательства
НИКОГДА --- со времен греков --- не удовлетворяли
декларируемым стандартам.
Классические работы, как и публикуемые сегодня, полны
заблуждений, ошибок и пробелов разной степени серьезности.
Что гораздо хуже, часто эти заблуждения и ошибки из поколения
в поколение воспроизводятся в монографиях и учебниках, и их
обнаружение в некоторых случаях потребовало многих десятилетий.
Следуя Конфуцию, я приглашаю к вскрытию ошибок, а не к их
замазыванию. Нужно честно признать, что математика является
человеческой деятельностью, целью и результатом которой является
понимание, и мало отличается в смысле своей надежности от
других видов человеческой деятельности. Достоверность
математического доказательства и его убедительность относится
к области психологии и социологии, а не логики.
В отличие от любых доказательств, математическое знание
КАК ТАКОВОЕ обладает ЧРЕЗВЫЧАЙНО высокой степенью надежности.
Эта надежность, как и надежность естественно-научного
и технического знания, гарантируется отнюдь не доказательствами
индивидуальных результатов, а общей когерентностью математической
и естественно-научной картины мира, индивидуальным и коллективным
пониманием и прямым контактом с миром идей, которое формируется
в процессе работы у каждого квалифицированного и понимающего
специалиста.
Вот, что знают о доказательстве практикующие математики,
но боятся сказать:
--- Математическое доказательство, РАССМАТРИВАЕМОЕ КАК ТЕКСТ,
не доказывает ничего, кроме факта существования доказательств.
--- Ни одно СЕРЬЕЗНОЕ математическое доказательство не может быть
полностью формализовано, т.е. записано в соответствии
со стандартами, пропагандируемыми математической логикой.
--- Доказательство классификации простых конечных групп
обладает ГОРАЗДО более высокой степенью достоверности, чем
доказательства большинства общепризнанных классических результатов
в области топологии, анализа или теории дифференциальных уравнений.
А что касается компьютерных вычислений, то лично я склонен
доверять им больше, чем любым математическим доказательствам, КРОМЕ
САМЫХ ПРОСТЫХ.
Тезисы доклада Ю.В. Матиясевича
Мои взгляды во многом противоположны взглядам первого докладчика. По
меньшей мере 99.999%
теорем, доказываемых современными математиками, выводятся из аксиом
теории множеств, и потому эти теоремы в принципе могут быть изложены по всем
канонам математической логики. Критерием может служить требование,
чтобы доказательство было проверено компьютером.
Более того, реальная работа в этом направлении ведется давно,
и на этом пути достигнут существенный прогресс. Примером
могут служить полная формализация доказательства первой теоремы
Геделя о неполноте и теоремы о четырех красках. Систематическое
формальное
изложение математики много лет ведется в рамках проекта MIZAR,
результаты публикуются в журнале "Formalized mathematics"
(http://mizar.org/fm/). Цели подобной формализации изложены в виде
"QED manifesto":
http://en.wikipedia.org/wiki/QED_manifesto
http://www.cs.ru.nl/~freek/qed/qed.ps.gzi (первоначальный вариант)
http://mizar.org/trybulec65/8.pdf (пересмотренная версия)
Если позволит время, во второй части доклада будет расказано о новых
взглядах на математическое доказательство с точки зрения информатики:
интерактивных доказательствах с "нулевым знанием", доказательствах,
которые не обязательно читать целиком, чтобы поверить в их правильность,
и т. п.