MIPT-Coq-25-Lect-01

Интерактивное доказывание теорем (Coq) в МФТИ. Темы: идея интерактивного доказывания теорем; неформальное введение в лямбда-исчисления.