Формализация математики на языке Lean

Lean - функциональный язык программирования, который также можно использовать как инструмент интерактивного доказательства теорем. Разработка Lean началась Leonardo de Moura (Microsoft Research) в 2013 году.

В этом курсе мы познакомимся с Lean как с инструментом доказательства теорем, и разовьем базу теории нескольких сфер математики. Первая версия этого спецкурса проходила в апреле-июне 2021 года. В этом курсе используется версия Lean 3. Некоторые упражнения заимствованы из курса Formalising Mathematics от Kevin Buzzard.

Неделя №5 (21.05.2021)

Конечные множества и начало теории матроидов.

Неделя №4 (14.05.2021)

Упражнения на теорию групп и пределы последовательностей (week_2 и week_3 курса Formalising Mathematics).

Ресурсы:

1. Как пользоваться calc
2. Продолжение упражнений на теорию групп

Неделя №3 (07.05.2021)

Упражнения на формальные языки: конкатенация, замыкание Клини. Обновите репозиторий через git pull, чтобы увидеть новые задания.

Неделя №2 (30.04.2021)

Четыре файла с упражнениями на множества, функции, отношения и индуктивные типы (на примере деревьев). Скачайте репозиторий с помощью leanproject get vartem/lean-itmo и замените sorry (кроме тех, что использованы для иллюстрации) на доказательства.

Для документации по тактикам можете обратиться к https://leanprover-community.github.io/mathlib_docs/tactics.html.

Неделя №1 (23.04.2021)

Мы решали Natural Number Game. Если вы застряли, то можно подсмотреть решения.

К следующей встрече:

Обязательно

1. NNG: Addition + Multiplication + Function + Proposition + Adv. Proposition worlds.
2. Установить Lean 3, elan и leanproject по инструкции для вашей ОС (потребуются git и pip/pip3). Я использую Visual Studio Code с расширением для Lean, но можно использовать и emacs с lean-mode.

Сделано! А еще?

1. Дорешать NNG до конца.
2. Поиграть в еще одну короткую игру! Эта игра про max a b и неравенства.
3. Посмотреть на репозиторий tutorials с упражнениями

Интересные видео

1. Видео встречи на Youtube
2. Лекция The Future of Mathematics? от Kevin Buzzard
3. Демонстрация доказательства бесконечности простых чисел

Полезные ссылки

• Youtube-плейлист с записями встреч
• Главная страница leanprover-community
• Документация API mathlib
• Zulip чат, основное место для обсуждений про Lean
• Twitter и блог Kevin Buzzard про Lean
• Репозиторий tutorials с упражнениями для начинающих
• Конференция Lean for the Curious Mathematician 2020: видео лекций и репозиторий с упражнениями с воркшопов
• Конвенции именования функций в mathlib

Книги

• Список учебных ресурсов на leanprover-community
• Theorem Proving in Lean
• Mathematics in Lean и репозиторий, который можно скачать (leanproject get mathematics_in_lean) и интерактивно запускать код и следить за книгой