Математическая гостиная. Лев Беклемишев «Компьютерные доказательства»
Лев Дмитриевич Беклемишев, известный российский математик, доктор физико-математических наук, академик РАН, выступил в рамках проекта «Математическая гостиная» 5 мая 2021 года в стенах Адыгейского государственного университета с лекцией на тему «Компьютерные доказательства». Главной ценностью "гостиной" всегда была возможность встретиться и послушать интересные лекции людей, чей вклад в математическую науку является бесценным как на отечественном, так и на мировом уровне, а также пообщаться с выступающими. Являясь экспертом в области математической логики, заместителем директора по научной работе и главным научным сотрудником математического института имени В.А. Стеклова РАН, профессором кафедры математической логики и теории алгоритмов механико-математического факультета МГУ и факультета математики НИУ ВШЭ, Львом Дмитриевичем был пройден огромный путь в вопросах изучения проблем математических доказательств с использованием компьютерных систем и не только. Основная книга по Coq под названием «CoqArt»: https://www.labri.fr/perso/casteran/C...
Материалы практикума по Coq (за авторством В.Н. Крупского и С.Л. Кузнецова), содержащие также ссылки на другие источники: http://www.mi-ras.ru/~sk/lehre/coq/co...
Страница практикума с упражениями и прочими материалами: http://www.mi-ras.ru/~sk/lehre/coq/
Помимо системы Coq, имеются и другие - Aqda и Lean, на которые также стоит обратить внимание. Справочная книга, состоящая из обзорных статей на тему автоматического доказательства теорем: «Handbook of automated reasoning». ____________ Много интересного можно найти в нашей группе ВК: https://vk.com/kavmatagu
Последние события в нашем аккаунте Инстаграм: / kavmatagu
