Algorithmic complexity of formal proof verification? In this question, suppose $S$ is some popular real-world automated proof system that is stronger than or equivalent to Peano Arithmetic.  I would be happy with a positive answer to the following for any such $S$, so please feel free to cherry-pick $S$ to make that easier:
Can the validity of an $S$-proof be verified in time polynomial in the
string-length of the proof?
I've been able to find some work assessing progress in formal proof verification, such as 
http://www.ams.org/journals/notices/200811/tx081101408p.pdf
but not much on the algorithmic complexity of verifying the outputs of various approaches, so I figure I must be looking in the wrong places / using the wrong search terms.  Please, help point me in the right direction!
 A: No, for languages based on Martin-Löf Type Theory
In proof systems based on Martin-Löf Type Theory, including Coq and Agda, proof-checking can involve evaluating arbitrarily complicated (proven-terminating) programs.
As a simple example, we can define a function is_positive : ℕ → Prop that evaluates to True if its argument is positive, and evaluates to False otherwise.  The size of a proof of is_positive is constant (it's just a proof of True when is_positive is given an argument that evaluates to a numeral).  However, it's relatively easy to define an exponentiation function that makes checking a proof of is_positive$2^n$ take time exponential in $n$.  Here is the Coq code:
(** Define a version of [+] which is recursive on the right argument. *)
Fixpoint plusr (n m : nat) {struct m} : nat :=
  match m with
    | 0 => n
    | S m' => S (plusr n m')
  end.
(** Define a version of [*] which is recursive on the right argument. *)
Fixpoint multr (n m : nat) {struct m} : nat :=
  match m with
    | 0 => 0
    | S m' => plusr n (multr n m')
  end.
Fixpoint pow (base exponent : nat) {struct exponent} : nat :=
  match exponent with
    | 0 => 1
    | S e' => multr base (pow base e')
  end.
(** Test [pow] *)
Compute pow 1 2. (* 1 *)
Compute pow 2 3. (* 8 *)
(** Return [True] if a number is [S _], [False] if it is [0] *)
Definition is_positive (n : nat) : Prop :=
  match n with
    | 0 => False
    | S _  => True
  end.
Time Check I : is_positive (pow 2 9). (* 0.09375 *)
Time Check I : is_positive (pow 2 10). (* 0.40625 *)
Time Check I : is_positive (pow 2 11). (* 1.875 *)

Since numbers are stored in unary, by default, in Coq, the proof term I : is_positive (pow 2 n) has $\mathcal O(n)$ nodes.
You could, hypothetically, output evidence of well-typedness.  In the degenerate case, where your well-typedness evidence is just a trace of the execution of the typechecker, you get linear time checking in the length of trace (assuming your trace-encoding isn't eliding expensive details).
I'm uncertain about languages like HOL, which are not based on dependent type theory.  It's plausible that there are some systems where proof-checking is extremely simple, and can't involve any computation.  I would look at Metamath as a likely candidate, even though it's closer to machine-checked proof than automated theorem proving (and I don't know of anyone using it for things outside of pure math).
A: Given that I can cherry-pick the system, consider HOL Light.  In HOL light (and probably in other systems like Isabelle and Coq), the proofs are written in a functional programming language (for HOL Light, it is OCaml).  The formal proof is a program which merely constructs a theorem object.  Part of the proof program are tactics, that is subroutines which apply powerful reasoning to calculate a proof.  These tactics can take a while.  More specifically, since the language the proof is written in is Turing complete there is no upper bound on the algorithmic complexity except that it is computable.  Even some of the built-in tactics check first order validity which is unsolvable, and therefore has no nice upper bound on complexity.
Obviously, in practice, the proofs in proof systems are checkable in a feasible amount of time.
Also, one can modify the proof system to output a lambda term as a proof witness.  This can be checked faster, but I don't know the exact upper bound on running time (it might still be theoretically bad).  An expert could give a better answer to this second point.
A: It of course depends on the proof system, but it's polynomial (actually basically linear) in any reasonable one.  The catch is that (by incompleteness) there's no effective bound on how long the proof might have to be based on the statement of the theorem.
Suppose you've got a proof system where verifying the proof takes triple-exponential time (or whatever) using some Turing machine T.  Then imagine running T on the proof, recording all the execution steps.  The sequence of recorded steps is in a sense a new proof, that can be verified in essentially linear time, though the new proof itself is much longer than the old proof.
