The end result you get out is something like "if the prover n accepts the claim P, then prover 1 also accepts the claim P". In logical terms you can think of it

The end result you get out is something like "if the prover n accepts the claim P, then prover 1 also accepts the claim P". In logical terms you can think of it as a relative consistency proof. In practice, even much simpler theorems would already raise our confidence a lot. E.g., the inference rules of Coq can be stated in a couple of pages of text, but the kernel checker that you need to trust is 14k lines of OCaml. A proof that the checker actually correctly implements the inference rules would already catch the majority of the bugs that happen in practice. Because of Gödel we then can't hope for a proof in Coq that there is no way to use those inference rules to derive False, but that's less of a concern.