Математическое доказательство: вчера, сегодня, завтра

Мои взгляды во многом противоположны взглядам первого докладчика. По меньшей мере 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.gz (первоначальный вариант)
http://mizar.org/trybulec65/8.pdf (пересмотренная версия)
Во второй части доклада было расказано о новых взглядах на математическое доказательство с точки зрения информатики: интерактивных доказательствах с «нулевым знанием», доказательствах, которые не обязательно читать целиком, чтобы поверить в их правильность, и т.п.
Видеозапись