I'm referring to producing the certificate as the time-consuming part, not the verification time (I disagree that verification is not subtle, but I suppose that

I'm referring to producing the certificate as the time-consuming part, not the verification time (I disagree that verification is not subtle, but I suppose that doesn't matter as there are verified verifiers). For example, many SAT solvers no longer attempt to provide "pure" resolution proofs because they are too expensive to produce, which restricts the kinds of techniques you see used in competition. In fact, producing certificates efficiently is an active research area, which wouldn't be the case if certificate production had negligible cost, e.g. see https://lmcs.episciences.org/9357/pdf https://lmcs.episciences.org/9357/pdf.