Семинары: Г. Б. Шабат, Верификация длинных доказательств: мечты, планы и реальность

СЕМИНАРЫ


Графы на поверхностях и кривые над числовыми полями 15 апреля 2020 г. 18:30, г. Москва, online

Верификация длинных доказательств: мечты, планы и реальность Г. Б. Шабат^ab ^a Институт теоретической и экспериментальной физики имени А.И. Алиханова Национального исследовательского центра «Курчатовский Институт» ^b Российский государственный гуманитарный университет, г. Москва
Аннотация: Речь в основном пойдет о незавершенном проекте Владимира Воеводского (предварительный итог которого подведен в коллективной монографии [1]), в котором предполагалось существенно расширить взаимодействие математиков c компьютерами при построении и проверке доказательств. После краткого обзора унивалентных оснований математики внимание будет сосредоточено на проблемах, возникающих в связи с доказательствами, традиционное понимание которых затруднено или невозможно по причине их длины и сложности. Будут приведены примеры; позиции докладчика будут критически сопоставлены с положениями известного провокационного текста Николая Вавилова [2]. В заключение будут высказаны соображения о формализации преподаваемой математики. [1] Homotopy Type Theory: Univalent Foundations for Mathematics. Univalent Foundations Project, Institute for Advanced Study, 2013. (465 pages) arXiv: 1308.0729 [2] Nikolai Vavilov. Reshaping the metaphor of proof. Philosophical Transactions of the Royal Society A. Mathematical, Physical, and Engineering Sciences, 2019. DOI: 10.1098/rsta.2018.0279 Заседание будет совмещенным с Научно-исследовательским семинаром по математической логике кафедры Математической логики и теории алгоритмов, ссылка на запись семинара: http://lpcs.math.msu.su/rus/nis.htm.