Факультативный курс «Формальная верификация и современные ИИ-инструменты исследователя-математика (AI4Math)»
МФТИ — Московский физико-технический институт ·
AI4Math – направление на стыке формальных методов и глубокого обучения, где математическое доказательство становится машинно проверяемым объектом, а языковая модель – рабочим инструментом исследователя. За последние годы системы вроде DeepSeek-Prover, AlphaProof и Aristotle показали, что автоформализация и автоматический поиск доказательств становятся реальным инструментом для решения сложнейших математических задач. Библиотека Mathlib перешагнула миллион строк формализованной математики, а крупные научные группы переводят свои результаты в Lean. Это меняет и саму профессию. Умение записать утверждение как тип, проверить его в ассистенте доказательств и отличить сгенерированный текст от проверенного рассуждения становится базовым навыком – и в академической математике, и в индустрии, где формальная верификация востребована, например, в криптографии, компиляторах, безопасности и ML-инфраструктуре. О курсе Курс даёт теоретические основания и рабочую среду для формальной математики с ИИ-ассистентом. Начинаем с фундамента: соответствие Кэрри-Ховарда, зависимые типы, теория категорий, функциональное программирование, а дальше решение содержательных задач в Lean4: самостоятельно и с агентом. В программе: тактический язык Lean 4 и навигация по Mathlib (LeanSearch, Loogle, exact/apply); индукция и рекурсия; формализация комбинаторики через Finset и Nat.choose; устройство генерации в LLM и типология её ошибок на математике; эмбеддинги, RAG и графы знаний; цикл автоформализации; агентские сценарии и бенчмарки (miniF2F, ProofNet); протокол MCP и сборка собственных инструментов исследователя; воспроизводимость и исследовательский журнал. Сквозной сюжет курса иерархия доверенных источников доказательства: формальное доказательство > верифицируемый эксперимент > независимая сверка > свободный текст модели. Курс сопровождает обязательный ОКТЧ: содержание то же (комбинаторика, теория чисел), но вместо текстового решения студент получает машинно проверяемое доказательство. Для кого Для студентов 1-4 курса ФПМИ. Предварительной подготовки по Lean или машинному обучению не требуется, всё необходимое будем разбирать с нуля. Курс особенно полезен тем, кто сейчас проходит ОКТЧ: задачи из листков курса используются как рабочий материал для формализации. Тем, кто уже знаком с функциональным программированием или ассистентами доказательств, курс даст исследовательскую рамку и практику работы с ИИ-агентами. Преподаватели Атаева Ольга Муратовна - кандидат наук, старший научный сотрудник ВЦ им. А. А. Дородницына ФИЦ ИУ РАН. Руководитель лаборатории SciLib ФИЦ ИУ РАН. Научные интересы: онтологии, системное программирование и базы данных. Халов Андрей Петрович - аспирант ФПМИ МФТИ, кафедра Интеллектуальных систем и исследователь лаборатории SciLib ФИЦ ИУ РАН. Научные интересы: формальная верификация, графы знаний, нейро-символический ИИ. Расписание Курс начинается 8 сентября. Занятия будут проходить в КВАНТ 202 по вторникам, в 20:05. 15 лекционных пар по 90 минут, одна пара в неделю, осенний семестр (сентябрь—декабрь). Дополнительная информация По всем вопросам можно обращаться к Андрею Халову: khalov.a@phystech.edu, @andreykhalov Где продолжить обучение Продолжить работу по направлению можно на кафедре интеллектуальных систем ФПМИ и в лаборатории SciLib ФИЦ ИУ РАН. В основе работы лаборатории лежат исследования по онтологическому моделированию, графам знаний и нейро-символическим методам, включая графовые методы кодирования поведения агентов ИИ. Студенты курса могут подключиться к текущим проектам лаборатории и продолжить тему курсового проекта как научную работу.
AI4Math – направление на стыке формальных методов и глубокого обучения, где математическое доказательство становится машинно проверяемым объектом, а языковая модель – рабочим инструментом исследователя. За последние годы системы вроде DeepSeek-Prover, AlphaProof и Aristotle показали, что автоформализация и автоматический поиск доказательств становятся реальным инструментом для решения сложнейших математических задач. Библиотека Mathlib перешагнула миллион строк формализованной математики, а крупные научные группы переводят свои результаты в Lean. Это меняет и саму профессию. Умение записать утверждение как тип, проверить его в ассистенте доказательств и отличить сгенерированный текст от проверенного рассуждения становится базовым навыком – и в академической математике, и в индустрии, где формальная верификация востребована, например, в криптографии, компиляторах, безопасности и ML-инфраструктуре. О курсе Курс даёт теоретические основания и рабочую среду для формальной математики с ИИ-ассистентом. Начинаем с фундамента: соответствие Кэрри-Ховарда, зависимые типы, теория категорий, функциональное программирование, а дальше решение содержательных задач в Lean4: самостоятельно и с агентом. В программе: тактический язык Lean 4 и навигация по Mathlib (LeanSearch, Loogle, exact/apply); индукция и рекурсия; формализация комбинаторики через Finset и Nat.choose; устройство генерации в LLM и типология её ошибок на математике; эмбеддинги, RAG и графы знаний; цикл автоформализации; агентские сценарии и бенчмарки (miniF2F, ProofNet); протокол MCP и сборка собственных инструментов исследователя; воспроизводимость и исследовательский журнал. Сквозной сюжет курса иерархия доверенных источников доказательства: формальное доказательство > верифицируемый эксперимент > независимая сверка > свободный текст модели. Курс сопровождает обязательный ОКТЧ: содержание то же (комбинаторика, теория чисел), но вместо текстового решения студент получает машинно проверяемое доказательство. Для кого Для студентов 1-4 курса ФПМИ. Предварительной подготовки по Lean или машинному обучению не требуется, всё необходимое будем разбирать с нуля. Курс особенно полезен тем, кто сейчас проходит ОКТЧ: задачи из листков курса используются как рабочий материал для формализации. Тем, кто уже знаком с функциональным программированием или ассистентами доказательств, курс даст исследовательскую рамку и практику работы с ИИ-агентами. Преподаватели Атаева Ольга Муратовна - кандидат наук, старший научный сотрудник ВЦ им. А. А. Дородницына ФИЦ ИУ РАН. Руководитель лаборатории SciLib ФИЦ ИУ РАН. Научные интересы: онтологии, системное программирование и базы данных. Халов Андрей Петрович - аспирант ФПМИ МФТИ, кафедра Интеллектуальных систем и исследователь лаборатории SciLib ФИЦ ИУ РАН. Научные интересы: формальная верификация, графы знаний, нейро-символический ИИ. Расписание Курс начинается 8 сентября. Занятия будут проходить в КВАНТ 202 по вторникам, в 20:05. 15 лекционных пар по 90 минут, одна пара в неделю, осенний семестр (сентябрь—декабрь). Дополнительная информация По всем вопросам можно обращаться к Андрею Халову: khalov.a@phystech.edu, @andreykhalov Где продолжить обучение Продолжить работу по направлению можно на кафедре интеллектуальных систем ФПМИ и в лаборатории SciLib ФИЦ ИУ РАН. В основе работы лаборатории лежат исследования по онтологическому моделированию, графам знаний и нейро-символическим методам, включая графовые методы кодирования поведения агентов ИИ. Студенты курса могут подключиться к текущим проектам лаборатории и продолжить тему курсового проекта как научную работу.