We investigate the provability of conjectures from complexity theory in theories of bounded arithmetic.
As we will see, this is closely related to the central problems in proof complexity like lower bounds on the lengths of proofs in Frege systems and, in particular, to Razborov's conjecture about Nisan-Wigderson generators which gives us candidate hard tautologies for strong proof systems. Additionally, we will show that quasi-polynomial circuit lower bounds for SAT are unprovable in the theory \(V\).