Лекция по теории категорий начинается прямо сейчас по ссылке

записи лекций по теории категорий обновлены

Следующая лекция по типам (System F) пройдет завтра, 16 сентября, в 19:00 CEST/UTC+2 / 20:00 MSK

Через 15 минут начинаем лекцию по типам (cсылка в календаре и на странице курса).

Ссылки статьи, которые я обещал, приложил комментариями вот сюда.

запись 4й лекции можно найти по ссылке

Курс "Формализация математики в Lean"

Всем привет! В этом семестре в ШАДе совместно с formal labs будет проходить полусеместровый курс по формальной математике. Курс ведёт Василий Нестеров.

Первая лекция — в субботу, 19 сентября, в 11:00 MSK, лекция идёт 3 часа.

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

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

Будут домашние задания с автопроверкой в системе Manytask: https://app.manytask.org/lean-2026-fall/
Пароль для записи на курс: LemmaDilemma

Лекции будут проходить в зуме, ссылка появится позже.
Лекции будут записываться.

Лекция по формализации математики в Lean начнется через 15 минут: https://yandex.zoom.us/j/99316512535

Завтра продолжится курс по теории категорий. Наша цель — детально разобраться в двух фундаментальных понятиях теории категорий: (ко)пределах и сопряженных функторах.

Что мы обсудим (ключевые слова):

• Конусы над диаграммой (коконусы под диаграммой).
• Общее определение (ко)предела диаграммы.
• (Ко)пределы избранных форм:
- (ко)произведения,
- (ко)уравнители,
- (ко)декартовы квадраты,
- обратные и прямые пределы.
• Сопряженные функторы, универсальное свойство.
• Основные примеры: свобода-забвение и тензор-хом.
• Декартово замкнутые категории.

23 сентября, среда
19:00 CEST/UTC+2 (20:00 MSK)
Онлайн, вход свободный

Ссылка на зум на странице курса

Через 5 минут мы начинаем!

(ссылка на трансляцию на странице курса)

Всем привет! На manytask вышла первая домашка по Lean. Во всех задачах нужно заменить sorry на валидные доказательства. Чекер проверяет что доказательство компилируется и не содержит запрещенных тактик. В решении вы можете менять импорты, вводить новые теоремы, и делать все что угодно, только не менять формулировки задач.

Кроме того, появилась запись первой лекции

Для поиска лемм в Mathlib можно использовать leansearch.net (семантический поиск) и
loogle.lean-lang.org (синтаксический)

Вопросы можете задавать под этим постом, постараюсь оперативно отвечать

записи лекций по теории категорий обновлены

Лекция по формализации математики в Lean начнется через 30 минут: https://yandex.zoom.us/j/99316512535

В этот раз обсудим функции, множества и теорию типов, на которой строится Lean