Complexity of verifying proofs My question can be read on many levels and  so I welcome answers to any reading. The general question is:

What is the computational complexity of verifying a proof?

One way of looking at a computational complexity class (for decision problems) is that is is a set of theories (a theory being a set of theorems) whose theorems can be proven with the resources allotted to the class (any computation of a yes/no by a TM can be viewed as a proof that the answer is yes/no).
Some complexity classes are defined using provability (at least NP), that is, given a proof (a witness or certificate), it can be checked (verified) by some other (strictly smaller) class's machine.
In most proofs of NP-completeness, showing that a problem is actually a member of NP usually is just showing that there is a witness fr any instance that can be verified by a P machine (or, better said, that the verification problem is a member of P).
My question comes from my observation that these verification problems (the one's I remember) seem almost always (I can't remember any others) to be very linear (yes, I'm confounding computational complexity with algorithmic running time).

Are there some verification algorithms that are (provably) polynomial of a higher degree than 1? Or even super-polynomial for EXP, EXP2, etc?
Or in general is the complexity of verification, applied to -any- complexity class, always linear (in P or some smaller class)?

(even though my question is about complexity classes, I am also curious about real life proofs where people may rely on lemmas that involve, for example, proving the existence of a particular intersection of hyperplanes (presumably (!) in some subclass of P)
 A: I will answer your questions in order:
1- The complexity of a proof is the length of the proof. Remember that a proof (witness or certificate) is simply a branch of a Turing machine on some given input. This corresponds to a solution to some problem. For example consider SAT, the input to the machine will be a SAT instance (i.e. a propositional formula), and the proof will be an assignment of 0-1 values to the variables. Some problems can have exponentially long proofs, like PSPACE-complete problems, or proofs of non-existence like in coNP.
2- The second question is not very clear for me. I think you are asking if there can be proofs with super-polynomial lenghts? Like I've said, PSPACE-complete and coNP languages have exponentially long proofs.
3- I don't understand what you mean with linear. You mean that the verifiers are always P machines? Not necessarily, for example, NEXP is also called Exponential-NP. This is because the proofs are verified by deterministic machines that run in exponential time.
In real life, you can consider that all the lines of text that a proof have, can be stated in formal logic, and this can be interpreted by a machine. A field in computational complexity that studies formal proofs is proof complexity. For example, you are given a statement written in some theory (e.g. Peano's arithmetic). Then, you calculated what are the necessary resources a machine needs to verify that the statement is true or not. 
