JetBrains Research — наука, меняющая мир

Семинар: Введение в Metamath

Основная идея проекта Metamath - построить формализованное здание математики, которое с одной стороны может быть проверено автоматически на компьютере, а с другой стороны "вручную" разобрано человеком в привычной ему нотации. В определенном смысле это Principia Mathematica. Какие идеи стоят за Metamath?

Если следовать традиции и взять формализованную теорию множеств - ZFC - в качестве оснований математики, то такие основания слабо подходят для заявленной цели. Мы разберем возникающие проблемы как со стороны языка первого порядка, так и со стороны теории множеств. Перечислим предложенные решения возникающих проблем, и что в итоге применяется в Metamath.

Далее будем постепенно отходить от основ и двигаться в сторону все более абстрактных конструкций: отношений, функций, ординалов, "обычных" чисел, структур. Напоследок покажем, как Metamath "справляется" с теорией категорий.

Докладчик: Кирилл Смирнов

7.10.2019, 17:15.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 28