> Basically I'm talking about the subset of proofs that could be done with pen and paper and pass a careful refereeing process. And you got that interpretation in your reply. You say that it is not insightful and that is of course an opinion you are entitled to.
Well, that part was me being subjective, but the objective part is that this subset of proofs doesn't necessarily have a verification algorithm "in NP." A very short proof that took time doubly exponential (in some sense) in the size of the proof could still feasibly be solved with pen and paper, because the proof was short even though the verification time was very long (or the verification was long due to a technicality--I describe an example below), depending on the exponent and the proof size. While at the same time, a short proof that took time polynomial (in some sense) in the size of the proof could take longer than the age of the universe to verify and be out of reach for both humans and computers, depending again on the degree of the polynomial and the proof size (and, since again proof verification in CiC is not reducible to 3SAT, proof search that incorporates non-polynomial functions plausibly might not even benefit from any speedup if P = NP!). I say "in some sense" because it's unclear exactly what function f to fix, since pretty much any decidable, total function you can think of grows more slowly than "max steps needed to typecheck a term of length n in CiC" (outside of other meta-level functions that similarly don't provide practical bounds on running time).
(To give a concrete example of where human verification might be much faster than computer verification of the same step, human mathematicians can easily use "tricks" when they know two results will be the same, without actually proving them equivalent, modifying the proof, or imparting extra knowledge to a verifier. For example, in Coq, by default you use Peano naturals, which are convenient for proofs but have very poor complexity--which means exponentiation actually takes exponential time to compute with them. Humans verifying a proof step will recognize this and just do exponentiation the normal way regardless of which inductive definition of naturals is being used, while for a computer to do so the person writing the proof has to deliberately switch out Peano naturals for digital naturals. It is entirely possible that the proof size when using non-Peano nats will be larger than the proof size using Peano nats, since induction on non-Peano nats is much more tedious, while the verification time is exponentially lower using non-Peano nats! So this is an example where proof search for a short proof and proof search for a fast to verify proof may be in conflict. It's also an example of somewhere where even though it's not explicitly stated in the proof, and even though different formulations of nats can't exactly be proved "fully equivalent" in CiC, humans verifying a proof understand that "in spirit" it doesn't really matter whether you use Peano nats or not.
Indeed, if you work with formal verification a lot, you will find you spend significant amounts of time optimizing your proofs, and learning tricks like whether to make an input to an inductive definition indexed or parametric, which are things that human mathematicians don't care about at all but which are very significant to the machine verifier).
In other words, I don't think being practical to verify can be described completely by either the complexity of verification or the size of the proof, and I don't think it's that useful to conflate this with a problem being in NP since (1) CiC proof synthesis isn't actually in NP, or even in the polynomial hierarchy, and (2) being in NP has a much more precise technical definition that only somewhat overlaps with "practical to verify."
Well, that part was me being subjective, but the objective part is that this subset of proofs doesn't necessarily have a verification algorithm "in NP." A very short proof that took time doubly exponential (in some sense) in the size of the proof could still feasibly be solved with pen and paper, because the proof was short even though the verification time was very long (or the verification was long due to a technicality--I describe an example below), depending on the exponent and the proof size. While at the same time, a short proof that took time polynomial (in some sense) in the size of the proof could take longer than the age of the universe to verify and be out of reach for both humans and computers, depending again on the degree of the polynomial and the proof size (and, since again proof verification in CiC is not reducible to 3SAT, proof search that incorporates non-polynomial functions plausibly might not even benefit from any speedup if P = NP!). I say "in some sense" because it's unclear exactly what function f to fix, since pretty much any decidable, total function you can think of grows more slowly than "max steps needed to typecheck a term of length n in CiC" (outside of other meta-level functions that similarly don't provide practical bounds on running time).
(To give a concrete example of where human verification might be much faster than computer verification of the same step, human mathematicians can easily use "tricks" when they know two results will be the same, without actually proving them equivalent, modifying the proof, or imparting extra knowledge to a verifier. For example, in Coq, by default you use Peano naturals, which are convenient for proofs but have very poor complexity--which means exponentiation actually takes exponential time to compute with them. Humans verifying a proof step will recognize this and just do exponentiation the normal way regardless of which inductive definition of naturals is being used, while for a computer to do so the person writing the proof has to deliberately switch out Peano naturals for digital naturals. It is entirely possible that the proof size when using non-Peano nats will be larger than the proof size using Peano nats, since induction on non-Peano nats is much more tedious, while the verification time is exponentially lower using non-Peano nats! So this is an example where proof search for a short proof and proof search for a fast to verify proof may be in conflict. It's also an example of somewhere where even though it's not explicitly stated in the proof, and even though different formulations of nats can't exactly be proved "fully equivalent" in CiC, humans verifying a proof understand that "in spirit" it doesn't really matter whether you use Peano nats or not.
Indeed, if you work with formal verification a lot, you will find you spend significant amounts of time optimizing your proofs, and learning tricks like whether to make an input to an inductive definition indexed or parametric, which are things that human mathematicians don't care about at all but which are very significant to the machine verifier).
In other words, I don't think being practical to verify can be described completely by either the complexity of verification or the size of the proof, and I don't think it's that useful to conflate this with a problem being in NP since (1) CiC proof synthesis isn't actually in NP, or even in the polynomial hierarchy, and (2) being in NP has a much more precise technical definition that only somewhat overlaps with "practical to verify."