Подробности
14.03.2010 18:23

Совместное заседание Санкт-Петербургского математического общества и Секции математики Дома ученых

23 марта 2010 г.

Дом ученых, Дворцовая наб., 26, Белый зал, 18 час.
Математическое доказательство: Вчера, Сегодня, Завтра
Выступают: Н.А. Вавилов, Ю.В. Матиясевич 

Тезисы доклада Н.А. Вавилова


Что доказывает математическое доказательство?


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

  • Сомнения в надежности доказательств, выполненных с помощью компьютера.
  • Сомнения в надежности исключительно длинных и сложных доказательств.

Однако я склонен верить, что статус трудных современных результатов - и их доказательств! - мало отличается от статуса трудных математических результатов предшествующих веков. Я готов проиллюстрировать многочисленными историческими примерами, что фактические математические доказательства НИКОГДА - со времен греков - не удовлетворяли декларируемым стандартам.
Классические работы, как и публикуемые сегодня, полны заблуждений, ошибок и пробелов разной степени серьезности. Что гораздо хуже, часто эти заблуждения и ошибки из поколения в поколение воспроизводятся в монографиях и учебниках, и их обнаружение в некоторых случаях потребовало многих десятилетий.
Следуя Конфуцию, я приглашаю к вскрытию ошибок, а не к их замазыванию. Нужно честно признать, что математика является человеческой деятельностью, целью и результатом которой является понимание, и мало отличается в смысле своей надежности от других видов человеческой деятельности. Достоверность математического доказательства и его убедительность относится к области психологии и социологии, а не логики.
В отличие от любых доказательств, математическое знание как таковое обладает чрезвычайно высокой степенью надежности. Эта надежность, как и надежность естественно-научного и технического знания, гарантируется отнюдь не доказательствами индивидуальных результатов, а общей когерентностью математической и естественно-научной картины мира, индивидуальным и коллективным пониманием и прямым контактом с миром идей, которое формируется в процессе работы у каждого квалифицированного и понимающего специалиста.
Вот, что знают о доказательстве практикующие математики, но боятся сказать:

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

А что касается компьютерных вычислений, то лично я склонен доверять им больше, чем любым математическим доказательствам, кроме самых простых.

Тезисы доклада Ю.В. Матиясевича

 

Мои взгляды во многом противоположны взглядам первого докладчика. По меньшей мере 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 (пересмотренная версия)

Если позволит время, во второй части доклада будет расказано о новых взглядах на математическое доказательство с точки зрения информатики: интерактивных доказательствах с "нулевым знанием", доказательствах, которые не обязательно читать целиком, чтобы поверить в их правильность, и т. п.
--
St. Petersburg Mathematical Society               Phone 7 (812) 312 8829
27 Fontanka, 191023 St. Petersburg                Fax   7 (812) 310 5377
E-mail:  Этот адрес электронной почты защищен от спам-ботов. У вас должен быть включен JavaScript для просмотра. WWW-site: http://www.mathsoc.spb.ru