About false theorems: we still don't have any. The examples
given were all correct results with incorrect or incomplete proofs.
The Four Color Theorem, the Hard Lefschetz Theorem, and Dehn's
Lemma all turned out to be true. Not only that, the erroneous
proofs were noticed by human mathematicians, not by automated
reasoning systems. I have never encountered a false theorem
that was used as the foundation for other theorems, with
disastrous results. And I don't think anybody else has, either.
There are many imperfections in the mathematical literature,
and some incomplete proofs, but I don't think there are any
substantive errors that affect the integrity of mathematics.
To repeat, Euclid's parallel postulate CANNOT be proved,
yet we had many (false) proofs of it for 2000 years. The whole
of classical mechanics is based on the assumption our space is
euclidean (as opposed to hyperbolic), because no other consistent
geometry was imaginable at that time.
I agree with you that the results were not disastrous, except in
the theory of relativity. Of course, this doesn't affect the
integrity of mathematics, it only effects the integrity of our
ideas of space.
You are also right in saying most of these errors were noticed
by humans, and not machines. This is because logical errors or
missing cases in proofs easy to spot, and belong to domain of
computer checking.
What is difficult to spot is wrong use of definitions and concepts
- spotting these proofs leads to advancement of mathematics. Such
errors become apparent as soon as you try to formalize a proof for
computer verification.
Considering this, it seems computer aided verification of chips
and algorithms would be a immediate use of proof systems, rather than
verifying pure mathematics.
-- - Mohsin.