From qed-owner Tue May 4 21:12:16 1993 Received: by antares.mcs.anl.gov id AA16626 (5.65c/IDA-1.4.4 for qed-outgoing); Tue, 4 May 1993 21:10:10 -0500 Received: from arp.anu.edu.au by antares.mcs.anl.gov with SMTP id AA16618 (5.65c/IDA-1.4.4 for ); Tue, 4 May 1993 21:10:03 -0500 Received: by arp.anu.edu.au id AA01129 (5.65c/IDA-1.4.2.9 for qed@mcs.anl.gov); Wed, 5 May 1993 12:09:52 +1000 Received: from Messages.7.15.N.CUILIB.3.45.SNAP.NOT.LINKED.arp.anu.edu.au.sun4.41 via MS.5.6.arp.anu.edu.au.sun4_41; Wed, 5 May 1993 12:09:51 +1000 (EST) Message-Id: Date: Wed, 5 May 1993 12:09:51 +1000 (EST) From: Zdzislaw Meglicki To: qed@mcs.anl.gov Subject: Re: Formalizing notations and context Sender: qed-owner Precedence: bulk In "swan.cl.cam.:104680:930505012709"@cl.cam.ac.uk John.Harrison@cl.cam.ac.uk writes: > Rather, I see the principal difficulty as being the large amount of informal or > semi-formal context which is traditionally associated with notations. For > example, flicking through the first few pages of Matsumura: "Commutative ring > theory" we find: > [... examples of how mathematicians can get flippant about context and > notation ...] > If one hopes to make mathematicians used to ignoring lowbrow details like this > use QED, then considerable powers of persuasion are called for. If it can't be > done, then some very difficult AI problems have to be faced! I feel that this issue should become one of the subprojects of QED: to allow for the use of natural mathematical context-dependent notations and other means of expression, possibly definable by the users themselves. This, certainly is a difficult AI problem, but not an insurmountable one. Since amongst the aims of the project is to give mathematics to the "masses" and also to attract real mathematicians to QED - a humane and intelligent interface which would be capable of swallowing and understanding equivalents of: > "If f:A->B is a ring homomorphism and J is an ideal of B, then f (J) is an > ideal of A and we denote this by A /\ J; if A is a subring of B and f is the > inclusion map then this is the same as the usual set-theoretic notion of > intersection. In general this is not true, but confusion does not arise." would be most helpful. I see this as a gradual process. It might look quite insurmountable at present to build a reasoning system which would accept something like: "In general this is not true, but confusion does not arise". But it may be less difficult to implement initially something that at least makes a little step in that direction and then improve on it. For example, upon having received a phrase like that from the user, the system could ask the user to be somewhat more specific and provide a few more hints which would allow the system to apply a more precise meaning to various statements within this particular domain. There is a European Community project called MEDLAR (Mechanising Deduction for Logics of Practical Reasoning) whose aim is to build a system for selling cars. The system must be capable of outguessing and outsmarting the customer, and if need be, even of lying (the things logic is used for nowadays!) - building a system which can understand what the user really means on top of what the user merely says is not a hopeless undertaking. Zdzislaw Gustav Meglicki, gustav@arp.anu.edu.au, Automated Reasoning Program - CISR, and Plasma Theory Group - RSPhysS, The Australian National University, G.P.O. Box 4, Canberra, A.C.T., 2601, Australia, fax: (Australia)-6-249-0747, tel: (Australia)-6-249-0158 From qed-owner Wed May 5 13:48:06 1993 Received: by antares.mcs.anl.gov id AA02857 (5.65c/IDA-1.4.4 for qed-outgoing); Wed, 5 May 1993 13:35:59 -0500 Received: from aerospace.aero.org by antares.mcs.anl.gov with SMTP id AA02850 (5.65c/IDA-1.4.4 for ); Wed, 5 May 1993 13:35:54 -0500 Received: from antares.aero.org by aerospace.aero.org with SMTP (5.65c/6.0.GT) id AA02457 for qed@mcs.anl.gov; Wed, 5 May 1993 11:35:49 -0700 Posted-Date: Wed, 5 May 93 11:35:46 PDT Message-Id: <199305051835.AA02457@aerospace.aero.org> Received: from calamari.aero.org by antares.aero.org (4.1/AMS-1.0) id AA04527 for qed@mcs.anl.gov; Wed, 5 May 93 11:35:47 PDT Date: Wed, 5 May 93 11:35:46 PDT From: cal@aero.org To: qed@mcs.anl.gov Subject: Continuing Conversation - NO Flames Sender: qed-owner Precedence: bulk I think Bob Boyer's reply to my somewhat intemperate message has helped clarify some of the issues over which we differ. I think some of the major points are summarized well in his note, though I would probably express them differently 8-). More on this later. My note about failures of imagination was not intended to imply ineptness; only that we are up against a very hard problem, and we need even more smarts about abstraction than the kinds currently in use. I hope the discussion continues to gather more mathematicians who can comment on their own impressions and expectations for such a system. more later, cal From qed-owner Wed May 5 18:57:39 1993 Received: by antares.mcs.anl.gov id AA08670 (5.65c/IDA-1.4.4 for qed-outgoing); Wed, 5 May 1993 18:53:49 -0500 Received: from arp.anu.edu.au by antares.mcs.anl.gov with SMTP id AA08660 (5.65c/IDA-1.4.4 for ); Wed, 5 May 1993 18:53:43 -0500 Received: by arp.anu.edu.au id AA21497 (5.65c/IDA-1.4.2.9 for qed@mcs.anl.gov); Thu, 6 May 1993 09:53:29 +1000 Received: from Messages.7.15.N.CUILIB.3.45.SNAP.NOT.LINKED.arp.anu.edu.au.sun4.41 via MS.5.6.arp.anu.edu.au.sun4_41; Thu, 6 May 1993 09:53:29 +1000 (EST) Message-Id: <8fu5Bt_KmlE2BHIGot@arp> Date: Thu, 6 May 1993 09:53:29 +1000 (EST) From: Zdzislaw Meglicki To: qed@mcs.anl.gov Subject: Re: Continuing Conversation - NO Flames Sender: qed-owner Precedence: bulk In <199305051835.AA02457@aerospace.aero.org> cal@aero.org writes: > My note about failures of imagination was not intended to imply ineptness; > only that we are up against a very hard problem, and we need even more smarts > about abstraction than the kinds currently in use. This is where the challenge for a system such as QED is. If only currently available techniques and technology were sufficient then where would the challenge be? It would merely be just a bureaucratic exercise in translating a book or a collection of books into a computer code. As QED develops I am sure that great many insights and new techniques will be developed. The richness of mathematics will force QED implementors to do just that. It is a bit like with the landing on the Moon. When JFK made his famous speech the technology to achieve that didn't exist yet. But to set up the goal provided the impetus for further technology developments and ultimately we all ended up having microwave ovens and teflon frying pans in our kitchens. Can you imagine life without a microwave? In 20 years time engineers will find it equally hard to believe that once upon a time people were doing mathematics without QED! Zdzislaw Gustav Meglicki, gustav@arp.anu.edu.au, Automated Reasoning Program - CISR, and Plasma Theory Group - RSPhysS, The Australian National University, G.P.O. Box 4, Canberra, A.C.T., 2601, Australia, fax: (Australia)-6-249-0747, tel: (Australia)-6-249-0158 From qed-owner Thu May 6 15:13:05 1993 Received: by antares.mcs.anl.gov id AA29493 (5.65c/IDA-1.4.4 for qed-outgoing); Thu, 6 May 1993 14:56:31 -0500 Received: from altair.mcs.anl.gov by antares.mcs.anl.gov with SMTP id AA29484 (5.65c/IDA-1.4.4 for ); Thu, 6 May 1993 14:56:28 -0500 From: Larry Wos Received: by altair.mcs.anl.gov (4.1/GeneV4) id AA10771; Thu, 6 May 93 14:56:28 CDT Date: Thu, 6 May 93 14:56:28 CDT Message-Id: <9305061956.AA10771@altair.mcs.anl.gov> To: qed@mcs.anl.gov Subject: another country Sender: qed-owner Precedence: bulk discovery and mathematicians The following is intended to be for the recent discussion on "discovery" and the subsequent response to Boyer's comments on the subject. Regarding the request for mathematicians to comment: Perhaps I qualify as a mathematician, having gotten my PhD in group theory under R. Baer, and having done my Masters at the University of Chicago. My main use of an automated reasoning program for applications is in the context of proving theorems from areas of mathematics and logic. With no intended denigration, I refer here to proof finding, rather than to proof checking. I consider the former "discovery". When I hear skepticism regarding the automation of "discovery", first I think that the skeptic might well have in mind a classical AI approach. If that is the case, I heartily agree, believing that for countless decades programs will not function as mathematicians do; nor must they. The goal of emulating the human mind is certainly not mine, when I focus on the automation of logical reasoning. Indeed, I think such emulation a goal essentially out of reach. For example, the mathematician uses instantiation when deducing that the square of yz is the identity from the hypothesis that the square of x is the identity, in the theorem that asserts that groups in which the square of every element is the identity are cmmutative. Wise instantiation seems too difficult to automate. Perhaps behind the negative New York article (July 14 1991) is some despair at capturing the mathematician's mind in a computer program. Clearly, the mathematicians they quoted were unaware of the successes in answering open questions, where a key role was played by an automated reasoning program. I am in no way talking about a computational role; instead, I mean arguments of the type found in group theory, ring theory, various logic calculi, and the like. That the "formalization of discovery is extremely hard" cannot be doubted. But, unless one is interested in the "theory" of discovery, it seems clear to me that we at Argonne have succeeded (in effect) in formalizing discovery in the sense that our programs do discover marvelous proofs. That mathematicians use "disparate" and "mysterious" methods of discovery is true; when I have asked them about how they found a proof, seldom can they tell me in detail. In my own work, I freely admit to waking up with a solution to a problem. However, rather than (as in classical AI) attempting to emulate such powerful minds (of people), our programs use disparate methods, diverse strategies and various inference rules. The explicit use of strategy, I have often said, is but one of the differences in some of automated reasoning as compared with research by mathematicians. Prediction: Within twenty years, some mathematicians will have formed an impressive team with some automated reasoning program to answer a number of deep questions. Mechanizing discovery is not a long way off: It is here, if one means the ability to answer open questions with a reasoning program. But perhaps I have missed the point of the objection. Perhaps the idea is the mechanization of presenting interesting theorems, culled from the output of the program, culled by the program itself. The New York Times was wrong: Computers do beautiful mathematics, and I regret that they never acknowledged my rebuttal article. I do not feel like a child in a candy shop, unable to choose; rather, I am delighted with OTTER (McCune's) and its predecessors, amazed at using it successfully to answer unrelated open questions. I would have predicted in 1970 that such would not occur in my lifetime or career. I was wrong, and am s pleased. Just to be explicit, far, far more is needed, but a grand beginning has occurred, and not merely one with potential. Larry Wos From qed-owner Thu May 6 22:02:22 1993 Received: by antares.mcs.anl.gov id AA06677 (5.65c/IDA-1.4.4 for qed-outgoing); Thu, 6 May 1993 21:46:58 -0500 Received: from arp.anu.edu.au by antares.mcs.anl.gov with SMTP id AA06669 (5.65c/IDA-1.4.4 for ); Thu, 6 May 1993 21:46:51 -0500 Received: by arp.anu.edu.au id AA15558 (5.65c/IDA-1.4.2.9 for qed@mcs.anl.gov); Fri, 7 May 1993 12:46:45 +1000 Received: from Messages.7.15.N.CUILIB.3.45.SNAP.NOT.LINKED.arp.anu.edu.au.sun4.41 via MS.5.6.arp.anu.edu.au.sun4_41; Fri, 7 May 1993 12:46:44 +1000 (EST) Message-Id: Date: Fri, 7 May 1993 12:46:44 +1000 (EST) From: Zdzislaw Meglicki To: qed@mcs.anl.gov Subject: Re: another country Sender: qed-owner Precedence: bulk In 9305061956.AA10771@altair.mcs.anl.gov Larry Wos writes: > Perhaps behind the negative New York article (July 14 1991) is some > despair at capturing the mathematician's mind in a computer program. > Clearly, the mathematicians they quoted were unaware of the successes in > answering open questions, where a key role was played by an automated > reasoning program. This and perhaps also some other articles in New York Times have been mentioned on occasions in this mailing group. Can someone summarise what it was all about? Is this article available via ftp to people from outside of the US? From qed-owner Fri May 7 09:12:22 1993 Received: by antares.mcs.anl.gov id AA15951 (5.65c/IDA-1.4.4 for qed-outgoing); Fri, 7 May 1993 08:59:12 -0500 Received: from altair.mcs.anl.gov by antares.mcs.anl.gov with SMTP id AA15944 (5.65c/IDA-1.4.4 for ); Fri, 7 May 1993 08:59:10 -0500 From: Larry Wos Received: by altair.mcs.anl.gov (4.1/GeneV4) id AA13647; Fri, 7 May 93 08:59:10 CDT Date: Fri, 7 May 93 08:59:10 CDT Message-Id: <9305071359.AA13647@altair.mcs.anl.gov> To: qed@mcs.anl.gov Subject: In response Sender: qed-owner Precedence: bulk In response to various queries, I enclose first an article from the New York Times, and second my rebuttal article, which they never acknowledged. Computers Still Can't Do Beautiful Mathematics - by Gina Kolata Week in Review Section E, Sunday, July 14, 1991 p. 4- Mathematicians often say that their craft is as much an art as a science. But as more and more researchers are using computers to prove their theorems, some worry that the magic is in danger of fading away. In the past, mathematicians could count on being able to sit down with a newly published proof and carefully follow the researcher's logic, determining whether the derivations held true, relishing particularly clean and clever arguments. But when a computer is used to help prove a conjecture, reasoning is often replaced by calculation. Instead of converging on an answer through a long chain of logical deduction, mathematicians now often use computers to systematically test and discard a vast number of possible answers until they hit on the right one. Dr. Daniet Kleitman, a mathematician at MIT, explained why many mathematicians shrink back from this experimental approach. "One's motivation for reading a paper is not only to become aware of the results, but also to understand how such a proof is formulated and how it actually works," he said. "The question is, Do you want to have an experimental mathematics? Do you want to make traditional papers into experimental things?" Many mathematicians object to being put in a position of having to trust a computer and the assumptions made by its programmer. In a sense, the program itself becomes a part of the proof, and few mathematicians are equipped to check its reliability. In May Dr. Fan R. K. Chung, the editor of the Journal of Graph Theory, decided she was getting so many computer-aided proofs that it was time to formulate a policy. She wrote to her 20-member editorial board, providing one newly received paper as a test case. "Is an important result with a computer-assisted proof acceptable?" she asked. If so, "how should the paper be evaluated knowing that it is almost impossible for the referee to verify its correctness?" The paper that Dr. Chung chose as an example was submitted by Dr. Brendan McKay of the Australian National University and Dr. Stanislaw P. Radiszzowski of the Rochester Institute of Technology. It solved a variant of what mathematicians call the party problem: What is the minimum number of people you have to invite to a party to be sure that, among them, there are eight people or more who all know one another or three people or more who are all strangers to one another? The answer, discovered after some marathon computer crunching, is 28. A classical proof would have demonstrated through an unassailable chain of logic that the answer could only be 28. Instead, Dr. McKAy and Dr. Radiszowski took an experimental approach. Even with a computer, it would be impossible to examine the myriad ways--10 followed by 112 zeroes--that 28 party-goers could be acquainted with one another. But using some clever mathematics, Dr. McKay and Dr. Radiszowski cut down the number of calculations to a mere 100 trillion and then automatically sifted through permutation after permutation, ruling out all gatherings smaller than 28. In the end, the method gave an answer, but did not show why the answer was what it was. And it could not be generalized to solve other party problems. Computer-aided proofs have been a festering problem in mathematics for 14 years, ever since a famous conjecture, the four-color problem, was solved. The problem asked whether any arbitrary map of real or invented countries could be colored, as was generally believed, with four or fewer different colors. No two adjacent countries could be colored the same. In 1977, Dr. Kenneth Appel and Dr. Wolfgang Haken of the University of Illinois published a paper proving that four colors were indeed enough. But the 100-page proof relied on extensive computer calculations. The mathematicians argued that all possible maps could be boiled down to 2,000 standard configurations and then proved, by trying different colorings, that each of those 2,000 maps could be colored in four or fewer hues. "It was a very routine type of calculation that was just repetitive," Dr. Appel said. Many mathematicians found the proof difficult to swallow. It revealed no deep mathematical truths and provided no techniques that could help with other problems. "It is such a nasty situation," Dr. Chung said. "A lot of people just reject the proof outright. It goes against the instincts of most mathematicians." In their replies to Dr. Chung, many members of her editorial board expressed their hesitation about embracing such proofs. Dr. Frank Harary of New Mexico State University wrote that the proof should be "fully verified as correct by an independent computing organization" before the journal considers it. Then, if it accepts the paper, it should publish only the result, he said, while the proof should appear in a computer journal. Dr. Gary Chartrand of Western Michigan University suggested that the result could be published in a special section, titled something like "Research Announcement," taking care to mention that the proof had not been verified. Several others, like Dr. Noga Alon of Tel Aviv University, suggested that the journal accept only papers on "important" theorems and then require the authors to submit a copy of their program, so it could be available to others if they wanted to examine it. In the end Dr. Chung decided to accept the paper., But she decided not to ask for the program. "I don't think the journal should be held accountable," she said. "I think computer-aided proofs are a trend we cannot ignore. But we have to weigh them. If it is a computer-assisted proof, it is a minus. If it is a classical problem, it is a plus." While computer-aided proofs may be published as mileposts on the way to solving a problem, many mathematicians won't consider the problem really solved until there is a proof-- even if it is a hundred or more pages long--that a lone human sitting in a room can go through line by line and understand. Computers Do Produce Beautiful Mathematics Dr. Larry Wos Mathematics and Computer Science Division Argonne National Laboratory Computers do produce beautiful mathematics. In drawing the opposite conclusion, the July 14 article published in the ``Week in Review'' section overlooked the entire field of automated reasoning. The science and art so evident in the research of mathematicians are now complemented by the assistance provided by a new type of computer program that reasons logically. The field whose research has culminated in the design of such programs is called automated reasoning. Rather than simply calculating what is needed to examine a myriad of possibilities, automated reasoning programs now produce proofs that are sequences of logical steps, each step drawn from earlier steps. Indeed, what makes the results provided by a computer so satisfying is that they include the history of the steps of which the result consists. Thus a mathematician can sit alone in an office and enjoy results that share the magic often found in publications in which computers play no role. Further, the mathematician can quickly learn how the proof works, often generalize the approach taken, sometimes encountering deep mathematical truths, and without the need to trust the program that produced the proof. In addition to exhibiting logical reasoning of the type found in mathematics, reasoning programs produce results that are startling and elegant. Dr. J. Lukasiewicz was well recognized for his contributions to areas of logic, and yet the program OTTER recently found a proof far shorter and more elegant than that produced by this eminent researcher, and the program used the same notation and style of reasoning. Mathematicians and logicians find elegance in shorter proofs. Indeed, mathematicians of note are more than interested in what might be done with an automated reasoning program. Dr. I. J. Kaplansky of the University of California at Berkeley once suggested an open question for study by the computer. That question was answered, and answered by reasoning and not by calculation. Dr. John Kalman of the University of Auckland posed a number of questions concerning possible axioms for a field in logic. Contrary to the conjecture that each of the formulas under study was too weak, a computer program provided a complicated and lengthy proof showing that two of them offer the needed and sought-after power. The proofs are precisely in the style that Kalman used in some of his published papers, offering a line of logical thought that could be checked for accuracy. Knowing that a reasoning program can produce such proofs, a scientist might wish to have a personal copy of such a program. That wish is easy to satisfy. Some reasoning programs run well on workstations, on personal computers, and on the Macintosh. Evidence of how well such programs run is provided by the following occurrence. In August of 1990, Dr. Dana Scott of Carnegie Mellon University attended a workshop at Argonne National Laboratory. There he learned of OTTER and some of its uses and successes. Upon returning to his university, Dr. Scott's curiosity prompted him to suggest (via electronic mail) 68 theorems for consideration by the computer. His curiosity was almost immediately satisfied, for the sought- after 68 proofs were returned with the comment that all were obtained in a single computer run with the program--and in less than 16 CPU minutes on a Sun 4 workstation. Dr. Scott now uses his own copy of OTTER on his Macintosh. The type of program that has produced these results and that we expect will continue to do so is in no way a replacement for the mathematician or logician. Nor will it ever be. Instead, this type of program provides an automated reasoning assistant whose work and methods complement those of the scientist. Reasoning assistants like OTTER are not designed in the classical notion of artificial intelligence; these programs do not take an approach that a person would take. Quite the reverse, for automated reasoning programs rely on techniques and procedures that a person would prefer not to use. Nevertheless, their use has resulted in answers to questions that were and are of interest to experts in various fields. Dr. R. Smullyan of the University of Indiana showed great pleasure and surprise at learning of some of the successes achieved by an automated reasoning program. As evidence of his interest, he posed a number of questions, receiving in turn the answers to all but one of them--a question that is still open. Without the following features, so evident in the program OTTER, far less beauty and elegance would have been produced by a program reasoning logically. This newest reasoning program, designed by Dr. William McCune of Argonne National Laboratory, can be instructed to seek shorter proofs. Such proofs are cited by Dr. E. Dijkstra of the University of Texas as important to proving the correctness of computer programs. OTTER can be given hints and suggestions based on the researcher's knowledge and intuition. The program can be instructed to seek one, two, or as many proofs as the allotted time allows, and then present each of the proofs with enough detail to permit checking for accuracy. What makes this program of particular appeal is its use of strategy, one type to restrict its reasoning, and one type to direct it. Rather than detracting from the beauty, elegance, and even magic of mathematics and logic, the use of a computer program--especially a reasoning program--can add to each. It has already. Some of the proofs found with such a program have been published in journals well respected by scientists, for example, the Journal of Algebra and the Notre Dame Journal of Formal Logic. Those proofs are logical in structure, not ones of computation. When I was a student in the Mathematics Department at the University of Chicago almost four decades ago, I would have thought it impossible for a computer to provide such proofs. After all, computers were to be used for calculations, mainly of a numerical character, not for logical reasoning. However, as it turns out, computer programs do reason, and reason so effectively that open questions are sometimes answered. Indeed, in my role as mathematician, I constantly use such a program (OTTER) in my own research. As for the difference of opinion expressed here and in the article published in the New York Times on July 14, the most probable explanation is the simplest: Most likely the scientists quoted in the article have no acquaintance with the program OTTER and with the successes obtained with it. Clearly, the enthusiasm of Dr. Scott, Dr. Smullyan, Dr. Kalman, and Dr. Kaplansky must be well placed. When I once asked Dr. Kaplansky about the automation of reasoning in the context of proving theorems, he replied, "You have a friend in court. Should you continue in your research, the mathematics papers written in 2060 or thereabouts will be at a new level of reading, with much of the current level within reach of a theorem-proving program." The beauty and magic of mathematics will never die, or even lessen. A proof consisting of a sequence of steps, each obtained by applying logical reasoning, is a marvel-- whether produced by a person or produced by a computer! Larry Wos From qed-owner Fri Jul 2 01:12:17 1993 Received: by antares.mcs.anl.gov id AA19008 (5.65c/IDA-1.4.4 for qed-outgoing); Fri, 2 Jul 1993 01:04:42 -0500 Received: from bos2a.delphi.com (delphi.com) by antares.mcs.anl.gov with SMTP id AA19001 (5.65c/IDA-1.4.4 for ); Fri, 2 Jul 1993 01:04:39 -0500 Received: from delphi.com by delphi.com (PMDF V4.2-11 #4520) id <01H01TC9CSUO8ZFQ1H@delphi.com>; Fri, 2 Jul 1993 02:04:14 EDT 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 From qed-owner Fri Jul 2 01:17:19 1993 Received: by antares.mcs.anl.gov id AA19104 (5.65c/IDA-1.4.4 for qed-outgoing); Fri, 2 Jul 1993 01:14:05 -0500 Received: from bos3a.delphi.com by antares.mcs.anl.gov with SMTP id AA19097 (5.65c/IDA-1.4.4 for ); Fri, 2 Jul 1993 01:14:02 -0500 Received: from delphi.com by delphi.com (PMDF V4.2-11 #4520) id <01H01TNJRW288ZFOWH@delphi.com>; Fri, 2 Jul 1993 02:13:20 EDT Date: Fri, 02 Jul 1993 02:13:20 -0400 (EDT) From: LYBRHED@delphi.com Subject: Motivation #1 To: qed@mcs.anl.gov Message-Id: <01H01TNJWG0I8ZFOWH@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 10. The Manifesto begins by promising to solve a problem which either does not exist, or can't be solved. 1. The problem doesn't exist. > First, the increase of mathematical knowledge during the last > two hundred years has made the knowledge, let alone > understanding, of even the most important mathematical results > something beyond the capacity of any human. Poincare understood all the important mathematics of his time. That was one hundred years ago. Hilbert and Klein also understood all the important mathematics of the 1890s. How has the situation changed since then? Did it get harder and harder to survey all the important areas of mathematics, until at some point it became impossible? On the contrary. Forty years ago, Rene Thom could go to just about any seminar and jump right in, and so could Hermann Weyl and John von Neumann. And many others: participants in the Bourbaki seminars had to be prepared to discuss any part of mathematics. There were more mathematicians who understood all the important areas of math in the 1950s than there had been at the turn of the century. There are probably even more mathematicians in the present generation who have a grasp of mathematics as a whole. For example, there are probably at least a hundred mathematicians who have an attention span wide enough to comprehend Andrew Wiles's proof in its entirety, including the steps leading up to it, and who are also capable of seeing how similar methods could be applied to other problems. I'm not one of them and I don't even know most of their names, but I'm sure they exist. Their vision spans a larger mathematical horizon than what was visible to Poincare or Gauss. Of course no one can know everything in detail. That's not the point. In mathematics, as in anything else, you have to think on a strategic level, and put systems together out of black boxes. Some people will always be able to do that. How much of 20th century mathematics is really important? Years ago I overheard a conversation between a young assistant professor and some graduate students. The professor was describing his plan to launch a new journal. He had invented some obscure new branch of mathematics, and was going to publish a journal that no one but he and his clique would read; therefore no one would know that it was bogus; therefore he could get government grants, promote his career, etc. He was inviting the graduate students to join him in this project. His journal is, alas, not the only one of its kind. If you don't read this stuff, you're not missing anything. (Incidentally, a manifesto is exactly the place to draw a firm line between what is important and what isn't.) Even if you leave aside junk written by cynical opportunists, and only consider mathematics written by sincere mathematicians, most of it is ephemeral. Of course no one could read all of it, but so what? Let's go on to the next sentence of the Manifesto: > For example, few mathematicians, if any, will ever understand > the entirety of the recently settled structure of simple finite > groups or the proof of the four color theorem. This is supposed to be an "example" of what was just stated. Why is the proof of the Four Color Theorem one of the "most important results?" It is certainly famous. It is one of those things high school teachers love to talk about. They think it is An Important Theorem in Advanced Mathematics. But is it? If someone had found an elegant proof that showed how it relates to a larger body of knowledge, then it would have been important. As a conjecture, it seemed to be important; as a theorem, it turned out to be disappointing. In what sense is it beyond my capacity to know or to understand? I know what the theorem says, and I know that it was finally proved by brute force, using a computer-aided enumeration of cases. What else do I need to know about it? It may be true that no one will ever understand this proof in its entirety, but this does not imply or illustrate that it is impossible for today's mathematicians to have the same strategic understanding of mathematics that Poincare had. In mathematics or any other science, understanding is not the same as omniscience. It would be impossible for a biologist to know the unique biochemical characteristics of all the insects in the world, but it is possible to understand biology. (Ask Cairns-Smith and Kaufmann!) It is also possible to understand mathematics. It is easier now than it ever was. The "problem" QED is supposed to solve is an illusion. 2. The problem exists but can't be solved. There is a sense in which there is a problem of "too much mathematics." There is an enormous amount of mathematics which is undeniably important, and which is inaccessible to me, because it would take a thousand years to read it. But this is an ineluctable fact. It's not a problem that could be solved. QED could not possibly change the situation. Nothing can change it. One man can't absorb all the mathematics produced by hundreds. If you take the collected works of Abel, Riemann, Poincare, Goedel, Thom, and two or three hundred other mathematicians whose work is at least sometimes on more or less the same level, and enter all that mathematics into a proof checker, it would still take many lifetimes to read it all. In fact it would take longer to read mathematics through a QED terminal than it would take to read it in printed form. (I envision a QED terminal as something resembling an ORION terminal.) 3. The "problem" can be mitigated, but not with QED. To the extent that there is a problem of "too much math," the only way to mitigate it is to increase one's reading speed. QED goes in the wrong direction. If the target is to increase my reading speed, you don't want to force me to resolve informal statements into all their nitty gritty logical and set theoretic details. That would be like forcing me to read program listings in assembly language. It would slow me down. To increase my reading speed, what you want to do is present mathematics on a computer screen in such a way that I can take in more of it at a glance, and see relationships quickly that I would otherwise have to discover with great labor. Better yet, you want to present mathematics on the screen in such a way that it trains my imagination, so that eventually I can learn to see vector fields the way Riemann saw them, without the aid of a computer, and maybe even learn to see everything from the center, as he did. Therefore, if Motivation #1 is the main reason for pursuing the QED project, we should think less about how mathematics is represented in the computer, and more about how it is presented on the screen. Lyle Burkhead From qed-owner Fri Jul 2 01:19:08 1993 Received: by antares.mcs.anl.gov id AA19129 (5.65c/IDA-1.4.4 for qed-outgoing); Fri, 2 Jul 1993 01:16:47 -0500 Received: from bos3a.delphi.com by antares.mcs.anl.gov with SMTP id AA19122 (5.65c/IDA-1.4.4 for ); Fri, 2 Jul 1993 01:16:42 -0500 Received: from delphi.com by delphi.com (PMDF V4.2-11 #4520) id <01H01TQ89PDY8ZFOWH@delphi.com>; Fri, 2 Jul 1993 02:16:03 EDT Date: Fri, 02 Jul 1993 02:16:02 -0400 (EDT) From: LYBRHED@delphi.com Subject: From idea to project. To: qed@mcs.anl.gov Message-Id: <01H01TQ89PE08ZFOWH@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 Explanatory note. In April, when I was in darkest Arkansas and had no access to computers, Bob was kind enough (or foolhardy enough) to send me a printed copy of the first two weeks of the QED e-mail discussion. The following letter is a slightly expanded copy of my reply, which was a handwritten letter dated May 10. "Objection 9" and "Objection 10" are also based on old letters and notes written in February, March, and April. I'm just now signing on and don't know what has happened since the last archive, so I don't know if any of this material is still relevant... L.B. Dear Bob, You and Rusty opened the discussion by asking for "suggestions on how to turn it from an idea into a project." I want to address myself to that point. You sent me 76 pages of notes, which were generated in a 2-week period. At this rate, you will soon have hundreds of pages of this stuff, with no structure, no way to connect one remark with others on the same subject, and no way to put it all together and arrive at a conclusion. The very next thing you need to do is establish a structure for the discussion. If Step 1 was to write the Manifesto, and Step 2 was to ask for comments, then Step 3 is to appoint a librarian to organize the comments. Actually steps 2 and 3 should have been reversed, but it's too late for that. The discussion itself should be a microcosm of QED, one aspect of which is "the ability to scan the literature for relevant results." Items should be numbered and classified as they come in. They should be put into a text base. I would suggest putting all the comments into Lotus "Agenda," but there are other possibilities. (Agenda is described in CACM, July 1990, page 105.) There should be pointers from each item to related items, and to the section of the Manifesto to which the comment applies. After about 100 - 200 pages of discussion, the participants (or the moderator) should review what has been said and bring it to a conclusion. The conclusion should result in an action. In the present case, the notes you sent me end with Konrad's statement that we should be addressing ourselves to students. If you take that to be the conclusion of the first round of discussion, it has implications for the Manifesto. A manifesto addressed to 18 year olds would have a different form, tone, and content than the original one. A manifesto addressed to students should not read like a bureaucratic document. You don't need to go into funding agencies and career planning in a manifesto -- imagine Jefferson discussing such things in the Declaration of Independence! Of course that level of reality has its place, it exists, it has to be dealt with at some point down the line. But this isn't the place to discuss it. A manifesto should present an inspiring vision of mathematics. If there is ever a time for unabashed enthusiasm, this is it. Thus the first round of discussion should result in an action: writing Version 2 of the Manifesto in such a way that a generation of students are inspired to devote their lives to the creation of QED. The next round of discussion might (for example) pursue Michael Beeson's line of thought, arrive at a conclusion about it, and result in Version 3 of the Manifesto (or some other tangible result). In other words the discussion should not be allowed to proceed in a desultory fashion until it fills five feet of shelf space. It should be divided into segments, each of which results in an action. Each iteration of the Manifesto should have a Manifestation, which would consist of a User's Manual for QED and a demo. I don't know what facilities UNIX has for developing demos. In the PC world, there are programs (such as Dan Bricklin's "Demo II") with which you can create a mock-up of a proposed piece of software. The functions are stubs which can only be called for one value and always return a pre- arranged result; however, the functions are all there, and the prospective user can see what the program looks like, put it through its paces, and make suggestions about the next iteration. If no such facilities exist in the UNIX world, a high priority task is to create them. This would be Step 4. You could start with Smalltalk or NextStep and build a workbench and a suite of tools designed specifically for creating QED demos, and for refining those demos into working programs. Step 5 is to get the iterative process started. Write a user's manual and demo according to your original vision of QED. Then rewrite the Manifesto and the Manifestation in view of the discussion up to that point. That would be Version 2. Have another discussion of about 200 pages, which culminates in Version 3 (or 2.1). And so forth. After several iterations, the general idea and the general appearance of QED will be fairly stable. Then the demo will be given more and more functionality, until eventually it becomes a working set of programs with a complete (or potentially complete) internal representation of mathematics. Meanwhile -- Step 6 -- you need to develop a computer science curriculum in which QED is the central project. The students will study exactly those topics in computer science that will prepare them to write a senior thesis on QED. I am assuming that QED includes not only a proof checker but also modelling software, tools for experimentation, and all the other things listed in Section 6 of the Manifesto; the evolutionary software mentioned in Section 3, Problem 7; models of the material world, such as the autonomous undersea mining operation of Motivation #2; the searchable digital library of Motivation #1; and other software that comes up in the course of the project, such as Michael Thayer's Hermeneutical Daemon, and the tools for producing demos, discussed above. I stress that this is an assumption. The Manifesto is ambiguous about what QED actually is. In most of the Manifesto (especially Sections 2 - 5), and in the e-mail discussion, it is taken for granted that QED is basically a proof checker. Only in Sections 1 and 6 do we get a glimpse of a higher vision of QED. The User's Manual and demo should clarify the question of what QED actually consists of (that is part of their purpose). Anyway for the moment I am going to assume that QED includes everything mentioned in the previous paragraph. What I am proposing is a double major in math/C.S. in which the students write all that software and use it. And it wouldn't have to stop with math. The same idea could be extended to other subjects. You and your colleagues could write a series of C.S. textbooks, in which you present Computer Science for the next century. At most universities, the C.S. curriculum seems to have jelled 10 or 15 years ago. "Computer Science" is an eclectic group of courses not based on any organizing principle or idea. If someone proposes a new C.S. curriculum that is based on an idea, it will pre-empt the field. In the 1960's, the "New Math" took over the mathematics curriculum, and Chomsky took over linguistics. Computer science is ripe for just such a takeover, and the new idea wouldn't even have to be a good one. I happen to take a dim view of both Chomsky and the New Math, but they had far reaching effects on their respective subjects. In the case of computer science I think the following proposal is, for better or worse, an idea whose time has come. Computer science could be not just one major among others, but the center of a whole new course of study. All students would take a double major in computer science and some other subject, and in their second subject they would make the computer representation of knowledge in that subject the organizing principle of their studies. Sometimes I wonder if it would be possible to create a computer representation of Plato's metaphysics, or Aristotle's. You could have a philosophy major within the C.S. department, in which this question is investigated. You could also have an economics major, in which the students create computer models of the economy. You could include the language transparency project. Biology could be the study of artificial life. Chemistry could be "dry" chemistry. Math majors would work on QED. And so forth. It would be possible to design an entire curriculum in which the computer modelling of reality is the central idea. Lyle From qed-owner Fri Jul 2 18:15:28 1993 Received: by antares.mcs.anl.gov id AA06620 (5.65c/IDA-1.4.4 for qed-outgoing); Fri, 2 Jul 1993 17:58:01 -0500 Received: from THIALFI.CS.CORNELL.EDU by antares.mcs.anl.gov with SMTP id AA06613 (5.65c/IDA-1.4.4 for ); Fri, 2 Jul 1993 17:57:57 -0500 Received: from CLOYD.CS.CORNELL.EDU by thialfi.cs.cornell.edu (5.67/I-1.99E) id AA11111; Fri, 2 Jul 93 18:57:56 -0400 Received: from GEMINI.CS.CORNELL.EDU by cloyd.cs.cornell.edu (5.67/I-1.99D) id AA24066; Fri, 2 Jul 93 18:58:02 -0400 Message-Id: <9307022257.AA27610@gemini.cs.cornell.edu> Received: by gemini.cs.cornell.edu (5.67/N-0.13) id AA27610; Fri, 2 Jul 93 18:57:53 -0400 To: qed@mcs.anl.gov Subject: Re: Motivation #1 In-Reply-To: 's message of "Fri, 02 Jul 93 02:13:20 EDT." <01H01TNJWG0I8ZFOWH@delphi.com> Date: Fri, 02 Jul 93 18:57:53 -0400 From: Wilfred Chen Sender: qed-owner Precedence: bulk Lyle Burkhead wrote: Objection 10. The Manifesto begins by promising to solve a problem which either does not exist, or can't be solved. 1. The problem doesn't exist. ... 2. The problem exists but can't be solved. There is a sense in which there is a problem of "too much mathematics." There is an enormous amount of mathematics which is undeniably important, and which is inaccessible to me, because it would take a thousand years to read it. But this is an ineluctable fact. It's not a problem that could be solved. QED could not possibly change the situation. Nothing can change it. One man can't absorb all the mathematics produced by hundreds. If you take the collected works of Abel, Riemann, Poincare, Goedel, Thom, and two or three hundred other mathematicians whose work is at least sometimes on more or less the same level, and enter all that mathematics into a proof checker, it would still take many lifetimes to read it all. In fact it would take longer to read mathematics through a QED terminal than it would take to read it in printed form. (I envision a QED terminal as something resembling an ORION terminal.) If reading is the only thing we want to make use of QED. One of the advantage a teacher has over a book is that you can ask questions that either aren't answered explicitly in the book or you can't find it in the book easily. A successful QED system would be somewhere in the middle between a book and a teacher: being able to answer some questions that are obvious consequences of what's in the book. There really is no limit to how much we could want from such a knowledge representation system. Furthermore, even a very poor machine approximation to human intelligence is appealing, because it is very much easier to duplicate. 3. The "problem" can be mitigated, but not with QED. To the extent that there is a problem of "too much math," the only way to mitigate it is to increase one's reading speed. QED goes in the wrong direction. If the target is to increase my reading speed, you don't want to force me to resolve informal statements into all their nitty gritty logical and set theoretic details. That would be like forcing me to read program listings in assembly language. It would slow me down. To increase my reading speed, what you want to do is present mathematics on a computer screen in such a way that I can take in more of it at a glance, and see relationships quickly that I would otherwise have to discover with great labor. Better yet, you want to present mathematics on the screen in such a way that it trains my imagination, so that eventually I can learn to see vector fields the way Riemann saw them, without the aid of a computer, and maybe even learn to see everything from the center, as he did. Why limit to the screen? Surely there are limitations to the visual system. While we are at it (not exacly a QED topic) perhaps abstract mathematical objects can be presented by feeding it directly to some kind of brain implant, or, perhaps easier, some kind of direct stimulation of the retina with light beams. We'd probably have to be trained from an early age to handle these. Wilfred Chen From qed-owner Mon Jul 5 22:43:13 1993 Received: by antares.mcs.anl.gov id AA23410 (5.65c/IDA-1.4.4 for qed-outgoing); Mon, 5 Jul 1993 21:57:38 -0500 Received: from chelm.cs.umass.edu by antares.mcs.anl.gov with SMTP id AA23403 (5.65c/IDA-1.4.4 for ); Mon, 5 Jul 1993 21:57:35 -0500 Received: by chelm.cs.umass.edu (5.65/DEC-Ultrix/4.3) id AA03113; Mon, 5 Jul 1993 22:57:14 -0400 Date: Mon, 5 Jul 1993 22:57:14 -0400 From: yodaiken@chelm.cs.umass.edu (victor yodaiken) Message-Id: <9307060257.AA03113@chelm.cs.umass.edu> To: LYBRHED@delphi.com, qed@mcs.anl.gov Subject: Re: How many false theorems are there? Sender: qed-owner Precedence: bulk I think that it's a mistake to consider automated deduction as a correction to mathematical practice, much as such thoughts boost the egos of computer scientists. IMHO automated deduction should aim at making it possible to treat deduction as calculation. The "theorems" that we wish to prove in computer science and engineering are quite different from the theorems that traditionally interest mathematicians. We need to prove that a specific piece of code computes a specific function or that there are no paths between two nodes of a specific and very large graph that contain less than a certain number of transitions, or that IEEE floating point calculations given as a certain mathematical expression approximate the real valued computation of that expression within some epsilon .... Proofs of these low theorems are going to be long, complicated and far less likely to be pretty or illuminating than proofs of the high theorems of mathematics. It has been shown that some very complex applied algebra and analysis can be automated to a degree (in MAPLE,Mathematica etc). What we need to do is show that complicated and boring proofs can also be automated. From qed-owner Tue Aug 3 05:19:35 1993 Received: by antares.mcs.anl.gov id AA16196 (5.65c/IDA-1.4.4 for qed-outgoing); Tue, 3 Aug 1993 03:01:11 -0500 Received: from bos1a.delphi.com (delphi.com) by antares.mcs.anl.gov with SMTP id AA16189 (5.65c/IDA-1.4.4 for ); Tue, 3 Aug 1993 03:01:08 -0500 Received: from delphi.com by delphi.com (PMDF V4.2-11 #4520) id <01H1AMQV4V0M90NYL7@delphi.com>; Tue, 3 Aug 1993 04:00:35 EDT Date: Tue, 03 Aug 1993 04:00:34 -0400 (EDT) From: LYBRHED@delphi.com Subject: from idea to project To: qed@mcs.anl.gov Message-Id: <01H1AMQV4V0O90NYL7@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 I have been reading "NeXTSTEP Programming: Step One," by Garfinkel and Mahoney. The two main projects in the book are... calculators! First you build a little four-function calculator, then a more elaborate one that can graph functions. I am struck by the fact that NeXTSTEP seems to be designed as a construction kit for making calculators. And the idea of a "calculator" can be taken to whatever level of sophistication you want. Steve Jobs's original vision of the NeXT Cube could be described as "a platform for QED." The original Cube came with Mathematica, Allegro Common Lisp, and a built-in searchable digital library, at least in skeleton form. It was a Pythagorean computer designed for mathematicians. But so far the only mathematicians who have taken him up on it are the quants on Wall Street and the cryptographers at the CIA. I don't think this was what Steve had in mind. In my last letter I said there should be a demo of QED, or actually a series of demos with increasing functionality. Why not take the NeXT Cube as a prototype of QED? Of course it fell far short of the ideal. It was concerned with numerical calculations rather than proofs. But it could be taken as a demo of Version 0 of QED. It was a first approximation to "a computer system that contains all of mathematics." It is the only computer that even aspires to be QED-like, and it actually exists, so it gives us a tangible starting point. If the Cube is Version 0, then Version 1 would be a 486 computer running NeXTSTEP 3.x. It will have a built-in proof constructor, to go with its built-in librarian and built-in calculation engine. By "proof constructor" I mean a mathematician's workbench, something like the combination of editor, compiler, and debugger that programmers use. It could be used to "compile" a proof into Machine Math and to connect it with other theorems in a "hypermath" network. It would also be able to animate a proof, like the programs that animate sorting algorithms. Version 1 will also have at least the beginning of a mathematical library. The Digital Librarian is already there in NeXTSTEP as a capability, but there is no actual content in the library; at least no mathematical content. The original Cube came with the works of Shakespeare on an optical disk. Shakespeare was the whole library! There is more in Heaven and Earth, Horatio, than is dreamt of in your philosophy! This was where Steve's vision wavered. This was one of his first strategic mistakes. You have to give him credit for conceiving the idea of a computer with a built- in library, but instead of Shakespeare he should have bundled a library of mathematical theorems, methods, and ideas. Version 1 of QED will have at least a token library, enough to see what it would look like. First it will be necessary to create the tools needed to write the proof constructor. NeXTSTEP comes with "kits" for constructing various kinds of applications: the Music Kit, the DB Kit, and so forth. What we need is a Math Kit. This could be an actual project as soon as school starts in the fall. All we need to do is find some students who think working on Version 1 would be a good way to learn computer science and math at the same time, and at least one professor willing to teach them. From qed-owner Tue Aug 3 11:03:47 1993 Received: by antares.mcs.anl.gov id AA24543 (5.65c/IDA-1.4.4 for qed-outgoing); Tue, 3 Aug 1993 10:54:55 -0500 Received: from linus.mitre.org by antares.mcs.anl.gov with SMTP id AA24532 (5.65c/IDA-1.4.4 for ); Tue, 3 Aug 1993 10:54:51 -0500 Received: from circe.mitre.org by linus.mitre.org (5.61/RCF-4S) id AA05976; Tue, 3 Aug 93 11:54:45 -0400 Posted-Date: Tue, 03 Aug 93 11:54:42 -0400 Received: by circe.mitre.org (5.61/RCF-4C) id AA01015; Tue, 3 Aug 93 11:54:43 -0400 Message-Id: <9308031554.AA01015@circe.mitre.org> To: qed@mcs.anl.gov Cc: jt@linus.mitre.org Subject: Re: from idea to project In-Reply-To: Your message of "Tue, 03 Aug 93 04:00:34 EDT." <01H1AMQV4V0O90NYL7@delphi.com> Date: Tue, 03 Aug 93 11:54:42 -0400 From: jt@linus.mitre.org Sender: qed-owner > In my last letter I said there should be a demo of QED, or actually > a series of demos with increasing functionality. The idea seems to be "design by convergence from demos." Is this really a serious idea for software development? If it is, I hope the idea does not catch in other areas -- such as airplane design. Javier Thayer From qed-owner Tue Aug 3 16:26:14 1993 Received: by antares.mcs.anl.gov id AA03624 (5.65c/IDA-1.4.4 for qed-outgoing); Tue, 3 Aug 1993 16:20:48 -0500 Received: from diamond.idbsu.edu by antares.mcs.anl.gov with SMTP id AA03615 (5.65c/IDA-1.4.4 for ); Tue, 3 Aug 1993 16:20:44 -0500 Message-Id: <199308032120.AA03615@antares.mcs.anl.gov> Received: by diamond.idbsu.edu (16.8/16.2) id AA17797; Tue, 3 Aug 93 15:21:04 -0600 Date: Tue, 3 Aug 93 15:21:04 -0600 From: Randall Holmes To: qed@mcs.anl.gov Subject: Systems Implementing All of Mathematics Sender: qed-owner Software capable of implementing mathematics already exists: for example, the HOL dialect of Edinburgh LCF (implementing classical type theory, basically the system of Russell's Principia Mathematica). The Nuprl project of Constable and others at Cornell has the same capabilities, although the foundational system they are using is of an unfamiliar type (constructive type theory). All of classical mathematics could be implemented in either of these systems (either has the capability of storing libraries of theorems built in). The opinions expressed | --Sincerely, above are not the "official" | M. Randall Holmes opinions of any person | Math. Dept., Boise State Univ. or institution. | holmes@math.idbsu.edu From qed-owner Tue Aug 3 17:55:11 1993 Received: by antares.mcs.anl.gov id AA05544 (5.65c/IDA-1.4.4 for qed-outgoing); Tue, 3 Aug 1993 17:49:36 -0500 Received: from arp.anu.edu.au by antares.mcs.anl.gov with SMTP id AA05532 (5.65c/IDA-1.4.4 for ); Tue, 3 Aug 1993 17:48:59 -0500 Received: by arp.anu.edu.au id AA04547 (5.65c/IDA-1.4.2.9 for qed@mcs.anl.gov); Wed, 4 Aug 1993 08:48:49 +1000 Received: from Messages.7.15.N.CUILIB.3.45.SNAP.NOT.LINKED.arp.anu.edu.au.sun4.41 via MS.5.6.arp.anu.edu.au.sun4_41; Wed, 4 Aug 1993 08:48:49 +1000 (EST) Message-Id: Date: Wed, 4 Aug 1993 08:48:49 +1000 (EST) From: Zdzislaw Meglicki To: qed@mcs.anl.gov Subject: Re: from idea to project In-Reply-To: <01H1AMQV4V0O90NYL7@delphi.com> References: <01H1AMQV4V0O90NYL7@delphi.com> Sender: qed-owner In <01H1AMQV4V0O90NYL7@delphi.com> LYBRHED@delphi.com writes: > [...] Why not take the > NeXT Cube as a prototype of QED? Good and elegantly designed computer systems such as NeXT certainly greatly facilitate working on difficult projects, but I would be reluctant to embrace a particular hardware/software platform for a system as important as QED. To begin with NeXT is very little known outside of the US. I have never seen this machine in Australia, although I've heard occasional rumours that someone is selling them here. QED ought to be highly portable. Perhaps a better idea would be to borrow whatever valuable software technology and ideas are required for QED from NeXT and other systems and combine them with the work that has been already done in this area so far. And, as it has been pointed recently by holmes@diamond.idbsu.edu there are already many advanced systems for implementing mathematics at various levels of formalism available. Zdzislaw Meglicki, Zdzislaw.Meglicki@anu.edu.au, Automated Reasoning Program - CISR, and Plasma Theory Group - RSPhysSE, The Australian National University, G.P.O. Box 4, Canberra, A.C.T., 2601, Australia, fax: (Australia)-6-249-0747, tel: (Australia)-6-249-0158 From qed-owner Thu Aug 5 00:47:02 1993 Received: by antares.mcs.anl.gov id AA07499 (5.65c/IDA-1.4.4 for qed-outgoing); Thu, 5 Aug 1993 00:36:57 -0500 Received: from bos2a.delphi.com (delphi.com) by antares.mcs.anl.gov with SMTP id AA07491 (5.65c/IDA-1.4.4 for ); Thu, 5 Aug 1993 00:36:55 -0500 Received: from delphi.com by delphi.com (PMDF V4.2-11 #4520) id <01H1DAAIU7S091X73N@delphi.com>; Thu, 5 Aug 1993 01:35:37 EDT Date: Thu, 05 Aug 1993 01:35:37 -0400 (EDT) From: LYBRHED@delphi.com Subject: from idea to project To: qed@mcs.anl.gov Message-Id: <01H1DAAIY8GI91X73N@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 "Perhaps a better idea would be to borrow whatever valuable software technology and ideas are required for QED from NeXT and other systems and combine them with the work that has been already done in this area so far." That's a better idea, but is it a project? What is the first step? Lyle From qed-owner Fri Aug 6 00:58:50 1993 Received: by antares.mcs.anl.gov id AA05371 (5.65c/IDA-1.4.4 for qed-outgoing); Fri, 6 Aug 1993 00:11:35 -0500 Received: from bos2a.delphi.com (delphi.com) by antares.mcs.anl.gov with SMTP id AA05364 (5.65c/IDA-1.4.4 for ); Fri, 6 Aug 1993 00:11:33 -0500 Received: from delphi.com by delphi.com (PMDF V4.2-11 #4520) id <01H1ENP1D8ZQ91XAWH@delphi.com>; Fri, 6 Aug 1993 01:10:43 EDT Date: Fri, 06 Aug 1993 01:10:43 -0400 (EDT) From: LYBRHED@delphi.com Subject: From idea to project To: qed@mcs.anl.gov Message-Id: <01H1ENP1D8ZS91XAWH@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 First I want to correct a mistake that has been bothering me for a month. In "Objection 10" I misspelled Stuart Kauffman's name. Two f's, one n. I am the kind of perfectionist who actually worries about such things. Now, about turning QED into a project: Back at the beginning of this discussion, David McAllester said that he could write a simple routine that would translate definitions and theorems from any of the other theorem-proving languages into Ontic. Nobody said "All right, let's do it." A few days later Michael Beeson came up with some excellent suggestions for making QED into a project, but no one said "Ok, let's do it." Then several people suggested getting students involved; make QED part of the cs curriculum, and get students to do much of the work. Once again, no one said "Ok, let's do it." I have a sense of futility about this. No matter what we suggest, nothing is going to happen. About portability: eventually the mathematics library will reside somewhere out here on the Net. You will be able to access it with just about any kind of computer. But that is several years in the future. When we make a prototype system, at some point somebody is going to have to sit down and start writing code in a specific language on a specific computer. At that stage it will not be portable. Lyle From qed-owner Fri Aug 6 11:25:00 1993 Received: by antares.mcs.anl.gov id AA15355 (5.65c/IDA-1.4.4 for qed-outgoing); Fri, 6 Aug 1993 11:01:45 -0500 Received: from cats.UCSC.EDU by antares.mcs.anl.gov with SMTP id AA15348 (5.65c/IDA-1.4.4 for ); Fri, 6 Aug 1993 11:01:43 -0500 Received: from si.UCSC.EDU by cats.ucsc.edu with SMTP id AA06776; Fri, 6 Aug 93 09:01:40 -0700 From: beeson@cats.ucsc.edu Received: by si.ucsc.edu (5.65/4.7) id AA27413; Fri, 6 Aug 93 09:01:39 -0700 Date: Fri, 6 Aug 93 09:01:39 -0700 Message-Id: <9308061601.AA27413@si.ucsc.edu> To: LYBRHED@delphi.com, qed@mcs.anl.gov Subject: Re: From idea to project Sender: qed-owner "No matter what we suggest, nothing is going to happen." The fundamental reason for this is that our project, while appealing for philosophical and theoretical scientific reasons, does not offer short-term benefit to anybody. I have just returned from a three-day conference (a 70th birthday fest for Bob Finn) on minimal surfaces, Navier-Stokes equations, and other topics in geometry and analysis. Someone was quoted as saying "pde (partial diff eqns) is nothing but inequality proving." This refers to the ubiquity of "estimates" in which one bounds a hypothetical solution in some norm in order to prove existence. But this still has to be done by hand, although one lecture was about checking some old calculations with Mathematica, and several used computer graphics (Brakke's Evolver package) or numerics. These people do not believe the computer will ever be able to assist them in their theorem-proving, and it is difficult to believe it for me too. I have a short-term suggestion of a semi-political nature. Let's see if we can mobilize enough energy to get Math Reviews on-line on the Internet! Here's the background: MathFile, the MR on-line system, is available on CD-ROM. If your library has six thousand dollars you can buy three CD-ROMS containing it. This useful system lets you computer-search Math Reviews 1980-now (although not all at once as you can search only one disk at a time). At the same time you can access MR on the Internet but you can get only MR numbers, not reviews themselves and not even bibliographical citations. These CD-ROM systems in libraries whiiich have them are underutilized anyway (I'm not sure why, but people I've spoken with say they would use it much more if it were on-line). The AMS told me that they use the proceeds from the CD-ROM sales to support the production of Math Reviews, and they are afraid that putting MR on-line would kill the physical MR, which supports some eighty jobs in Providence. Indeed it would: MR should go all-electronic, be available ONLY or primarily on the Internet, and be constantly updated, and paid for "somehow" by the AMS. But since reviewers write for free, if it's in electronic form it shouldn't cost much to add new reviews. From qed-owner Fri Aug 6 11:25:30 1993 Received: by antares.mcs.anl.gov id AA15242 (5.65c/IDA-1.4.4 for qed-outgoing); Fri, 6 Aug 1993 10:58:33 -0500 Received: from diamond.idbsu.edu by antares.mcs.anl.gov with SMTP id AA15235 (5.65c/IDA-1.4.4 for ); Fri, 6 Aug 1993 10:58:30 -0500 Message-Id: <199308061558.AA15235@antares.mcs.anl.gov> Received: by diamond.idbsu.edu (16.8/16.2) id AA25992; Fri, 6 Aug 93 09:58:57 -0600 Date: Fri, 6 Aug 93 09:58:57 -0600 From: Randall Holmes To: qed@mcs.anl.gov Subject: Context Sender: qed-owner A lot of what you are describing is already being done. For instance, I have written a theorem prover, with ultimate aims similar to what you are discussing, and am going to test it by getting undergraduates to work with it in the coming semester. This is "code in a specific language on a specific computer". There are several actual theorem prover projects in existence, busily building libraries of proved theorems, so far as I can tell. The official aim of these projects (and of mine) is software verification, but this covers a lot of nontrivial mathematics. I'm going to go back and read your introductory messages; I'm having some difficulty figuring out why you are discussing as hypothetical things which already exist and have existed for some time! The opinions expressed | --Sincerely, above are not the "official" | M. Randall Holmes opinions of any person | Math. Dept., Boise State Univ. or institution. | holmes@math.idbsu.edu From qed-owner Fri Aug 6 13:30:30 1993 Received: by antares.mcs.anl.gov id AA19610 (5.65c/IDA-1.4.4 for qed-outgoing); Fri, 6 Aug 1993 13:27:36 -0500 Received: from cli.com by antares.mcs.anl.gov with SMTP id AA19603 (5.65c/IDA-1.4.4 for ); Fri, 6 Aug 1993 13:27:32 -0500 Received: by CLI.COM (4.1/1); Fri, 6 Aug 93 13:21:56 CDT Date: Fri, 6 Aug 93 13:22:46 CDT From: Robert S. Boyer Message-Id: <9308061822.AA01372@dilbert.CLI.COM> Received: by dilbert.CLI.COM (4.1/CLI-1.2) id AA01372; Fri, 6 Aug 93 13:22:46 CDT To: holmes@diamond.idbsu.edu Cc: qed@mcs.anl.gov Subject: QED-like Efforts Reply-To: boyer@CLI.COM Sender: qed-owner I'm having some difficulty figuring out why you are discussing as hypothetical things which already exist and have existed for some time! Indeed, there have been a good number of QED-like efforts spread over at least the last 27 years, both large scale and small. (I hear rumors that the Polish MIZAR effort may be the largest so far.) But one can ask the question whether any of the efforts now underway has sufficient support to achieve coverage of the most commonly used sorts of mathematics. I would guess that despite at least 27 years of such projects, what has been proof-checked so far is an insignificant percentage (maybe 5%, if I may be permitted to take a blind, naive shot in the dark, could be less than 1%) of what a typical math graduate student must learn to pass qualifying exams. I fear that QED faces more difficult organizational problems (personal, national, political, social, economic, etc.) than technical problems. We not only have *some* proof checking systems, we may have a Babel's worth of them. I doubt whether this plethora of really wonderful alternative proof-checking systems is appealing to the various funding agencies or to potential users. People seemed to tire of inventing new programming languages sometime around 1980 or so. Maybe some day the C and FORTRAN of proof checking systems will become clear. (That was a joke.) Bob From qed-owner Fri Aug 6 14:56:09 1993 Received: by antares.mcs.anl.gov id AA22342 (5.65c/IDA-1.4.4 for qed-outgoing); Fri, 6 Aug 1993 14:53:23 -0500 Received: from linus.mitre.org by antares.mcs.anl.gov with SMTP id AA22335 (5.65c/IDA-1.4.4 for ); Fri, 6 Aug 1993 14:53:21 -0500 Received: from circe.mitre.org by linus.mitre.org (5.61/RCF-4S) id AA12483; Fri, 6 Aug 93 15:53:17 -0400 Posted-Date: Fri, 06 Aug 93 15:53:16 -0400 Received: by circe.mitre.org (5.61/RCF-4C) id AA01605; Fri, 6 Aug 93 15:53:16 -0400 Message-Id: <9308061953.AA01605@circe.mitre.org> To: qed@mcs.anl.gov Cc: jt@linus.mitre.org Subject: Re: From idea to project In-Reply-To: Your message of "Fri, 06 Aug 93 09:01:39 PDT." <9308061601.AA27413@si.ucsc.edu> Date: Fri, 06 Aug 93 15:53:16 -0400 From: jt@linus.mitre.org Sender: qed-owner > The fundamental reason for this is that our project, while appealing > for philosophical and theoretical scientific reasons, does not offer > short-term benefit to anybody. "Benefit" is a very vague notion, reminiscent of the largely discredited concept of "utility" in economic theory. The question is in my opinion "Is there any chance anybody will buy our product" To answer this question we have to understand the potential market for this product. Moreover, this potential market (like most other markets) is not sitting out there in some field patiently waiting to be picked like ripe strawberries. Markets are created from many segments. In this case, the many diverse groups of individuals who use mathematics in some form, would presumably constitute the segments of the QED market. For instance, publishers of math books must make a profitability calculation of this kind. Does one really know the benefit provided by books on Modular forms, elliptic curves or number theory? Yet people buy them, publishers publish them, and everybody seems to be much happier. It is true that publishers don't always encourage the best literature, but the obstacles to literature are usually ostensibly not-for-profit institutions like the Catholic church. Similarly, (Despite all his hyperbole) Stephen Wolfram deserves enormous credit for understanding that people would buy a computerized mathematics system if they were reached by an appropriate marketing strategy. Clearly, there is more to his success than that, but succesful marketing is certainly one element. If there is no reason to expect anyone would buy the QED-product then maybe we should forget it. Ask yourself this question: Under what conditions would you buy stock in the QED company? Javier Thayer