Курс будет посвящён оценкам длины доказательств в первую очередь для утверждений логики высказываний, хотя будут рассмотрены и другие языки. Существование системы, в которой есть доказательство полиномиальной длины для каждой тавтологии, эквивалентно (неправдоподобному) утверждению NP = co-NP. Однако на констатации этого факта вопросы не заканчиваются: даже если такой системы нет, есть ли оптимальная система с самыми короткими доказательствами? Для каких систем мы можем доказать экспоненциальные нижние оценки на длину доказательств? Как длины доказательств связаны со сложностью вычислительных задач? Подобным вопросам и будет посвящён этот курс.