#мехмат_студентам #мехмат_аспирантам

Приглашаем студентов, аспирантов и практикующих математиков на новый спецкурс "Алгебра ИИ Lean" о применении ИИ в доказательствах!

С 1 октября по четвергам на 6-ой паре (18:30) в аудитории 1610 ГЗ МГУ.

Спецкурс - о современной работе математика в связке человек - ИИ - формализация, ориентирован на практические занятия, цель спецкурса - наработка навыков и выстраивание рабочего окружения. Лекторы - к.ф.-м.н., PhD А.Ю.Перепечко и П.П.Соколов (ФКН).

Программа:
1. Коммутативная алгебра - алгебры многочленов, идеалы, факторалгебры, локализации, модули, дифференцирования и так далее.
2. Инструменты - ИИ-агенты, навыки, плагины, mcp-серверы (например, zotero для ведения библиографии), aristotle, Lean / blueprint.
3. Рабочие процессы - изучение отдельной статьи с осознанием и попутной переработкой доказательств, обзор результатов по вопросу, (авто)формализация объектов и доказательств, перепроверка теоремы и формализации её формулировки.