#матлог #учёба #семинар #не_мехмат #ВШЭ

Уважаемые коллеги, приглашаем вас принять участие в заседании научного семинара "Современные проблемы математической логики" в ВШЭ.

Семинар пройдет ОНЛАЙН! В аудитории 110 (ул. Усачева, д. 6) будет организована трансляция.
Если вам нужна ссылка или пропуск в здание матфака, пишите на почту kudinov.andrey@gmail.com.

Дата и время: 05.06.2026 в 16:20

Докладчик: Игорь Почепчов

Название доклада: Формальные доказательства — Lean как инфраструктура исследований

Аннотация:
Один из самых интересных сдвигов последних лет в математике — превращение Lean из нишевого инструмента в реальную инфраструктуру исследований. Lean — это интерактивный пруфассистент: язык программирования, в котором доказательство проверяется до уровня аксиом, и если код скомпилировался — теорема верна.
За два года в области произошёл качественный скачок. Полиномиальная гипотеза Фреймана–Рузы (Тао, Гауэрс, Грин, Манерс) была формализована за 23 дня силами Blueprint-проекта. AlphaProof от DeepMind взял серебро IMO 2024, доказывая задачи на Lean — все шаги верифицированы компилятором.
На докладе разберём, что такое Lean, посмотрим на примеры исследований с его использованием и обсудим идею автоматической формализации научных статей.