Лекция 11 | Формальные методы в математике | Георгий Каданцев

09.07.2024
Курс предлагает введение в мат. логику и теорию типов, а также обзор различных формальных систем, современных theorem prover'ов и их истории. В течение семинара предлагается освоить одно из программных средств доказательства теорем (Arend, agda, Coq) и формализовать с помощью него небольшой кусочек математики (алгебры или анализа).
Пререквизиты:
Умение подставлять одни выражения в другие и замечать аналогии.