It always seemed to me that the real question here is whether or not we trust mathematics, not computers. After all, if we can prove that theorem provers work correctly, then it follows that the proofs they generate will be correct. Humans write the theorem provers, so that problem is certainly comprehensible.
I haven't read the article, but...
It always seemed to me that the real question here is whether or not we trust mathematics, not computers. After all, if we can prove that theorem provers work correctly, then it follows that the proofs they generate will be correct. Humans write the theorem provers, so that problem is certainly comprehensible.