Thanks for the pointer. I already had Avigad’s paper open on my computer, but I haven’t read it yet.

I take the point about the output – as opposed to the process – being “close to worthless”; though I suspect it’s only a matter of time before some result whose correctness ‘was never in doubt’ is found to be incorrect as a consequence of an attempt to formalize it.