TGViewer
Channel Public Channel
formal labs

formal labs

@formallabs

Open in Telegram
Subscribers
418
Photos
0
Videos
0
Links
30
Recent Posts 20 shown
Post #46 318
formal labs Завтра продолжится курс по теории категорий. Наша цель — детально разобраться в двух фундаментальных понятиях теории категорий: (ко)пределах и сопряженных функторах. Что мы обсудим (ключевые слова): • Конусы над диаграммой (коконусы под диаграммой). • Общее…
записи лекций по теории категорий обновлены
Zoom Теория категорий 2026
  • 🔥 6
  • 👍 4
Post #45 353
Всем привет! На manytask вышла первая домашка по Lean. Во всех задачах нужно заменить sorry на валидные доказательства. Чекер проверяет что доказательство компилируется и не содержит запрещенных тактик. В решении вы можете менять импорты, вводить новые теоремы, и делать все что угодно, только не менять формулировки задач.

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

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

Вопросы можете задавать под этим постом, постараюсь оперативно отвечать
  • 👍 7
  • 🥰 4
  • 🔥 3
Post #44 348
formal labs Завтра продолжится курс по теории категорий. Наша цель — детально разобраться в двух фундаментальных понятиях теории категорий: (ко)пределах и сопряженных функторах. Что мы обсудим (ключевые слова): • Конусы над диаграммой (коконусы под диаграммой). • Общее…
Через 5 минут мы начинаем!

(ссылка на трансляцию на странице курса)
formal-labs.github.io Онлайн-курс «Теория категорий» — Лаборатория формальной математики Онлайн-курс «Теория категорий».
  • 🔥 7
Post #43 456
Завтра продолжится курс по теории категорий. Наша цель — детально разобраться в двух фундаментальных понятиях теории категорий: (ко)пределах и сопряженных функторах.

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

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


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

Ссылка на зум на странице курса
  • 🔥 8
  • ❤ 3
  • 😱 3
  • 👍 2
Post #42 632
formal labs Курс "Формализация математики в Lean" Всем привет! В этом семестре в ШАДе совместно с formal labs будет проходить полусеместровый курс по формальной математике. Курс ведёт Василий Нестеров. Первая лекция — в субботу, 19 сентября, в 11:00 MSK, лекция идёт…
Лекция по формализации математики в Lean начнется через 15 минут: https://yandex.zoom.us/j/99316512535
Zoom Join our Cloud HD Video Meeting Zoom is the leader in modern enterprise cloud communications.
  • 🤔 2
Post #41 1.59K
Курс "Формализация математики в 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

Лекции будут проходить в зуме, ссылка появится позже.
Лекции будут записываться.
  • 🔥 32
  • 👏 7
  • ❤ 4
  • 👍 2
Post #39 513
formal labs Через 15 минут начинаем лекцию по типам (cсылка в календаре и на странице курса).
Ссылки статьи, которые я обещал, приложил комментариями вот сюда.
  • ❤ 3
Post #33 581
Следующая лекция по типам (System F) пройдет завтра, 16 сентября, в 19:00 CEST/UTC+2 / 20:00 MSK
  • ❤ 6
  • 👍 2
  • 🎉 1
Post #32 938
formal labs Сегодня продолжаем курс по теории категорий! Что мы сегодня обсудим: • Инициальные и терминальные объекты. • Мономорфизмы и эпиморфизмы, . • Естественные преобразования (revisited), вычисление хом-сетов естественных преобразований. • Основная теорема теории…
записи лекций по теории категорий обновлены
Zoom Теория категорий 2026
  • 🔥 15
  • 👍 5
  • ❤ 3
  • 😢 2
Post #31 845
formal labs Сегодня продолжаем курс по теории категорий! Что мы сегодня обсудим: • Инициальные и терминальные объекты. • Мономорфизмы и эпиморфизмы, . • Естественные преобразования (revisited), вычисление хом-сетов естественных преобразований. • Основная теорема теории…
Лекция по теории категорий начинается прямо сейчас по ссылке
  • ❤ 2
  • 👍 1
Post #30 805
Сегодня продолжаем курс по теории категорий!

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

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


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

Ссылка на зум на странице курса
  • 👍 11
  • 🔥 8
  • ❤ 6
Post #29 919
Сегодня лекции по теории категорий не будет — переносим её на следующую неделю (увы!)

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

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

Подробные анонсы появятся позднее.
  • 😢 10
  • 🥰 5
  • 👍 4
  • ❤ 2
Post #27 1K
Следующая лекция по типам (PCF) пройдет завтра, 26 августа, в 19:00 CEST/UTC+2 / 20:00 MSK
  • 👍 4
Post #26 1.28K
formal labs В ближайшую среду будет продолжение курса по теории категорий, лектором выступит Вася Ионин. На лекции мы продолжим осваивать внутренний язык теории категорий. Рассказ будем сопровождать проясняющими примерами и полезными майндсетами, помогающими думать о…
Плейлист — первые три лекции по теории категорий
Zoom Теория категорий 2026
  • ❤ 7
  • 👍 4
  • 🎉 1
Post #25 1.14K
homework-system-t.pdf148.4 KB
Следующая лекция по теориям типов планируется в следующую среду, 26го августа, а пока предлагаем вам прорешать домашние задания по предыдущей лекции (System T, NbE и Dialectica-трансляция).
  • 👍 7
  • 🔥 4
Older posts →

About this channel

How can I read @formallabs without a Telegram account?
TGViewer shows the public web preview Telegram publishes for formal labs: recent posts, photos, videos and the subscriber count, with no app, login or account.
How many subscribers does formal labs have?
formal labs (@formallabs) has 418 subscribers on Telegram, refreshed roughly every 30 minutes.
Does formal labs know I viewed it here?
No. Public channel previews carry no viewer identity, and TGViewer has no accounts or tracking of what you look up.
Threads Profile ViewerView any public Threads profile without an account.Open ThreadLook →Writing with AI? Make it sound human.Metric37 rewrites AI drafts so they read naturally. Free AI detector, 1,500 words free.Try Metric37 →