Skip to content

README.md

Latest commit

 

History

History
10 lines (7 loc) · 1.23 KB

README.md

File metadata and controls

10 lines (7 loc) · 1.23 KB

Верификация программ на 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.