This is perhaps closer to computational complexity than to logic, but there are many open problems in propositional proof complexity that are analogous to, and have close connections to, well-known open problems in computational complexity. For example, it is widely believed that there are tautologies whose proof in a Frege system is necessarily exponential in size; however, so far, no superpolynomial lower bounds have been proven.