formal labs

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

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

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

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

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

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

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

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

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

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

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

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

https://arxiv.org/abs/0810.1279

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

Ссылка на сегодняшнюю лекцию

Ссылка на запись лекции 2 по теориям типов (STLC+System T):

https://us02web.zoom.us/clips/share/QrkQ7bSVRD-6O0Gwg62LRw

Сегодня вечером пройдет вторая вводная лекция по теории категорий. Поговорим про то, как язык функторов естественно возникает в линейной алгебре, теории групп и топологии

Это будет развитие рассказа про комбинаторные виды в новом контексте, так что будет полезно пересмотреть слайды с прошлого раза — я их улучшил после лекции, должно быть понятно

✨ Теория категорий: вторая лекция

На первой лекции я успел заметно меньше задуманного, так что многое, ради чего лекция затевалась, переезжает на вторую

🔵 Что значит «естественная конструкция»?

Математики постоянно говорят, что одна конструкция каноническая, а другая зависит от выбора. Разберёмся, что это значит формально — язык категорий тут и возникает

Начнём со школьной формулы замены базиса: из неё прямо вырастает определение естественного преобразования. Дальше посмотрим на конечномерное пространство и двойственное к нему — они изоморфны, но не канонически, а вот дважды двойственное уже канонически

Вторая половина лекции — про то, как язык категорий запрещает. Мы научимся доказывать, что конструкции не существует: функтора центра группы нет, окружность не ретракт диска. Из последнего почти бесплатно следует теорема Брауэра о неподвижной точке

Понадобятся линейная алгебра и основы теории групп. Топологию знать не нужно — всё, что оттуда берётся, я расскажу на пальцах

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

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

Начинаем лекцию через 2 минуты! Также прикладываем конспект для первых трех лекций для освежения памяти.

Лекция по типам начнется через час. Обратите внимание на то, что изменилась ссылка на зум (новая ссылка есть в календаре и на странице курса)

Напоминаем, что следующая лекция по типам (STLC и System T) уже завтра, 5 августа, в 19:00 CEST/UTC+2 / 20:00 MSK

⭐ Теория категорий: запись

Наконец, готова запись и слайды первой лекции курса по теории категорий

Я успел заметно меньше задуманного — больше половины материала осталась на следующий раз. Почти вся лекция ушла на теорию комбинаторных видов. Мне показалась, что это очень естественная мотивация категоричных понятий

🔵 Что такое комбинаторные виды?

Это язык, на котором удобнее формулировать задачи перечислительной комбинаторики. Школьное требование «предъявить красивую биекцию» получает в нём точный смысл — построить изоморфизм видов

На самом деле, виды это функторы, а их изоморфизмы — естественные преобразования. На лекции мы начали с видов, а категорные определения появились в самом конце, когда мы видели примеры уже много раз

Такое введение в теорию категорий — не самое стандартное. Если вы знаете хорошие мотивированные изложения категорий "с нуля" напишите в комментариях! Там же можно задавать любые вопросы по лекции

😱 Лекция шла 4 (!) часа, включая масштабное обсуждение после основной части. Его на записи нет, и вообще сам рассказ получился достаточно сумбурным — к сожалению, это частая проблема первой лекций, когда не понятна аудитория и скорость, с которой надо рассказывать.
Но я сильно переделал слайды, обязательно посмотрите, если было что-то непонятно

Запись · Слайды (html, pdf)

Начинаем через 5 минут!
Ссылка на зум на странице курса

Следующая лекция по теориям типов (STLC и System T) пройдет в среду 5 августа, в то же время (19:00 CEST/UTC+2 / 20:00 MSK).

Ссылка на запись первой лекции:
https://zoom.us/clips/share/YvHUOkq2Qa6-Yb4QQjhw8w

Онлайн-курс «Современные теории типов»

В среду 15 июля в 19:00 CEST/UTC+2 (20:00 MSK) в Лаборатории формальной математики стартует курс по современным теориям типов. Лекции читают @akuklev и @clayrat по средам, примерно по часу, частота - раз в неделю (с летними пропусками). Начнём с обзора формальных языков и алгебраических теорий и пойдём до самого фронтира синтетических и направленных теорий типов. Примерная программа:

1. Вводная лекция
2. Языки и алгебраические теории
3. STLC и System T
4. PCF
5. System F и Fω
6. Зависимо-типизированные языки
7. Индукция
8. Рефайнмент- и фактор-типы
9. Эффекты в типах
10. HoTT
11. OTT/CuTT
12. □-полиморфизм
13. Модальные типы
14. Охраняемая рекурсия
15. Когезивные модальности
16. Направленные и симплициальные теории

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

Ссылка на гугл-календарь, где будем публиковать даты лекций:
https://calendar.google.com/calendar/u/0?cid=YzdkMGI0MTdlZjFiMTg1OGVmNzUyYjFkZjBjYjYwZjBhYTI0MGExNjlhMWVhZGY5OTcyOGYwOTM4OTVlMDliM0Bncm91cC5jYWxlbmRhci5nb29nbGUuY29t

Тот же календарь, в формате .ics
https://calendar.google.com/calendar/ical/c7d0b417ef1b1858ef752b1df0cb60f0aa240a169a1eadf99728f093895e09b3%40group.calendar.google.com/public/basic.ics

Channel created