Looking for reference on NP-Completeness of proofs of length n Given a deductive system $\Lambda$, and some well-formed-formula S, one can ask the question "Is there a proof S in $\Lambda$ of length n?"  If n is presented in base-1 and if all the axioms of $\Lambda$ are polynomial-time verifiable, and if $\Lambda$ is sufficiently powerful to express the verification for some NP-Complete problem like 3-SAT, this problem is known to be NP-Complete.  It requires super-polynomial time if n is not.

I know how to prove this, but I am also sure that somebody else has already proven this.  Can somebody direct me to an existing published reference?
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.