[throwawaykeno]

FWIW the answer to all of the questions you ask in the first paragraph is "yes, but come on, that level of skepticism is a waste of time and money". It's like demanding proof that the reviewer wasn't hallucinating when reviewing the paper.

> but having a proof that humans can reason through from beginning to end makes people feel more comfortable.

Saying that humans can't reason about computer-checked proofs is like saying humans can't reason about source code; which is to say, it's obviously false in the general case.