Верификация программ на Lean

Это репозиторий курса по формальной верфикации программ в системе Lean, читаемый в Центральном Университете осенью 2025 года. Он будет пополнятся материалами (лекциями, семинарами, домашними заданиями) по мере движения курса.

С чего начать?

1. Установите git.
2. Установите VS Code и Lean по инструкции с официального сайта Lean.
3. В VS Code в расширении для Lean 4 нажмите Open Project -> Download Project и введите ссылку на этот репозиторий. Начнется скачивание репозитория и нужных зависимостей.
4. Проверьте что все работает корректно, открыв файл Test.lean в корне репозитория. Файл должен прогрузиться без ошибок а строка с #check выдать сообщение TopologicalSpace.{u} (X : Type u) : Type u.