I will talk about the broad field of proof complexity. Its central question is whether there exists an NP algorithm certifying that a Boolean formula is unsatisfiable. Or, put differently, whether there exists a propositional
proof system P in which every unsatisfiable formula has a short refutation. The expected answer is ”no”, but this can be unconditionally proved only for relatively weak systems P, such as Resolution, Cutting Planes, or bounded-depth Frege. I will overview techniques used in the area, as well as focus on open problems.