'<<
When a long computer calculation is an important part of the proof of
a mathematical theorem, we should ask for proof (preferably both
computer-checked and hand checked) that the program does the
advertised calculation. For example, we want a proof that if the
calculation comes out, the four color conjecture is true.
>>

This is of course desirable, but brings up a new question: where does this stop?

A typical "verification of correctness" of a sizeable computer program involves the application of another program. Then we need to know that the verification program is valid and was used properly. Etc.'

I think that the main problem with computer proves is proving the exhaustion of all possible cases. With some problems, e.g. Ramsey Theory on small graphs, this is possible and proofs are acceptable and accepted. With problems that do not fall into simple enumeration patterns, e.g. the four colour conjecture and Kepler's conjecture, the basic axiom of truth is that a deterministic model such as the computer is incapable of such a proof, in the same way proving the primality of numbers with 10^100 digits will remain out of deterministic computing's reach for eternity.