With the rise of computer science, questions like ``can we solve a problem?'' got a quantitative counterpart: ``how hard is it to solve a problem?''. Proof complexity deals with the quantitative version of ``can we prove a theorem?'', namely, the question ``how hard is it to prove a theorem?''. The systematic study of the latter question for propositional proof systems started with Cook and Reckhow~\cite{CookReck74,CookReck79}, initiating a line of research which investigates how different proof systems for propositional logic compare with each other with respect to the minimum size needed to prove tautological formulas. A question that had remained open in the classification of Cook and Reckhow is whether cut-free sequent calculus can polynomially simulate resolution, in other words, whether adding atomic cuts to cut-free sequent calculus can super-polynomially decrease the size of proofs. We answer this question negatively, by showing a super-polynomial separation between cut-free sequent calculus as a system for refuting sets of clauses, and resolution. Now, while size is certainly the most well studied, and arguably the most important measure of the complexity of proofs, other complexity measures have emerged, along with a line of study about relations between them, lack of relations thereof, and the inherent impossibility of optimizing two different measures at once. We contribute to this line of research by identifying two new clusters of known proof complexity measures equal up to polynomial and $\log n$ factors. The first cluster contains the logarithm of tree-like resolution size, regularized clause and monomial space, and clause space, ordinary and regularized, in regular and tree-like resolution. Consequently, separating clause or monomial space from the logarithm of tree-like resolution size is equivalent to showing strong trade-offs between clause space and length, and equivalent to showing super-critical trade-offs between clause space and depth. The second cluster contains resolution width, $\Sigma_2$ space (a generalization of clause space to depth-2 Frege systems), ordinary and regularized, and the logarithm of tree-like $R(\log)$ size. As an application, we improve a known size-space trade-off for polynomial calculus with resolution. We further show a quadratic lower bound on tree-like resolution size for formulas refutable in clause space $4$, and introduce a measure intermediate between depth and the logarithm of tree-like resolution size that might be of independent interest. A third contribution of the dissertation is on the topic of automatability, that is the topic of how hard it is to find short proofs of a statement in a proof system. Significantly refining earlier results, Atserias and M{\" u}ller \cite{AtseMull20} showed that the problem of automatability is $\mathsf{NP}$-hard for resolution. Subsequently, this result was extended to stronger proof systems, including cutting planes, Res($k$), and algebraic proof systems. We extend it to bounded-depth Frege, showing that for any $d>0$, depth-$d$ Frege systems are $\mathsf{NP}$-hard to automate.