Лекции транслируются в Zoom (Идентификатор конференции: 815 6349 2059 Код доступа: 548372) и будут доступны на YouTube и на RuTube.

Анонс курса – на YouTube и на RuTube

Плейлист курса – на YouTube и на RuTube

Спецкурс в формате лекция + семинар

Для полноценного участия в семинаре, необходим компьютер.

Аннотация

Курс посвящён теоретическим основаниям и практике формальной верификации математических утверждений. На лекциях обсуждаются 𝜆-исчисление, интуиционистская логика, соответствие Карри– Говарда, зависимые типы, индуктивные типы и их роль в современных proof assistant’ах. Семинары полностью посвящены Lean: в первой половине курса изучается язык Lean, во второй библиотека формализованной математики mathlib.

Программа лекций

1. Бестиповое 𝜆-исчисление. Синтаксис. 𝛼-конверсия, 𝛽 и 𝜂-редукции. Теорема Чёрча-Россера (без доказательства). Комбинатор неподвижной точки и рекурсия.
2. Интуиционисткая логика. Семантика Брауэра-Гейтинга-Колмогорова. Натуральные выводы.
3. Простое типизированное 𝜆-исчисление (𝜆→). Типизация по Чёрчу и по Карри. Изморфизм КарриГоварда.
4. Интуиционисткая теория типов Мартин-Лёфа (MLTT). Σ-типы. Π-типы. Универсумы. Тип равенства.
5. Индуктивные типы. Единственность. 𝑊-типы. Семантика индуктивных типов. Равенство как индуктивный тип.
6. Теория типов Lean. Универсум Prop. Proof-Irrelevance. Subsigleton elimination. Экстенсиональность. Классические принципы: закон исключённого третьего и аксиома Выбора. Фактор-типы.
7. Алгоритмические вопросы*.
8. Гомотопическая теория типов*.

Программа семинаров

Часть 1. Знакомство с Lean.

1. Термовый язык Lean. Установка Lean и настройка среды. Термы и типы. Функции: абстракция и эвалюация. Определения локальные и глобальные. Переменные, секции и пространства имён. Зависимые типы.
2. Высказывания и доказательства. Высказывания как типы. Логика высказываний. Теория типов и классическая логика.
3. Кванторы и равенство. Квантор всеобщности. Пропозициональное и вычислительное равенство. Квантор существования.
4. Тактики. Базовые тактики. Тактикалы. Переписывание и simp. Структурирование доказательств.
5. Индуктивные типы. Натуральные числа, списки, деревья. Индуктивно определяемые предикаты. Тактики, связанные с индуктивными типами. Взаимные и вложенные индуктивные типы.
6. Индукция и рекурсия. Паттерн-матчинг. Структурная рекурсия и индукция. Сильная (не структурная) рекурсия и индукция. Функциональная индукция. Взаимная рекурсия. Зависимый паттерн-матчинг.
7. Структуры и классы. Structure и Record в Lean. Классы типов и поиск экземпляров. Нотации, coercions, implicit arguments. Как Lean представляет алгебраические структуры.
8. Аксиомы и вычислимость. Экстенсиональность. Факторы. Аксиома выбора. Закон исключённого третьего.

Часть 2. Знакомство с MathLib.

1. Обзор mathlib: устройство библиотеки.
2. Множества, функции и отношения в mathlib.
3. Алгебра в mathlib.
4. Арифметика, комбинаторика и конечные объекты.
5. Анализ и топология в mathlib.

Библиография

[1] The Lean Developers, «The Lean Language Reference Manual». [Онлайн]
[2] J. Avigad, L. de Moura, S. Kong, S. Ullrich, и with contributions from the Lean Community, «Theorem Proving in Lean 4». [Онлайн]
[3] J. Avigad и P. Massot, «Mathematics in Lean». [Онлайн]
[4] The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics. 2013. [Онлайн]
[5] M. H. B. Sørensen и P. Urzyczyn, Lectures on the Curry-Howard Isomorphism. Elsevier Science, 2006. [Онлайн]
[6] J.-Y. Girard, Y. Lafont, и P. Taylor, Proofs and Types. Cambridge University Press, 1989. [Онлайн]

Программа файлом