The proof is a sequence of extremely easy logical inference rules like if A=>B and A then B. You check the correctness of the proof by verifying that these rules are applied correctly. Obviously though, there is no way to prove that your mathematical model corresponds to reality. That is because mathematics is not concerned with reality.
What if you make a mistake in checking the proof? Sure, that may sound silly, but mistakes are the point at issue here.
The usual rejoinder is that you can use an automated proof checker/assistant like COQ. Now you're relying on a program. Is the program correct? Well, we checked it with itself...
I admit this is far better than not having a proof at all. As I said, it's a tool, and has pragmatic merit. My objection is it's not absolute proof - which is what "proof" sounds like to me. In reality, a proof is an argument for the truth of a claim, with a level of convincingness.
BTW: Admittedly, reducing a proof to simple rules makes it harder to get wrong, though this is rarely done by mathematicians. Also, it's a curious fact that some mathematicians have made mistakes in their proofs, but turned out to be right anyway, presumably because they could see that it was true, and the notation was secondary.
Proving theorems in mathematics plays a bit different role than proving correctness of programs. In mathematics, it's about sharing ideas, so if the proof is not completely correct, it can still be interesting because of the ideas and methods it uses. When you prove correctness of programs though, the whole point is to be sure that the program is correct, so the actual proof is important here, not its method or structure, because it's usually clear why the program at hand works.
If you make a mistake in checking the proof, the the proof is incorrect. The problem is with your application of the mathematics, not the applicability of mathematics itself to the problem of showing the truth of things.
