https://arxiv.org/abs/0810.1279

Майк Шульман — Теория множеств для нужд теории категорий: Теория множеств Фефермана, её сильный и слабый варианты

17 августа в 20:00 MSK (19:00 CET, 10:00 PT) пройдет доклад Лаборатории формальной математики. Приглашаются все желающие.

Спикер: Василий Ильин, Директор Лаборатории ИИ для Математики в Университете Вашингтона

Тема доклада: ИИ для формализации математики: прогресс за 4 месяца

Описание: Сравним ИИ 4 месяца назад и сегодня. Насколько мы близки к формализации всей математики и как к этому подступиться? Посмотрим на эксперименты в Physlib, решение 11 новых задач в LeanEval и краудсорсинг формализации в эру ИИ. Также обсудим как мерять качество формального кода и как презентовать ИИ проект по формализации.

Материалы:
• статьи https://arxiv.org/abs/2602.05216, https://arxiv.org/abs/2606.25363
• видео https://www.youtube.com/watch?v=H2z3VRRd4aQ
• краудсорсим формализацию https://github.com/Vilin97/lean-pool

Доклад пройдет в зуме по ссылке.

В ближайшую среду будет продолжение курса по теории категорий, лектором выступит Вася Ионин.

На лекции мы продолжим осваивать внутренний язык теории категорий. Рассказ будем сопровождать проясняющими примерами и полезными майндсетами, помогающими думать о категорных вещах.

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

• Взгляд на математические объекты через призму [данные, аксиомы].
• Жизнь внутри категории: мономорфизмы и эпиморфизмы, инициальные и терминальные объекты.
• Операции над категориями, категория категорий и категория функторов.
• Иерархия забывающих функторов.
• Эквивалентность категорий и принцип эквивалентности.
• Предельные и копредельные конструкции.

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

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

ИИ для формализации математики: прогресс за 4 месяца

Доклад начинается прямо сейчас в зуме по ссылке.

Видео и слайды с сегодняшнего доклада «ИИ для формализации математики: прогресс за 4 месяца»

Напоминание: уже сегодня, в среду, в 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