**Mail folder:**QED**Next message:**LYBRHED@delphi.com: "Motivation #1"**Previous message:**Larry Wos: "In response"**Reply:**victor yodaiken: "Re: How many false theorems are there?"

Date: Fri, 02 Jul 1993 02:04:14 -0400 (EDT) From: LYBRHED@delphi.com Subject: How many false theorems are there? To: qed@mcs.anl.gov Message-id: <01H01TC9KAWY8ZFQ1H@delphi.com> X-Vms-To: INTERNET"qed@mcs.anl.gov" Mime-Version: 1.0 Content-Type: TEXT/PLAIN; CHARSET=US-ASCII Content-Transfer-Encoding: 7BIT Sender: qed-owner Precedence: bulk

Objection 9. QED is bound to fail in its own terms, because mathematicians are already constructing accurate proofs. The Manifesto says (Reply to Objection 8) "The standard of success or failure [will be] whether it permits us to construct proofs substantially more accurately than we can with current hand methods." It follows that if current hand methods are already accurate, then QED is doomed to fail by its own standard. Therefore, it is necessary to demonstrate at the outset that current hand methods leave substantial room for improvement. This has not been demonstrated. In my letter of March 14 I said: > After all, most theorems are true anyway. Correctness is > not usually an issue in mathematics. Out of the thousands of > theorems you have checked, how many have been discovered > to be false? In the 18th century some mistakes were made > concerning the convergence of series, but that was settled in > the 19th century, and at this point the important areas of > mathematics are usable as is. One does not have to worry > about the soundness of Poincare's mathematics, or Hilbert's, > or R.L. Moore's, or von Neumann's... etc. You replied that 95% of the theorems you have checked turned out to be false: > It turns out to be as difficult to sit down with a formal system > and type in definitions and theorems correctly, as it is to write > a program correctly. People always make mistakes that Nqthm > catches. Generally, these are tiny little stupid mistakes. > But mistakes! All right, but that's not what I meant. We seem to be talking about two different things. I was not asking, "How often are mistakes made in entering a theorem into a proof checker?" No doubt many mistakes are made in this process. What I meant was, "Once the proof has been correctly entered into the proof checker, how often does it turn out that the original theorem was false?" I am talking about theorems from mathematics proper, not logic or computer science. When you said you had checked thousands of theorems, I thought you meant theorems from analysis, topology, algebra, geometry, and number theory. Can you give an example of a mathematical theorem that was published in a standard textbook or major journal, accepted by the mathematicians who read it, and used by them in further work, and then found to be false? By "found to be false" I don't mean a trivial lacuna was found in the proof. I mean the theorem itself alleges something to be true which is simply false, so that everything based on it falls down like a house of cards. For example, it might turn out that a contraction mapping doesn't have a fixed point after all, which would destroy most of analysis. Has anything like this ever happened? I don't think so. At the level of fixed point theorems, and the basic theorems about vector fields, linear transformations, quotient groups, covering spaces, and so forth -- the thousand or so theorems that are used as the ingredients for all further work -- at that level there are no mistakes. If the "building" metaphor is valid at all (which is not to be taken for granted), what mathematicians build is more like a coral reef than a house of cards. There may be some brittleness around the edges, but the center of mathematics is as solid as a rock. (I'm saying the center is solid, not the "foundation." Set theory is not the center; set theory is as far out on the fringe in one direction as the four color theorem is in another direction. (Incidentally, it isn't even necessary to know something is true to "build on" it. Mathematicians have been investigating what follows from the Riemann Hypothesis for more than a hundred years, and this is a perfectly valid activity whether the R.H. is ever proved or not.)) Objection 9 could be overcome in at least four different ways. 1. 2. By meeting it head on. You could demonstrate that current hand methods are not accurate. This could be done by answering my question (Can you give an example of a theorem...) in the affirmative. A few years ago, someone investigated how many papers in experimental science contained errors. It turned out that a shocking number of papers contained meaningless experiments, non sequiturs, statistical fallacies, impossible data, etc. Maybe the same thing happens in mathematics. But I'm saying it doesn't, and I think the burden of proof is on the one who asserts that it does. The way to settle this question is to ask for comments from the editors of ten major journals. How often do they have to print corrections and retractions? 3. By changing the domain of application of QED to an area where hand methods really are inadequate, such as programming. Programmers already use compilers and debuggers, and still make mistakes; QED could be conceived as a kind of super-debugger that would permit programmers to write an entire operating system (or engineers to design a chip) and be absolutely certain that it contains no bugs anywhere. 4. By changing the criterion of success or failure. You could go back to Objection 8 and say that a certain region of mathematics is perfect, and the purpose of QED is to extend that region. "The standard of success or failure of the QED project will be whether it helps us to extend the kingdom of perfection." That sounds more like a manifesto! As you put it, what you are working toward is "the extremely wonderful goal of having all mathematics in a single computing system." QED is pyramid-building on a grand scale. The idea is to create a mathematical jewel that sparkles like nothing ever has, because for the first time each atom is in its exact place. Nothing less! Lyle Burkhead