Hanlin Ren, a researcher at the Institute for Advanced Study, opens a two-part seminar asking why proving even modest complexity lower bounds, let alone P versus NP, has proven so resistant to decades of effort. His claim is that the obstacle is not just missing combinatorial tricks but the logical strength of the axioms available to prove such results. Ren reworks classical lower bounds through bounded arithmetic, showing that Maass's 1984 result that one-tape Turing machines need quadratic time to recognize palindromes is logically equivalent to the weak pigeonhole principle over the feasible reasoning system PV. He then turns to Resolution proof systems, arguing that a specific threshold of logical strength is required to prove hardness there regardless of which hard tautology is chosen. Delivered as part of the Computer Science/Discrete Mathematics Seminar II at IAS, the talk draws on recent papers by Chen, Li and Oliveira and by Korten, and assumes no prior background in bounded arithmetic.