Hard Theorems

'Cause when the proof gets tough… the tough get provin' (…proof complexity lower bounds!)