# short proof

## F_d versus F_{d+1} ★★★

Author(s): Krajicek

\begin{problem} Find a constant $k$ such that for any $d$ there is a sequence of tautologies of depth $k$ that have polynomial (or quasi-polynomial) size proofs in depth $d+1$ Frege system $F_{d+1}$ but requires exponential size $F_d$ proofs. \end{problem}

Keywords: Frege system; short proof