О сложности доказательств

Теория сложности доказательств преимущественно изучает, насколько простыми могут быть формальные доказательства интересных истинных утверждений в различных системах доказательств. Я постараюсь рассказать на простом языке и с различными примерами (доказательства не планируются) о некоторых основных идеях, результатах и открытых вопросах теории сложности доказательств. Особое внимание будет уделено её связям со смежными областями, такими как математическая логика, сложность вычислений, SAT-решатели, комбинаторная оптимизация, элементарная алгебраическая и полуалгебраическая геометрия и т.д.
В качестве сравнительно популярного, но уже более систематического введения, я могу порекомендовать свой обзорный доклад A. Razborov, “Propositional Proof Complexity”, in Proceedings of the 8th European Congress of Mathematics, 439-464, 2023; там же можно найти ссылки для более углублённого изучения.