Напоминание: уже сегодня, в среду, в 20:00 MSK (19:00 CEST/UTC+2) пройдет лекция Васи Ионина по теории категорий.

начинаем лекцию курса по теории категорий https://us02web.zoom.us/j/85792683781?pwd=Bu95LejaCO48RkqfcmeWfeXfWjG5ia.1

Следующая лекция по теориям типов планируется в следующую среду, 26го августа, а пока предлагаем вам прорешать домашние задания по предыдущей лекции (System T, NbE и Dialectica-трансляция).

Плейлист — первые три лекции по теории категорий

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

Через 5 минут начинаем лекцию по типам! Ссылка в календаре и на странице курса.

Сегодня лекции по теории категорий не будет — переносим её на следующую неделю (увы!)

Таким образом, ближайшие лекции:
1) 9 сентября (среда) — теория категорий (Василий Ионин)
2) 16 сентября (среда) — теория типов (Александр Куклев и Александр Грызлов)

Обе лекции пройдут в обычное время — 20:00 MSK (19:00 CEST/UTC+2).

Подробные анонсы появятся позднее.

Сегодня продолжаем курс по теории категорий!

Что мы сегодня обсудим:

• Инициальные и терминальные объекты.
• Мономорфизмы и эпиморфизмы, .
• Естественные преобразования (revisited), вычисление хом-сетов естественных преобразований.
• Основная теорема теории категорий.
• Принцип эквивалентности.
• Расширения Кана.
• Пределы и копределы диаграмм: примеры и общий формализм.

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

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

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

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

Следующая лекция по типам (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