#мехмат_студентам #мехмат_аспирантам Приглашаем студентов, аспирантов и практикующих математиков на новый спецкурс "Алгебра ИИ Lean" о применении ИИ в доказательствах! С 1 октября по четвергам на 6-ой паре (18:30) в аудитории 1610 ГЗ МГУ. Спецкурс - о современной работе математика в связке человек - ИИ - формализация, ориентирован на практические занятия, цель спецкурса - наработка навыков и выстраивание рабочего окружения. Лекторы - к.ф.-м.н., PhD А.Ю.Перепечко и П.П.Соколов (ФКН). Программа: 1. Коммутативная алгебра - алгебры многочленов, идеалы, факторалгебры, локализации, модули, дифференцирования и так далее. 2. Инструменты - ИИ-агенты, навыки, плагины, mcp-серверы (например, zotero для ведения библиографии), aristotle, Lean / blueprint. 3. Рабочие процессы - изучение отдельной статьи с осознанием и попутной переработкой доказательств, обзор результатов по вопросу, (авто)формализация объектов и доказательств, перепроверка теоремы и формализации её формулировки.