Лекция начнется с неформального рассказа про взгляд теоретической информатики на понятие доказательства по мотивам статьи на хабре: https://habrahabr.ru/company/spbau/blog/217215/.

После перерыва мы узнаем, что такое система доказательств для языка, перечислимые языки (для которых существуют системы доказательств), разрешимые языки и поймем, что есть перечислимый язык, который не является разрешимым (задача об остановке алгоритма).