Comment by cocoto
3 days ago
The way it works is that if you trust the theorem prover to be bug free, then you only have to verify that the theorem was correctly stated in the program. The proof itself becomes irrelevant and there is no need to verify it.
Humans still have to state the goal and write a proof of it, but the proof is computer-verified. It's not irrelevant, except in the sense that any two different ways to prove the same statement are equivalently valid proofs.