Theorem provers work like this: the axioms are input, then there is a program (using libraries) that transforms them, and the output of that program is the theo

Theorem provers work like this: the axioms are input, then there is a program (using libraries) that transforms them, and the output of that program is the theorem. If the runtime is correctly executing the program, then the theorem is proven from the axioms. Importantly, as long as there is any program that outputs the theorem from the axioms, you have a proof. So even if your program doesn't do what you think it does, if it outputs the theorem, that doesn't matter. So do you trust the runtime? Bit flip errors can be eliminated by running things multiple times. The more human proven statements the runtime executes correctly the more you believe it's implemented correctly. Importantly, all proofs done in lean increase the trust in the common runtime. And: do you trust your ability to understand the formal theorem that is output. That's the question discussed elsewhere in this comment section in depth.