Quantifying and understanding the complexity of mathematical proofs is a fundamental question in proof complexity. At the qualitative level, bounded arithmetic formalizes the notion of feasible proofs, where all functions implicit in proofs are from certain complexity classes. For instance, Cook's theory PV (STOC'75) captures proofs using only polynomial-time computable functions. Analogous to the relationship between algorithms and circuits, there is a tight connection between proofs in bounded arithmetic and propositional proofs via the propositional translation: If a statement is provable in a bounded theory (e.g. PV), then the family of propositional formulas formalizing the statement admits polynomial-length propositional proofs in its corresponding propositional proof system (e.g. Extended Frege).

The paper proposes a theory for the quantitative time complexity of arithmetic proofs. For any proof $\pi$ in Cook's theory PV, its time complexity is a function of the input length of the variables in its conclusion, defined as the size of the propositional proofs obtained via a fixed propositional translation. In other words, the time complexity of arithmetic proofs is a uniform counterpart of proposition proof size, which is analogous to computational complexity theory, where the time complexity of algorithms is a uniform counterpart of circuit size.

Our main result is a feasibility hierarchy theorem, which shows that proofs with higher time complexity are strictly more powerful than those with lower time complexity. In other words, one cannot hope to generically reduce the time complexity of proving certain PV equations by writing longer and more complicated PV proofs. This theorem reveals the internal structure of the theory PV, suggesting the existence of a rich theory for the time complexity of proofs. Motivated by the feasibility hierarchy theorem, we propose a new proof complexity conjecture, which implies the unprovability of NP=coNP in Cook's theory PV. This contributes to a recent line of work on the unprovability of complexity conjectures.