left right UP

Some Objections to the Idea of the QED Project and Some Responses

1 Paradoxes, Incompatible Logics, etc.
2 Intellectual property problems.
3 Too much mathematics.
4 Mechanically checked formality is impossible.
5 If QED were feasible, it would have already been underway several decades ago.
6 QED is too expensive.
7 Good mathematicians will never agree to work with formal systems.
8 The QED system will be large, and hence, unreliable.
9 The cooperation of mathematicians is essential but mathematicians will have no incentive to help.
10 QED would divert resource more profitably employed in support of the verification of hardware and software.
11 The notion that interesting mathematics can ever, in practice, be formally checked is a fantasy
Objection 1: Paradoxes, Incompatible Logics, etc. Anyone familiar with the variety of mathematical paradoxes, controversies, and incompatible logics of the last hundred years will realize that it is a myth that there is certainty in mathematics. There is no fundamentally justifiable view of mathematics which has wide support, and no widely agreeable logic upon which such an edifice as QED could be founded.

Reply to Objection 1: Although there are a variety of logics, there is little doubt that one can describe all important logics within an elementary logic, such as primitive recursive arithmetic, about which there is no doubt, and within which one can reliably check proofs presented in the more controversial logics. We plan to build the QED system upon such a `root logic', as we discuss below extensively. But the QED system is to be fundamentally unbiased as to the logics used in proofs. Or if there is to be a bias, it is to be a bias towards universal agreement. Proofs in all varieties of classical, constructive, and intuitionist logic will be found rigorously presented in the QED system---with sharing of proofs between logics where justified by metatheorems. For example, Godel showed how to map theorems in classical number theory into intuitionist number theory, and E. Bishop showed how to develop much of modern mathematics in a way that is simultaneously constructive and classical. A mathematical logic may be regarded as being very much like a model of the world---one can often profit from using a model even if one ultimately chooses an alternative model because it is more suited to one's purposes. Furthermore, merely because some logic is so overly strong as to be ultimately found inconsistent or so weak as to ultimately fail to be able to express all that one hopes, one can nevertheless often transfer almost all of the technique developed in one logic to a subsequent, better logic.

Objection 2: Intellectual property problems. Such an enterprise as QED is doomed because as soon as it is even slightly successful, it will be so swamped by lawyers with issues of ownership, copyright, trade secrecy, and patent law that the necessary wide cooperation of hundreds of mathematicians, computer scientists, research agencies, and institutions will become impossible.

Reply to Objection 2: In full cognizance of the dangers of this objection, we put forward as a fundamental and initial principle that the entirety of the QED system is to be in the international public domain, so that all can freely benefit from it, and thus be inspired to contribute to its further development.

Objection 3: Too much mathematics. Mathematics is now so large that the hope of incorporating all of mathematics into a system is utterly humanly impossible, especially since new mathematics is generated faster than it can be entered into any system.

Reply to Objection 3: While it is certainly the case that we imagine anyone being free to add, in a mechanically checked, rigorous fashion, any sort of new mathematics to the QED system, it seems that as a first good objective, we should pursue checking `named' theorems and algorithms, the sort of things that are commonly taught in universities, or cited as important in current mathematics and applications of mathematics.

Objection 4: Mechanically checked formality is impossible. There is no evidence that extremely hard proofs can be put into formal form in less than some utterly ridiculous amount of work.

Reply to Objection 4: Based upon discussions with numerous workers in automated reasoning, it is our view that using current proof-checking technology, we can, using a variety of systems and expert users of those systems, check mathematics at within a factor of ten, often much better, of the time it takes a skilled mathematician to write down a proof at the level of an advanced undergraduate textbook. QED will support proof checking at the speeds and efficiencies of contemporary proof-checking systems. In fact, we see one of the benefits of the QED project as being a demonstration of the viability of mechanically-assisted (-enforced) proof-checking.

Objection 5: If QED were feasible, it would have already been underway several decades ago.

Reply to Objection 5: Many of the most well-known projects related to QED were commenced in an era in which computing was exorbitantly expensive and computer communication between geographically remote groups was not possible. Now most secretaries have more computing power than was available to most entire QED-related projects at their inception, and rapid communication between most mathematics and computer science departments through email, telnet, and ftp has become almost universal. It also now seems unlikely that any one small research group can, alone, make a major dent in the goal of incorporating all of mathematics into a single system, but at the same time technology has made widespread collaboration entirely feasible, and the time seems ripe for a larger scale, collaborative effort. It is also worth adding that research agencies may now be in a better position to recognize the Babel of incompatible reasoning systems and symbolic computation systems that have evolved from a plethora of small projects without much attention to collaboration. Then perhaps they can work towards encouraging collaboration, to minimize the lack of interoperability due to diversity of theorem-statement languages, proof languages, programming languages, computing platforms, quality, and so on.

Objection 6: QED is too expensive.

Reply to Objection 6: While this objection requires careful study at some point, we note that simply concentrating the efforts of some currently-funded projects could go a long way towards getting QED off the ground. Moreover, as noted above, students could contribute to the project as an integrated part of their studies once the framework is established, presumably at little or no cost. We can imagine a number of professionals contributing as well. In particular, there is currently a large body of tenured or retired mathematicians who have little inclination for advanced research, and we believe that some of these could be inspired to contribute to this project. It may be a good idea to have a QED governing board to recognize contributions.

Objection 7: Good mathematicians will never agree to work with formal systems because they are syntactically so constricting as to be inconsistent with creativity.

Reply to Objection 7: The written body of formal logic rightly repulses most mathematical readers. Whitehead and Russell's Principia Mathematica did not establish mathematics in a notation that others happily adopted. The traditional definition of formal logics is in a form that no one can stand to use in practice, e.g., with function symbols named f1 , f2 , f3 , ... The absence of definitional principles for almost all formal logics is an indication that from the beginning, formal logics became something to be studied (for properties such as completeness) rather than to be used by humans, the practical visions of Leibniz and Frege notwithstanding. The developers of proof checking and theorem-proving systems have done little towards making their syntax tolerable to mathematicians. Yet, on this matter of syntax, there is room for the greatest hope. Although the subject of mechanical theorem-proving in general is beset with intractable or unsolvable problems, a vastly improved computer-human interface for mathematics is something easily within the grasp of current computer theory and technology. The work of Knuth on and the widespread adoption of by mathematicians and mathematics journals demonstrates that it is no problem for computers to deal with any known mathematical notation. Certainly, there is hard work to be done on this problem, but it is also certainly within the capacity of computer science to arrange for any rigorously definable syntax to be something that can be conveniently entered into computers, translated automatically into a suitable internal notation for formal purposes, and later reproduced in a form pleasant to humans. It is certainly feasible to arrange for the users of the QED system to be able to shift their syntax as often as they please to any new syntax, provided only that it is clear and unambiguous. Perhaps the major obstacle here is simply the current scientific reward system: precisely because new syntaxes, new parsers, and new formatters are so easy to design, little or no credit (research, academic, or financial) is currently available for working on this topic. Let us add that we need take no position on the question whether mathematicians can or should profit from the use of formal notations in the discovery of serious, deep mathematics. The QED system will be mainly useful in the final stages of proof reporting, similar to writing proofs up in journals, and perhaps possibly never in the discovery of new insights associated with deep results.

Objection 8: The QED system will be so large that it is inevitable that there will be mistakes in its structure, and the QED system will, therefore, be unreliable.

Reply to Objection 8: There is no doubt considerable room for error in the construction of the QED system, as in any human enterprise. A key motivation in Babbage's development of the computer was his objective of producing mathematical tables that had fewer errors than those produced by hand methods, an objective that has certainly been achieved. It is our experience that even with the primitive proof checking systems of today, errors made by humans are frequently found by the use of such tools, errors that would perhaps not otherwise be caught. The standard of success or failure of the QED project will not be whether it helps us to reach the kingdom of perfection, an unobtainable goal, but whether it permits us to construct proofs substantially more accurately than we can with current hand methods. In defense of the QED vision, let us assert that we believe that room for error can be radically reduced by (a) expressing the full foundation of the QED system in a few pages of mathematics and (b) supporting the development of essentially independent implementations for the basic checker. It goes without saying that in the development of any particular subfield of mathematics, errors in the statements of definitions and other axioms are possible. Agreement by experts in each mathematical subfield that the definitions are `right' will be a necessary part of establishing confidence that mechanically checked theorems establish what is intended. There is no mechanical method for guaranteeing that a logical formula says what a user intuitively means.

Objection 9: The cooperation of mathematicians is essential to building the QED edifice of proofs. However, because it is likely to remain very tedious to prove theorems formally with mechanical proof checkers for the forseeable future, mathematicians will have no incentive to help.

Reply to Objection 9: To be developed, QED does not need to attract the support of all or most mathematicians. If only a tenth of one percent of mathematicians could be attracted, that will probably be sufficient. And in compensation for the extra work currently associated with entering formal mathematics in proof checking systems, we can point out that some mathematicians may find the following benefit sufficiently compensatory: in formally expressing mathematics, one's own thoughts are often sharply clarified. One often achieves an appreciation for subtle points in proofs that one might otherwise skim over or skip. And the sheer joy of getting all the details of a hard theorem `exactly right', because formalized and machine checked, is great for many individuals. So we conjecture that enough mathematicians will be attracted to the endeavor provided it can be sufficiently organized to have a real chance of success.

Objection 10: The QED project represents an unreasonable diversion of resources to the pursuit of the checking of ordinary mathematics when there is so much profitably to be done in support of the verification of hardware and software.

Reply to Objection 10: Current efforts in formal, mechanical hardware and software verification are exceptionally introspective, focusing upon internal matters such as compilers, operating systems, networks, multipliers, and busses. From a mathematical point of view, essentially all these verifications fall into a tiny, minor corner of elementary number theory. But eventually, verification must reach out to consider the intended effect of computing systems upon the external, continuous world with which they interact. If one attempts to try to verify the use of a DSP chip for such potentially safety critical applications as telecommunications, robot vision, speech synthesis, or cat scanning, one immediately sees the need for such basic engineering mathematics as Fourier transforms, not something at which existing verification systems are yet much good. By including the rigorous development of the mathematics used in engineering, the QED project will make a crucial contribution to the advance of the verification of computing systems.

Objection 11: The notion that interesting mathematics can ever, in practice, be formally checked is a fantasy. Whitehead and Russell spent hundreds of pages to prove something as trivial as that 0 is not 1. The notion that computing systems can be verified is another fantasy, based upon the misconception that mathematical proof can guarantee properties of physical devices.

Reply to Objection 11: That many interesting, well-known results in mathematics can be checked by machine is manifest to those who take the trouble to read the literature. One can mention merely as examples of mathematics mechanically checked from first principles: Landau's book on the foundations of analysis, Girard's paradox, Rolle's theorem, both Banach's and Knaster's fixed point theorems, the mean value theorem for derivatives and integrals over Banach-space valued functions, the fundamental counting theorem for groups, the Schroeder-Bernstein theorem, the Picard-Lindelof theorem for the existence of ODEs, Wilson's theorem, Fermat's little theorem, the law of quadratic reciprocity, Ramsey's theorem, Godel's incompleteness theorem, and the Church-Rosser theorem. That it is possible to verify mechanically a simple, general purpose microprocessor from the level of gates and registers up through an application, via a verified compiler, has been demonstrated. So there is no argument against proof-checking or mechanical verification in principle, only an ongoing and important engineering debate about cost-effectiveness. The noisy verification debate is largely a comedy of misunderstanding. In reaction to a perceived sanctimony of some verification enthusiasts, some opponents impute to all enthusiasts grandiose claims that complete satisfaction with a computing product can be established by mathematical means. But any verification enthusiast ought to admit that, at best, verification establishes a consistency between one mathematical theory and another, e.g., between a formal specification of intended behavior of a system and a formal representation of an implementation, say in terms of gates and memory. Mathematical proof can establish neither that a specification is what any user `really wants' nor that a description of gates and memory corresponds to physical reality. So whether the results of a computation will be pleasing to or good for humans is something that cannot be formally stated, much less proved.
left right UP HOME RBJ created 31/12/95 modified 13/1/96 c