**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).

3more comments