Лекция 10 | Формальные методы в математике | Георгий Каданцев
Вставка
- Опубліковано 3 жов 2024
- 03.07.2024
Курс предлагает введение в мат. логику и теорию типов, а также обзор различных формальных систем, современных theorem prover'ов и их истории. В течение семинара предлагается освоить одно из программных средств доказательства теорем (Arend, agda, Coq) и формализовать с помощью него небольшой кусочек математики (алгебры или анализа).
Пререквизиты:
Умение подставлять одни выражения в другие и замечать аналогии.