Recap про FCA
Перед завтрашним семинаром можно посмотреть предыдущие доклады Егора:
▫️ Егор Дудырев, Неформальное введение в Анализ Формальных Понятий, 2024. YouTube | Дзен | RuTube (~1 час 30 минут);
▫️ Егор Дудырев, Модели человеческих знаний, или Когда простейшие правила работают на уровне градиентных бустингов, 2023. YouTube | Дзен | RuTube (~1 час 10 минут).
И еще вспомнить подборку про FCA.
Перед завтрашним семинаром можно посмотреть предыдущие доклады Егора:
▫️ Егор Дудырев, Неформальное введение в Анализ Формальных Понятий, 2024. YouTube | Дзен | RuTube (~1 час 30 минут);
▫️ Егор Дудырев, Модели человеческих знаний, или Когда простейшие правила работают на уровне градиентных бустингов, 2023. YouTube | Дзен | RuTube (~1 час 10 минут).
И еще вспомнить подборку про FCA.
Про FCA для кластеризации и не только
В дополнение к докладу на прошлой неделе Егор рекомендует несколько статей от других команд, работающих над схожими задачами.
Две статьи про кластеризации от коллег из Ля Рошеля, которые так же разрабатывают теорию узорных структур (eng. Pattern Structures) :
▫️ Boukhetta S., Trabelsi M., Formal Concept Analysis for Trace Clustering in Process Mining, at ICCS 2023;
▫️ Waffo Kemgne M. et al., Fuzzy and Overlapping Communities Detection: An Improved Approach Using Formal Concept Analysis, at ASONAM 2024.
Две статьи от коллег из университета Артуа, где кластеризацию и бинарную классификацию решают через SAT солверы:
▫️ Ben Hassine M. et al, On the Discovery of Conceptual Clustering Models Through Pattern Mining, at ECAI 2024;
▫️ Hidouri A. et al., On the Learning of Explainable Classification Rules through Disjunctive Patterns, at ICTAI 2024.
В этой статье можно найти подробный обзор символьных подходов к кластеризации:
▫️ Pérez-Suárez A. et al., A review of conceptual clustering algorithms, in Artificial Intelligence Review, 2018.
Напоследок, в этой статье ниже можно найти множество техник и алгоритмов для оптимизации переборов описаний на бинарных данных:
▫️ Szathmary L. et al., A fast compound algorithm for mining generators, closed itemsets, and computing links between equivalence classes, in Annals of Mathematics and AI, 2014.
В дополнение к докладу на прошлой неделе Егор рекомендует несколько статей от других команд, работающих над схожими задачами.
Две статьи про кластеризации от коллег из Ля Рошеля, которые так же разрабатывают теорию узорных структур (eng. Pattern Structures) :
▫️ Boukhetta S., Trabelsi M., Formal Concept Analysis for Trace Clustering in Process Mining, at ICCS 2023;
▫️ Waffo Kemgne M. et al., Fuzzy and Overlapping Communities Detection: An Improved Approach Using Formal Concept Analysis, at ASONAM 2024.
Две статьи от коллег из университета Артуа, где кластеризацию и бинарную классификацию решают через SAT солверы:
▫️ Ben Hassine M. et al, On the Discovery of Conceptual Clustering Models Through Pattern Mining, at ECAI 2024;
▫️ Hidouri A. et al., On the Learning of Explainable Classification Rules through Disjunctive Patterns, at ICTAI 2024.
В этой статье можно найти подробный обзор символьных подходов к кластеризации:
▫️ Pérez-Suárez A. et al., A review of conceptual clustering algorithms, in Artificial Intelligence Review, 2018.
Напоследок, в этой статье ниже можно найти множество техник и алгоритмов для оптимизации переборов описаний на бинарных данных:
▫️ Szathmary L. et al., A fast compound algorithm for mining generators, closed itemsets, and computing links between equivalence classes, in Annals of Mathematics and AI, 2014.
Семинар про модель Cotype Nano от MTS AI
▫️ 19 февраля (среда), 17:00 МСК
▫️ Подключение→
Выступает: Алан-Барсаг Газзаев, разработчик-исследователь в MTS AI, магистрант второго курса в ИТМО
Тема: Обучение языковой модели Cotype Nano
Аннотация
Языковые модели развиваются стремительным образом. В то же время, они занимают очень много ресурсов для обучения и для инференса. Поэтому, одним из важных трендов в NLP является тренд на уменьшение размеров языковых моделей. Современные модели размером от 0.5B параметров превосходят в производительности старые LLM размеров в 7 и 14 миллиардов параметров. И мы обучили одну из них. В докладе мы затронем процесс обучения модели Cotype Nano, который несколько месяцев был лидером в своей весовой категории, а также расскажем про квантизацию этой модели
Уровень сложности: начинающий/средний, для понимания доклада будет достаточно базовых знаний по NLP
Ключевые слова: LLM, NLP, Supervised Fine-tuning, Data Generation, Data Preparation
▫️ 19 февраля (среда), 17:00 МСК
▫️ Подключение→
Выступает: Алан-Барсаг Газзаев, разработчик-исследователь в MTS AI, магистрант второго курса в ИТМО
Тема: Обучение языковой модели Cotype Nano
Аннотация
Языковые модели развиваются стремительным образом. В то же время, они занимают очень много ресурсов для обучения и для инференса. Поэтому, одним из важных трендов в NLP является тренд на уменьшение размеров языковых моделей. Современные модели размером от 0.5B параметров превосходят в производительности старые LLM размеров в 7 и 14 миллиардов параметров. И мы обучили одну из них. В докладе мы затронем процесс обучения модели Cotype Nano, который несколько месяцев был лидером в своей весовой категории, а также расскажем про квантизацию этой модели
Уровень сложности: начинающий/средний, для понимания доклада будет достаточно базовых знаний по NLP
Ключевые слова: LLM, NLP, Supervised Fine-tuning, Data Generation, Data Preparation
Семинар про оптимизацию сталеварения
▫️ 26 февраля (среда), 17:00 МСК
▫️ Подключение→
Выступает: Ярослав Шмулев, Cofounder / CTO R77 AI (@r77_ai)
Тема: Рекомендательная система для завода по оптимизации процесса производства стали
Аннотация
На семинаре будет рассмотрен кейс оптимизация потребления ферросплавов в конвертерном цехе для снижения затрат при производстве стали высокого качества. В ходе доклада будет представлен подход реализации рекомендательного сервиса на базе моделей машинного обучения.
Уровень сложности: начинающий
Ключевые слова: предиктивная аналитика, ML, прогнозирование временных рядов, оптимизация, рекомендации, сталеварение, металлургия
▫️ 26 февраля (среда), 17:00 МСК
▫️ Подключение→
Выступает: Ярослав Шмулев, Cofounder / CTO R77 AI (@r77_ai)
Тема: Рекомендательная система для завода по оптимизации процесса производства стали
Аннотация
На семинаре будет рассмотрен кейс оптимизация потребления ферросплавов в конвертерном цехе для снижения затрат при производстве стали высокого качества. В ходе доклада будет представлен подход реализации рекомендательного сервиса на базе моделей машинного обучения.
Уровень сложности: начинающий
Ключевые слова: предиктивная аналитика, ML, прогнозирование временных рядов, оптимизация, рекомендации, сталеварение, металлургия
Про ML в металлургии
Статьи, которые упоминал Ярослав в докладе на прошлой неделе:
▫️ Помощник сталевара: для чего металлургам нужно машинное обучение? 2021 (~9 минут);
▫️ Про внедрение ИИ в сталелитейную компанию и борщ, 2024 (~9 минут).
Также подписывайтесь на канал коллег: @r77_ai
Статьи, которые упоминал Ярослав в докладе на прошлой неделе:
▫️ Помощник сталевара: для чего металлургам нужно машинное обучение? 2021 (~9 минут);
▫️ Про внедрение ИИ в сталелитейную компанию и борщ, 2024 (~9 минут).
Также подписывайтесь на канал коллег: @r77_ai
Семинар про интерпретацию моделей ML для нефтегазовой отрасли
▫️ 5 марта (среда), 17:00 МСК
▫️ Google Meet→
▫️ Трансляция YouTube→
Выступает: Антон Воскресенский, Founder / CEO Voskresenskii Consulting (@voskresenskiiconsulting)
Тема: Методы интерпретации моделей машинного обучения в нефтегазовой отрасли
Аннотация
На семинаре разберем кейсы интерпретации моделей машинного обучения для нефтегазовой отрасли и инженерии признаков с опорой на экспертные знания. Рассмотрим:
- Модели для прогнозирования временных рядов
- Методы заполнения пропущенных данных
- Подходы к поиску схожих объектов
Каждый метод будет представлен с вводной по предметной области.
Уровень сложности: продвинутый
Ключевые слова: интерпретация моделей ML, прогнозирование временных рядов, каротажные кривые, взаимовлияние скважин, нефтегаз
▫️ 5 марта (среда), 17:00 МСК
▫️ Google Meet→
▫️ Трансляция YouTube→
Выступает: Антон Воскресенский, Founder / CEO Voskresenskii Consulting (@voskresenskiiconsulting)
Тема: Методы интерпретации моделей машинного обучения в нефтегазовой отрасли
Аннотация
На семинаре разберем кейсы интерпретации моделей машинного обучения для нефтегазовой отрасли и инженерии признаков с опорой на экспертные знания. Рассмотрим:
- Модели для прогнозирования временных рядов
- Методы заполнения пропущенных данных
- Подходы к поиску схожих объектов
Каждый метод будет представлен с вводной по предметной области.
Уровень сложности: продвинутый
Ключевые слова: интерпретация моделей ML, прогнозирование временных рядов, каротажные кривые, взаимовлияние скважин, нефтегаз
Запись семинара
Антон Воскресенский (@voskresenskiiconsulting), Методы интерпретации моделей машинного обучения в нефтегазовой отрасли. YouTube | Дзен | RuTube (~1 час 10 минут).
Антон Воскресенский (@voskresenskiiconsulting), Методы интерпретации моделей машинного обучения в нефтегазовой отрасли. YouTube | Дзен | RuTube (~1 час 10 минут).
Созвон о том как и зачем заниматься наукой
▫️ 12 марта (среда), 17:00 МСК
▫️ Google Meet→
Вопросы к обсуждению:
▫️ Как выбрать тему для исследований? Какая задача подойдет для начала? Начинать ли с небольших и технических задач, или сразу строить стратегические планы по решению крупных научных проблем? Как понять, что выбранная задача по силам, и что делать, если продвижения замедлились. Как эффективнее всего освоить ключевые классические результаты в выбранной области, и как следить за свежими результатами и развитием исследований по своей теме?
▫️ Зачем писать статьи? Как понять, что полученный результат достоин публикации? Как выбрать научный журнал для публикации? Как писать научные тексты, чем в целом этот жанр отличается от других? На что обратить внимание при написании курсовой/диплома/диссертации/…? Какие еще есть способы участия в жизни научного сообщества: конференции, коллаборации, рецензирование, …?
▫️ Зачем идти в аспирантуру, писать диссертацию и получать учёную степень? Зачем вообще заниматься наукой? Какие могут быть варианты развития карьеры в науке? Какие есть особенности финансирования и как работать с системой грантов?
▫️ 12 марта (среда), 17:00 МСК
▫️ Google Meet→
Вопросы к обсуждению:
▫️ Как выбрать тему для исследований? Какая задача подойдет для начала? Начинать ли с небольших и технических задач, или сразу строить стратегические планы по решению крупных научных проблем? Как понять, что выбранная задача по силам, и что делать, если продвижения замедлились. Как эффективнее всего освоить ключевые классические результаты в выбранной области, и как следить за свежими результатами и развитием исследований по своей теме?
▫️ Зачем писать статьи? Как понять, что полученный результат достоин публикации? Как выбрать научный журнал для публикации? Как писать научные тексты, чем в целом этот жанр отличается от других? На что обратить внимание при написании курсовой/диплома/диссертации/…? Какие еще есть способы участия в жизни научного сообщества: конференции, коллаборации, рецензирование, …?
▫️ Зачем идти в аспирантуру, писать диссертацию и получать учёную степень? Зачем вообще заниматься наукой? Какие могут быть варианты развития карьеры в науке? Какие есть особенности финансирования и как работать с системой грантов?
Запись созвона
Как и зачем заниматься наукой? YouTube | Дзен | RuTube (~1 час 40 минут)
В дискуссии принимали участие:
▫️ Иван Чижов (ВМК МГУ)
▫️ Вадим Порватов (Сбербанк)
▫️ Никита Олехно (ИТМО)
▫️ Екатерина Строева (ВМК МГУ)
▫️ Александр Гавриков (Т-Банк)
▫️ Григорий Карпунин (КриптоПро)
▫️ Павел Снурницын (ВМК МГУ, GlowByte)
Как и зачем заниматься наукой? YouTube | Дзен | RuTube (~1 час 40 минут)
В дискуссии принимали участие:
▫️ Иван Чижов (ВМК МГУ)
▫️ Вадим Порватов (Сбербанк)
▫️ Никита Олехно (ИТМО)
▫️ Екатерина Строева (ВМК МГУ)
▫️ Александр Гавриков (Т-Банк)
▫️ Григорий Карпунин (КриптоПро)
▫️ Павел Снурницын (ВМК МГУ, GlowByte)
Семинар про теорию игр и покер
▫️ 19 марта (среда), 17:00 МСК
▫️ Google Meet→
▫️ Трансляция YouTube→
Выступает: Олег Остроумов
Тема: Алгоритмы и солвер для покера
Аннотация
В докладе расскажу:
— Как я перешёл от профессиональной игры в покер к созданию солвера для покера, и помог моим клиентам стать лучшими игроками в мире.
— Как работает алгоритм Counterfactual Regret Minimization для вычисления равновесия Нэша в покере.
— Что на самом деле означает блеф в покере и как рассчитать оптимальную частоту блефа.
— Как помочь игрокам изучить и понять оптимальную стратегию, ведь массив из 80 ГБ чисел запомнить нельзя.
— Как я продавал свой продукт игрокам, которые изначально сомневались в его точности.
Уровень сложности: продвинутый, для понимания доклада требуется знакомство с теорией игр.
Ключевые слова: Poker, Extensive form game, Imperfect information game, Nash Equilibrium, (Monte-Carlo) Counterfactual Regret Minimization.
▫️ 19 марта (среда), 17:00 МСК
▫️ Google Meet→
▫️ Трансляция YouTube→
Выступает: Олег Остроумов
Тема: Алгоритмы и солвер для покера
Аннотация
В докладе расскажу:
— Как я перешёл от профессиональной игры в покер к созданию солвера для покера, и помог моим клиентам стать лучшими игроками в мире.
— Как работает алгоритм Counterfactual Regret Minimization для вычисления равновесия Нэша в покере.
— Что на самом деле означает блеф в покере и как рассчитать оптимальную частоту блефа.
— Как помочь игрокам изучить и понять оптимальную стратегию, ведь массив из 80 ГБ чисел запомнить нельзя.
— Как я продавал свой продукт игрокам, которые изначально сомневались в его точности.
Уровень сложности: продвинутый, для понимания доклада требуется знакомство с теорией игр.
Ключевые слова: Poker, Extensive form game, Imperfect information game, Nash Equilibrium, (Monte-Carlo) Counterfactual Regret Minimization.
Запись семинара
Олег Остроумов (@oleg_ostroumov), Алгоритмы и солвер для покера. YouTube | Дзен | RuTube (~1 час 20 минут).
Олег Остроумов (@oleg_ostroumov), Алгоритмы и солвер для покера. YouTube | Дзен | RuTube (~1 час 20 минут).
Созвон про LLM
▫️ 26 марта (среда), 17:00 МСК
▫️ Google Meet→
Тема: LLM для бизнеса 2 года спустя
Вопросы к обсуждению:
— Какие есть реальные кейсы и бизнес задачи, решение которых опирается на LLM?
— Есть ли примеры неудачного внедрения технологии и какие уроки можно из них извлечь?
— В каких индустриях и направлениях уже есть стандартные бизнес-кейсы приложений LLM, а где технология только набирает обороты?
— Какие организационные и технические особенности необходимо учесть при реализации проектов на базе LLM в крупных компаниях?
— Как крупные компании оценивают ROI от внедрения LLM?
— В каких случаях кастомизация и тюнинг моделей имеет преимущество по сравнению с использованием готовых сервисов?
— Имеет ли смысл начинать проекты с LLM если ресурсы GPU ограничены?
— Почему Gartnet пишет про тренд Small Language Models?
— Как сейчас решаются вопросы безопасности и конфиденциальности данных при использовании LLM?
— Где грань между полной автоматизацией процессов и необходимостью участия человека?
— Может ли LLM стать основой для создания полностью автономных бизнес-процессов?
— Какой новый функционал может радикально изменить подход к использованию LLM в будущем?
▫️ 26 марта (среда), 17:00 МСК
▫️ Google Meet→
Тема: LLM для бизнеса 2 года спустя
Вопросы к обсуждению:
— Какие есть реальные кейсы и бизнес задачи, решение которых опирается на LLM?
— Есть ли примеры неудачного внедрения технологии и какие уроки можно из них извлечь?
— В каких индустриях и направлениях уже есть стандартные бизнес-кейсы приложений LLM, а где технология только набирает обороты?
— Какие организационные и технические особенности необходимо учесть при реализации проектов на базе LLM в крупных компаниях?
— Как крупные компании оценивают ROI от внедрения LLM?
— В каких случаях кастомизация и тюнинг моделей имеет преимущество по сравнению с использованием готовых сервисов?
— Имеет ли смысл начинать проекты с LLM если ресурсы GPU ограничены?
— Почему Gartnet пишет про тренд Small Language Models?
— Как сейчас решаются вопросы безопасности и конфиденциальности данных при использовании LLM?
— Где грань между полной автоматизацией процессов и необходимостью участия человека?
— Может ли LLM стать основой для создания полностью автономных бизнес-процессов?
— Какой новый функционал может радикально изменить подход к использованию LLM в будущем?
Запись созвона
LLM для бизнеса 2 года спустя. YouTube | Дзен | RuTube (~1 час 25 минут).
В дискуссии принимали участие:
▫️ Михаил Зайцев (GlowByte)
▫️ Кирилл Блохнин (GlowByte)
▫️ Илья Усов (bimlib.pro)
▫️ Егор Шишковец (Честный Знак)
▫️ Семён Ким
▫️ Павел Снурницын
LLM для бизнеса 2 года спустя. YouTube | Дзен | RuTube (~1 час 25 минут).
В дискуссии принимали участие:
▫️ Михаил Зайцев (GlowByte)
▫️ Кирилл Блохнин (GlowByte)
▫️ Илья Усов (bimlib.pro)
▫️ Егор Шишковец (Честный Знак)
▫️ Семён Ким
▫️ Павел Снурницын
Мероприятия NoML в апреле
План мероприятий на ближайший месяц, место и время те же: онлайн по средам в 17:00 МСК:
▫️ 02.04 | семинар | Дмитрий Штукенберг (ИТМО), Теория типов и некоторые её применения;
▫️ 09.04 | семинар | Байрам Аннаков (Onsa), AI агенты: что это такое, что уже возможно, и что ожидать в будущем?;
▫️ 16.04 | семинар | Виталий Черненко (Амальгама), Имитационное моделирование: планирование и поддержка принятия решений на реальных примерах;
▫️ 23.04 | созвон | Тренды Data & Analytics 2025;
Следите за обновлениями в канале @noml_digest и чате @noml_community, там же публикуются детали предстоящих докладов и ссылки для подключения.
План мероприятий на ближайший месяц, место и время те же: онлайн по средам в 17:00 МСК:
▫️ 02.04 | семинар | Дмитрий Штукенберг (ИТМО), Теория типов и некоторые её применения;
▫️ 09.04 | семинар | Байрам Аннаков (Onsa), AI агенты: что это такое, что уже возможно, и что ожидать в будущем?;
▫️ 16.04 | семинар | Виталий Черненко (Амальгама), Имитационное моделирование: планирование и поддержка принятия решений на реальных примерах;
▫️ 23.04 | созвон | Тренды Data & Analytics 2025;
Следите за обновлениями в канале @noml_digest и чате @noml_community, там же публикуются детали предстоящих докладов и ссылки для подключения.
Семинар про теорию типов
▫️ 2 апреля (среда), 17:00 МСК
▫️ Google Meet→
▫️ Трансляция YouTube→
Выступает: Дмитрий Штукенберг (Университет ИТМО)
Тема: Теория типов и некоторые её применения
Аннотация
Данная встреча будет посвящена теории типов: области информатики, пограничной между математической логикой и программированием. Эта область связана с использованием изоморфизма Карри-Ховарда, предлагающего рассматривать типы значений как логические утверждения, а сами значения - как доказательства этих утверждений.
Подход имеет многочисленные применения - как в вопросах, полезных для программирования (например, он важен для дизайна языков программирования), так и в математике (дополнительные подходы к формализации математических утверждений и теорий).
На встрече мы обсудим как теоретическую составляющую, так и конкретные практические применения.
Уровень сложности: начинающий, каких-то специальных знаний для понимания материала встречи не требуется, должно быть достаточно общей математической эрудиции.
Ключевые слова: математическая логика, теория типов, изоморфизм Карри-Ховарда.
▫️ 2 апреля (среда), 17:00 МСК
▫️ Google Meet→
▫️ Трансляция YouTube→
Выступает: Дмитрий Штукенберг (Университет ИТМО)
Тема: Теория типов и некоторые её применения
Аннотация
Данная встреча будет посвящена теории типов: области информатики, пограничной между математической логикой и программированием. Эта область связана с использованием изоморфизма Карри-Ховарда, предлагающего рассматривать типы значений как логические утверждения, а сами значения - как доказательства этих утверждений.
Подход имеет многочисленные применения - как в вопросах, полезных для программирования (например, он важен для дизайна языков программирования), так и в математике (дополнительные подходы к формализации математических утверждений и теорий).
На встрече мы обсудим как теоретическую составляющую, так и конкретные практические применения.
Уровень сложности: начинающий, каких-то специальных знаний для понимания материала встречи не требуется, должно быть достаточно общей математической эрудиции.
Ключевые слова: математическая логика, теория типов, изоморфизм Карри-Ховарда.
Про теорию типов
В завершение темы прошлой недели подборка материалов от Дмитрия Штукенберга.
Введение в основания математики
▫️ S.C. Kleene, Introduction to Metamathematics, 1952 (перевод: С.К. Клини, Введение в метаматематику, 1957) (~550 стр.)
Теория типов
▫️ Хорошее введение в тему: интуиционисткая логика, изоморфизм Карри-Ховарда, линейная логика и как всё это связано с функциональным программированием: P. Wadler, A Taste of linear Logic, 1993 (27 стр.)
▫️ Здесь в целом про конструктивную математику для программирования: P. Martin-Löf, Constructive mathematics and computer programming, 1982 (23 стр.)
▫️ Гомотопическая теория типов (HoTT) и вообще один из современных взглядов в сторону оснований математики, плюс в первой главе хорошее введение в целом в теорию типов: Homotopy Type Theory: Univalent Foundations of Mathematics, 2013 (перевод) (475 стр.)
На ресурсе homotopytypetheory.org можно найти много других материалов про HoTT.
Языки и инструменты
▫️ Coq / Rocq
Плюс учебник: A. Chipala, Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant, 2013–2019 (~400 стр.)
▫️ Agda
▫️ F* (F star)
▫️ Arend
И список библиотек и расширений на базе HoTT
Пара интересных приложений
▫️ Задача о четырёх красках: G. Gonthier, A computer-checked proof of the Four Colour Theorem, 2005 (57 стр.)
▫️ Верификатор для Solidity: coq-of-solidity
В завершение темы прошлой недели подборка материалов от Дмитрия Штукенберга.
Введение в основания математики
▫️ S.C. Kleene, Introduction to Metamathematics, 1952 (перевод: С.К. Клини, Введение в метаматематику, 1957) (~550 стр.)
Теория типов
▫️ Хорошее введение в тему: интуиционисткая логика, изоморфизм Карри-Ховарда, линейная логика и как всё это связано с функциональным программированием: P. Wadler, A Taste of linear Logic, 1993 (27 стр.)
▫️ Здесь в целом про конструктивную математику для программирования: P. Martin-Löf, Constructive mathematics and computer programming, 1982 (23 стр.)
▫️ Гомотопическая теория типов (HoTT) и вообще один из современных взглядов в сторону оснований математики, плюс в первой главе хорошее введение в целом в теорию типов: Homotopy Type Theory: Univalent Foundations of Mathematics, 2013 (перевод) (475 стр.)
На ресурсе homotopytypetheory.org можно найти много других материалов про HoTT.
Языки и инструменты
▫️ Coq / Rocq
Плюс учебник: A. Chipala, Certified Programming with Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant, 2013–2019 (~400 стр.)
▫️ Agda
▫️ F* (F star)
▫️ Arend
И список библиотек и расширений на базе HoTT
Пара интересных приложений
▫️ Задача о четырёх красках: G. Gonthier, A computer-checked proof of the Four Colour Theorem, 2005 (57 стр.)
▫️ Верификатор для Solidity: coq-of-solidity