That's only obvious in a vacuous sense.

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.

Well, I've spent a lot of time with theorem provers as well as with normal mathematics. I've never experienced an exponential blowup when formalizing mathematical ideas. It would always boild down to step-by-step verification. And I don't see any reason to suspect that the paper under discussion uses non-standard techniques.

Wow, this got more replies than I expected. I was partly kidding, in that I don’t think it’s a huge concern for humans, but for example the tableau decision procedure[1] for modal logics such as epistemic logic is EXPTIME-complete[2].

[1]: https://en.wikipedia.org/wiki/Method_of_analytic_tableaux

[2]: https://arxiv.org/abs/0808.4133