Proof checking in dependent type theory is nonelementary. Of course, this is a completely artificial result with no real world consequences, but that's complexity theory for you...
As a PhD student in Programming Languages, can I request a reference?* Nobody managed to provide one on MathOverflow, and that's the StackExchange for professional mathematicians:
https://mathoverflow.net/q/226966/36016
Of course, your claim is vacuously true, since you can add a trace of all steps of a proof verifier. It's also vacuously true because you can add a dump of the Internet to the proof. Neither thing is insightful.
> what we normally think of as an "honest proof" is a series of steps each of which follows from the previous by application of one of a finite number of axioms or rules of deduction, and such an "honest" proof is thus checkable in linear time by checking each step
Also, for the record: actual formal proofs for (say) standard ZFC are exponentially bigger than anything you want to work with.
EDIT: To clarify, I didn't mean to imply I'm some authority, just to suggest I'm not so obviously* an idiot. Which was maybe stupid anyway.
[1]: https://en.wikipedia.org/wiki/Method_of_analytic_tableaux