Онлайн-курс «Формализация математики в Lean»

Василий Нестеров

Полусеместровый курс по формальной математике в ШАДе совместно с Лабораторией формальной математики. Курс проходит осенью 2026 года по субботам в 11:00 MSK, первая лекция — 19 сентября. Лекции проходят онлайн в Zoom и записываются.

Цель курса — познакомиться с языком формальных доказательств Lean, научиться выражать на нём математические определения, утверждения и доказательства и понять, почему ему можно доверять при проверке доказательств.

Программа:

  1. Синтаксис Lean. Определения, теоремы, тактики. Пропозициональная логика.
  2. Логика с кванторами. Числа, функции и множества.
  3. Математический анализ.
  4. Алгебра, в том числе линейная.
  5. Дискретная математика.
  6. Вероятность.
  7. Формальная математика в эпоху ИИ.

Лекция 1

Вводная лекция
19 сентября 2026 года
видео

Домашние задания

Задания с автоматической проверкой доступны в Manytask. Пароль для записи на курс: LemmaDilemma.

Первое домашнее задание опубликовано 24 сентября. Во всех задачах нужно заменить sorry на корректные доказательства. Проверяющая система проверяет, что доказательство компилируется и не содержит запрещённых тактик.

В решениях можно менять импорты и вводить новые теоремы. Формулировки задач менять нельзя.

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

Лекции проходят в Zoom.