В докладе будут рассмотрены основные подходы к автоматической проверке (верификации) математических доказательств, актуальность и область применения этих подходов, современное состояние формальной математики и её перспективы; в частности, наиболее популярные сегодня инструменты проверки доказательств. Кроме того, планируется обсудить краеугольные теоремы, определяющие развитие и теоретические пределы систем верификации.
Будет представлена операционная семантика языка, достаточно мощного для выражения произвольных формальных систем с вычислимыми правилами вывода и метатеорем об этих системах, при этом достаточно простого для реализации и теоретического анализа, а также потенциально пригодного для самоверификации.