|
|
Графы на поверхностях и кривые над числовыми полями
15 апреля 2020 г. 18:30–20:00, г. Москва, online
|
 |
|
 |
|
|
|
Верификация длинных доказательств: мечты, планы и реальность
Г. Б. Шабатab
a Институт теоретической и экспериментальной физики имени А.И. Алиханова Национального исследовательского центра «Курчатовский Институт»
b Российский государственный гуманитарный университет, г. Москва
|
| Количество просмотров: |
| Эта страница: | 260 |
|
Аннотация:
Речь в основном пойдет о незавершенном проекте Владимира Воеводского (предварительный итог которого подведен в коллективной монографии [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.
|
|
Обратная связь: