Richard Schroeppel writes:
>I believe the published mathematics literature contains a
>significant number of errors. Most are at the typo level,
>but there are some number of missing terms, missing
>hypotheses, and important wrong words. Long calculations,
>and tables, frequently have errors. Many journals have a
>section for Errata & Corrections. If QED could fix these prior
>to publication, we would be better off.
Agreed. Whenever a mathematical paper is submitted to a
journal (in machine-readable form), it could be run through QED
and checked before publication. QED would work like a compiler.
It would attempt to translate the paper into low-level logic and
generate error messages if it ran into difficulties. This would
certainly be an excellent way to eliminate errors. We all know
what a joy it is to read a program listing with hundreds of
obscure error messages due to typos and other minor mistakes,
and I'm sure mathematicians would be eternally grateful for this
service... ;-)
Seriously, this provides an answer to the question: Who are the
customers of QED? The customers are journal editors.
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.
Lyle