We show that every language in NP has a probabilistically checkable proof of
proximity (i.e., proofs asserting that an instance is ``close'' to a member of
the language), where the verifier's running time is polylogarithmic in the input
size and the length of the probabilistically checkable proof is only
polylogarithmically larger that the length of the classical proof. (Such a
verifier can only query polylogarithmically many bits of the input instance and
the proof. Thus it needs oracle access to the input as well as the proof, and
cannot guarantee that the input is in the language --- only that it is close to
some string in the language. If the verifier is restricted further in its
query complexity and only allowed q queries, then the proof size blows up by a
factor of 2^{(log n)^{c/q}} where the constant c depends only on the language
(and is independent of q). Our results thus give efficient (in the sense of
running time) versions of the shortest known PCPs, due to Ben-Sasson et al. (STOC
'04) and Ben-Sasson and Sudan (STOC '05), respectively. The time
complexity of the verifier and the size of the proof were the original emphases
in the definition of holographic proofs, due to Babai et al. (STOC '91), and our
work is the first to return to these emphases since their work.
Of technical interest in our proof is a new complete problem for NEXP based on
constraint satisfaction problems with very low complexity constraints, and
techniques to arithmetize such constraints over fields of small characteristic.