Looking for reference on NP-Completeness of proofs of length n
See this paper: On Godel’s Theorems on Lengths of Proofs II:
Lower Bounds for Recognizing $k$ Symbol Provability by Samuel R. Buss, 1995.


  This paper discusses a claim made by Godel in a letter to von
  Neumann which is closely related to the P versus NP problem.
  Godel’s claim is that $k$-symbol provability in first-order logic can
  not be decided in $o(k)$ time on a deterministic Turing machine.
  We prove Godel’s claim and also prove a conjecture of S. Cook’s
  that this problem can not be decided in $o(k/ \log k)$ time by a
  nondeterministic Turing machine. In addition, we prove that the
  $k$-symbol provability problem is NP-complete, even for provability
  in propositional logic.