The Circuit Size Hierarchy CSH$^a_b$ states that if $a > b \geq 1$ then the set of functions on $n$ variables computed by Boolean circuits of size $n^a$ is strictly larger than the set of functions computed by circuits of size $n^b$. This result, which is a cornerstone of circuit complexity theory, follows from the non-constructive proof of the existence of functions of large circuit complexity obtained by Shannon in 1949.

Are there more "constructive" proofs of the Circuit Size Hierarchy? Can we quantify this? Motivated by these questions, we investigate the provability of CSH$^a_b$ in theories of bounded arithmetic. Among other contributions, we establish the following results:

(1) Given any $a > b > 1$, CSH$^a_b$ is provable in Buss's theory T$^2_2$.

(2) In contrast, if there are constants $a > b > 1$ such that CSH$^a_b$ is provable in the theory T$^1_2$, then there is a constant $\varepsilon
> 0$ such that $P^{NP}$ requires non-uniform circuits of size $n^{1 + \varepsilon}$.

In other words, an improved upper bound on the proof complexity of CSH$^a_b$ would lead to new lower bounds in complexity theory.

We complement these results with a proof of the Formula Size Hierarchy (FSH$^a_b$) in PV$_1$ with parameters $a > 2$ and $b = 3/2$. This is in contrast with typical formalizations of complexity lower bounds in bounded arithmetic, which require APC$_1$ or stronger theories and are not known to hold even in T$^1_2$.