Всем привет! В этом семестре в ШАДе совместно с formal labs будет проходить полусеместровый курс по формальной математике. Курс ведёт Василий Нестеров.
Первая лекция — в субботу, 19 сентября, в 11:00 MSK, лекция идёт 3 часа.
Цель курса: познакомиться с языком формальных доказательств Lean, понять как на нем выражать известные математические конструкции (определения, утверждения и доказательства), понять почему ему можно доверять в проверке доказательств.
Программа:
1. Синтаксис Lean. Определения, теоремы, тактики. Пропозициональная логика.
2. Логика с кванторами. Числа, функции и множества
3. Математический анализ
4. Алгебра, в том числе линейная
5. Дискретная математика
6. Вероятность
7. Формальная математика в эпоху ИИ
Будут домашние задания с автопроверкой в системе Manytask: https://app.manytask.org/lean-2026-fall/
Пароль для записи на курс:
LemmaDilemmaЛекции будут проходить в зуме, ссылка появится позже.
Лекции будут записываться.