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