Спецкурс осеннего семестра 2026/2027

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

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

Лекторы - к.ф.-м.н., PhD А.Ю.Перепечко, П.П.Соколов (ФКН).

Спецкурс "Алгебра ИИ Lean" - о современной работе математика в связке человек - ИИ - формализация. Он ориентирован на практические занятия, цель спецкурса - наработка навыков и выстраивание рабочего окружения. 

Программа:

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

Предполагается, что у слушателей есть предварительные знания по алгебре и знакомство с ИИ-агентами, но все необходимое планируется напомнить. Итог курса - создание исследовательского проекта в LaTeX и Lean.

Поделиться: