A version of this appeared as "The QED Manifesto" in "Automated Deduction - CADE 12", Springer-Verlag, Lecture Notes in Artificial Intelligence, Vol. 814, pp. 238-251, 1994. Authorship and copyright information for this document may be found at the end. ## The QED Manifesto
## 1. What Is the QED Project and Why Is It Important?QED is the very tentative title of a project to build a computer system that effectively represents all important mathematical knowledge and techniques. The QED system will conform to the highest standards of mathematical rigor, including the use of strict formality in the internal representation of knowledge and the use of mechanical methods to check proofs of the correctness of all entries in the system. The QED project will be a major scientific undertaking requiring the cooperation and effort of hundreds of deep mathematical minds, considerable ingenuity by many computer scientists, and broad support and leadership from research agencies. In the interest of enlisting a wide community of collaborators and supporters, we now offer reasons that the QED project should be undertaken. First, the increase of mathematical knowledge during the last two hundred years has made the knowledge, let alone understanding, of all, or even of the most important, mathematical results something beyond the capacity of any human. 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. Remarkably, however, the creation of mathematical logic and the advance of computing technology have also provided the means for building a computing system that represents all important mathematical knowledge in an entirely rigorous and mechanically usable fashion. The QED system we imagine will provide a means by which mathematicians and scientists can scan the entirety of mathematical knowledge for relevant results and, using tools of the QED system, build upon such results with reliability and confidence but without the need for minute comprehension of the details or even the ultimate foundations of the parts of the system upon which they build. Note that the approach will almost surely be an incremental one: the most important and applicable results will likely become available before the more obscure and purely theoretical ones are tackled, thus leading to a useful system in the relatively near term. Second, the development of high technology is an endeavor of fabulously increasing mathematical complexity. The internal documentation of the next generation of microprocessor chips may run, we have heard, to thousands of pages. The specification of a major new industrial system, such as a fly-by-wire airliner or an autonomous undersea mining operation, is likely to be even an order of magnitude greater in complexity, not the least reason being that such a system would perhaps include dozens of microprocessors. We believe that an industrial designer will be able to take parts of the QED system and use them to build reliable formal mathematical models of not only a new industrial system but even the interaction of that system with a formalization of the external world. We believe that such large mathematical models will provide a key principle for the construction of systems substantially more complex than those of today, with no loss but rather an increase in reliability. As such models become increasingly complex, it will be a major benefit to have them available in stable, rigorous, public form for use by many. The QED system will be a key component of systems for verifying and even synthesizing computing systems, both hardware and software. The third motivation for the QED project is education. Nothing is more important than mathematics education to the creation of infrastructure for technology-based economic growth. The development of mathematical ability is notoriously dependent upon "doing" rather than upon "being told" or "remembering". The QED system will provide, via such techniques as interactive proof checking algorithms and an endless variety of mathematical results at all levels, an opportunity for the one-on-one presenting, checking, and debugging of mathematical technique, which it is so expensive to provide by the method of one trained mathematician in dialogue with one student. QED can provide an engaging and non-threatening framework for the carrying out of proofs by students, in the same spirit as a long-standing program of Suppes at Stanford for example. Students will be able to get a deeper understanding of mathematics by seeing better the role that lemmas play in proofs and by seeing which kinds of manipulations are valid in which kinds of structures. Today few students get a grasp of mathematics at a detailed level, but via experimentation with a computerized laboratory, that number will increase. In fact, students can be used (eagerly, we think) to contribute to the development of the body of definitions and proved theorems in QED. Let also us make the observation that the relationship of QED to education may be seen in the following broad context: with increasing technology available, governments will look not only to cut costs of education but will increasingly turn to make education and its delivery more cost-effective and beneficial for the state and the individual. Fourth, although it is not a practical motivation, nevertheless perhaps the foremost motivation for the QED project is cultural. Mathematics is arguably the foremost creation of the human mind. The QED system will be an object of significant cultural character, demonstrably and physically expressing the staggering depth and power of mathematics. Like the great pyramids, the effort required (especially early on) may be great; but the rewards can be even more staggering than this effort. Mathematics is one of the most basic things that unites all people, and helps illuminate some of the most fundamental truths of nature, even of being itself. In the last one hundred years, many traditional cultural values of our civilization have taken a severe beating, and the advance of science has received no small blame for this beating. The QED system will provide a beautiful and compelling monument to the fundamental reality of truth. It will thus provide some antidote to the degenerative effects of cultural relativism and nihilism. In providing motivations for things, one runs the danger of an infinite regression. In the end, we take some things as inherently valuable in themselves. We believe that the construction, use, and even contemplation of the QED system will be one of these, over and above the practical values of such a system. In support of this line of thought, let us cite Aristotle, the Philosopher, the Father of Logic, "That which is proper to each thing is by nature best and most pleasant for each thing; for man, therefore, the life according to reason is best and pleasantest, since reason more than anything else is man." We speculate that this cultural motivation may be the foremost motivation for the QED project. Sheer aesthetic beauty is a major, perhaps the major, force in the motivation of mathematicians, so it may be that such a cultural, aesthetic motivation will be the key motivation inciting mathematicians to participate. Fifth, the QED system may help preserve mathematics from corruption. We must remember that mathematics essentially disappeared from Western civilization once, during the dark ages. Could it happen again? We must also remember how unprecedented in the history of mathematics is the clarity, even perfection, that developed in this century in regard to the idea of formal proof, and the foundation of essentially the entirety of known mathematics upon set theory. One can easily imagine corrupting forces that could undermine these achievements. For example, one might suspect that there is already a trend towards believing some recent "theorems" in physics because they offer some predictive power rather than that they have any meaning, much less rigorous proof, with a possible erosion in established standards of rigor. The QED system could offer an antidote to any such tendency. The standard, impartial answer to the question "Has it been proved?" could become "Has it been checked by the QED system?". Such a mechanical proof checker could provide answers immune to pressures of emotion, fashion, and politics. Sixth, the "noise level" of published mathematics is too high. It has been estimated that something between 50 and 100 thousand mathematical papers are published per year. Nobody knows for sure how many contain errors or how many are repetitions, but some pessimists claim the number of both is high. QED can help to reduce the level of noise, both by helping to find errors and by helping to support computer searches for duplication. Seventh, QED can help to make mathematics more coherent. There are similar techniques used in various fields of mathematics, a fact that category theory has exploited very well. It is quite natural for formalizers to generalize definitions and propositions because it can make their work much easier. Eighth, by its insistence upon formalization, the QED project will add to the body of explicitly formulated mathematics. There is mathematical knowledge that is neither taught in classes nor published in monographs. It is below what mathematicians call "folklore," which is explicitly formulated. Let us call this lower level of unformulated knowledge "mathlore". In formalization efforts, we must formalize everything, and that includes mathlore lemmas. Ninth, the QED project will help improve the low level of self-consciousness in mathematics. Good mathematicians understand trends and connections in their field. The QED project will enable mathematicians to analyze, perhaps statistically, the whole structure of the mathematics, to discover new trends, to forecast developments and so on. ## 2. Some Objections to the Idea of the QED Project and Some Responses
## 3. Some Background, Being a Critique of Current Related Efforts
In some sense project QED is already underway, via a very diverse collection of projects. Unfortunately, progress seems greatly slowed by duplication of effort and by incompatibilities. If the many people already involved in work related to QED had begun cooperation twenty-five years ago in pursuing the construction of a single system (or federation of subsystems) incorporating the work of hundreds of scientists, a substantial part of the system, including at least all of undergraduate and much of first year graduate mathematics and computer science, could already have been incorporated into the QED system by now. We offer as evidence the nontrivial fragments of that body of theorems that has been successfully completed by existing proof-checking systems. The idea of QED is perhaps 300 years old, but one can imagine tracing it back even 2500 years. We can agree that many groups and individuals have made substantial progress on parts of this project, yet we can ask the question, is there today any project underway which can be reasonably expected to serve as the basis for QED? We believe not, we are afraid not, though we would be delighted to join any such project already underway. One of the reasons that we do not believe there is any such project underway is that we think that there exist a few basic, unsolved technical problems, which we discuss below. A second reason is that few researchers are interested in doing the hard work of checking proofs - probably due to an absence of belief that much of the entire QED edifice will ever be constructed. Another reason is that we are familiar with many automated reasoning projects but see very serious problems in many of them. Here are some of these problems.
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11. ## 4. The Relationship of QED to Artificial Intelligence (AI) and to Automated Reasoning (AR)Project QED is largely independent of the question of the possibility or utility of artificial intelligence or automated reasoning. To the extent that mechanical aids of any kind can be used to help construct (or shorten) entries in the QED system, we can be appreciative of such aids, even if the aids use techniques that are from the realms of artificial intelligence, assuming of course that what the aids suggest doing is verifiably correct. A key fact is that it will not matter, from the viewpoint of soundness, whether proofs were added to the QED system by humans, dumb programs, smart programs or some combination thereof. All of the QED system will be checkable by a simple program, from first principles. The QED system will focus on what is known in mathematics, both theorems and techniques, rather than upon the problems of discovering new mathematics. It is the view of some of us that many people who could have easily contributed to project QED have been distracted away by the enticing lure of AI or AR. It can be agreed that the grand visions of AI or AR are much more interesting than a completed QED system while still believing that there is great aesthetic, philosophical, scientific, educational, and technological value in the construction of the QED system, regardless of whether its construction is or is not largely done "by hand" or largely automatically. ## 5. The Root Logic - Some Technical Details
An important early technical step will be to "get off the ground", logically speaking, which we will do by rooting the QED system in a "root logic", whose description requires only a few pages of typical logico-mathematical text. As a model for brevity and clarity, we can refer the reader to Goedel's presentation, in about two pages, of high-order logic with number theory and set theory, at the beginning of his famous paper on undecidable questions. The reason that we emphasize succinctness in the description of the logic is that we hope that there will be many separate implementations of a proof checker for this "root logic" and that each of these implementations can check the correctness of the entire QED system. In the end, it will be the "social process" of mathematical agreement that will lead to confidence in the implementations of these proof-checkers for the root logic of the QED system, and multiple implementations of a succinct logic will greatly increase the chance this social process will occur. It is crucial that a "root logic" be a logic that is agreeable to all practicing mathematicians. The logic will, by necessity, be sufficiently strong to check any explicit computation, but the logic surely must not prejudge any historically debated questions such as the law of the excluded middle or the existence of uncountable sets. As just one hint of a logic that might be used as the basis of QED, we mention Primitive Recursive Arithmetic (PRA) which is the logic Skolem invented for the foundations of arithmetic, which was later adopted by Hilbert-Bernays as the right vehicle for proof theory. It has also been further developed by Goodstein. In PRA one finds (a) an absence of explicit quantification, (b) an ability to define primitive recursive functions, (c) a few rules for handling equality, e.g., substitution of equals for equals, (d) a rule of instantiation, and (e) a simple induction principle. One reason for taking such a logic as the root logic is that it is doubtful that Metamathematics can be developed in a weaker logic. In any root logic one needs to be able to define, inductively, an infinite collection of terms and, inductively, an infinite collection of theorems, using in the definition of "theorem" such primitive recursive concepts as substitution. Thus PRA has the bare minimum power we would need to "get off the ground". Yet we think it suffices even for checking theorems in classical set theory, in a sense we describe below. The logic FS0, conservative over PRA, but with sets and quantifiers, has been proposed by Feferman as a vehicle more congenial than PRA for studying logics. It is probably the case that the syntax of resolution theorem-proving is the most widely used and most easily understood logic in the history of work on mechanical theorem-proving and proof checking, and thus perhaps a resolution-like logic could serve as a natural choice for a root logic. Some may object on the grounds that resolution, being based upon classical first order logic, "wires in" the law of the excluded middle, and therefore is objectionable to constructivists. In response to this objection, let us note that constructivists do not object to the law of the excluded middle in a free variable setting if all of the predicates and function symbols "in sight" are recursively defined; for example, it is a constructive theorem that for all positive integers x and y, x divides y or x does not divide y. Thus we might imagine taking as a root logic resolution restricted to axioms describing recursive functions and hereditarily finite objects, such as the integers. The lambda-calculus-based "logical frameworks" work in Europe, in the de Bruijn tradition, is perhaps the most well developed potential root logic, with several substantial computer implementations which have already checked significant parts of mathematics. And already, many different logics have been represented in these logical frameworks. As a caution, we note that some may worry there is dangerously too much logical power in some of these versions of the typed lambda calculus. But such logical frameworks give rise to the hope that the root logic might be such that classical logic could simply be viewed as the extension of the root logic by a few higher-order axioms such as (all P) (Or P (Not P)). One possible argument in favor of adopting a root logic of power PRA is that its inductive power permits the proof of metatheorems, which will enable the QED system to check and then effectively use decision procedures. For example, the deduction theorem for first order logic is a theorem of FS0, something not provable in some logical framework systems, for want of induction. Regardless of the strength or weakness of the root logic chosen, we believe that we can rigorously incorporate into the QED system any part of mathematics, including extremely non-constructive set theoretic arguments, because we can represent these arguments "one level removed" as "theorems" that a certain finite object is indeed a proof in a certain theory. For example, if we have in mind some high powered theorem, say, the independence of the continuum hypothesis, we can immediately think of a corresponding theorem of primitive recursive arithmetic that says, roughly, that some sequence of formulas is a proof in some suitable set theory, S1, of another theorem about some other set theory, where a, say, primitive recursive proof checker for S1 has been written in the root logic of QED. In practice, it will be highly advantageous if we make it appear that one isn't really proving a theorem of proof theory but rather is proving a theorem of group theory or topology or whatever. Although many groups have built remarkable theorem-proving and proof checking systems, we believe that there is a need for some further scientific or computational advances to overcome some "resource" problems in building a system that can hold all important mathematics. Simply stated, it appears that complete proofs of certain theorems that involve a lot of computation will require more disk space for their storage than could reasonably be expected to be available for the project. The most attractive solution to such a problem is the development of "reflection" techniques that will permit one to use algorithms that have been rigorously incorporated within QED as part of the QED proof system. Although we have spoken of a single root logic, we need to make clear that we do not want to fall into the trap of searching for a single, ideal logic. We can easily imagine that it will be possible to develop several different root logics each of which can be fully regarded to be "a" foundation of QED, each of which is capable as acting as a basis for the other, and each of which has very short implementations which have been checked by the "social process". And each of which can be used to check the correctness of the entire QED system. In any case, it is a highly desireable goal that a checker for the root logic can be easily written in common programming languages. The specification should be so unambiguous that many can easily implement it from its specification in a few pages of code, with total comprehension by a single person. It has been argued that the idea of having multiple logics in addition to the root logic is a mistake that will result in too much complexity, and that it would be far more sensible to have a single logic in which proofs were clearly flagged with an indication of the assumptions used, so that a single logic could be enjoyed by people of both classical and constructive persuasions. Certainly such a single logic is desireable, but whether such a single logic can be developed is a serious question given that some famous constructive theorems (such as the continuity of all functions on the reals) are classical falsehoods. It has been argued that the idea of searching for a single logic or a single computer system is inferior to the idea of developing translation mechanisms that would permit proof checking systems to exchange proofs with one another. If this were feasible, it would certainly permit an alternative, distributed approach to achieving the major QED objectives. However, the history of radical incompatibility of many proof checking systems does suggest that such translation mechanisms may be difficult to produce. In seeking a root logic, it is clear that there will be many controversies that will be impossible to resolve to everyone's satisfaction. For example, there seems no hope of satisfying in a single logic those who insist upon a typed syntax and those who loathe typed syntax, preferring to do typing internally, e.g., with sets. There are also simple questions not yet resolved after centuries of thought, such as the semantics of a function applied outside its domain, e.g., division by zero. ## 6. What Is To Be Done?
Leadership. It seems certain that inviting deliberation by many interested parties at the planning stage is important not only to get the QED project off on a correct footing but also to encourage many to participate in the project. Until we can establish general agreement within a large, critical mass of scientists (including many distinguished mathematicians) that the QED project is probably worth doing, and until a basic "manifesto" agreeable to them can be drafted, possibly using parts of this document as a starting point, it is not clear whether there will be any further progress on this project. Given the extraordinary scope of this project, it is also essential that research agency leadership be obtained. It is perhaps unlikely that any one agency would be willing to undertake the funding of the entirety of such a large project. So an agreement by many agencies to cooperate will probably be essential. The requirements for leadership, both by scientists and by research agencies, are so major that it is perhaps premature to speculate about what other things should be done, in what order. Nevertheless, we will speculate about a few issues. What planning steps should be taken to start the QED project? An obvious first concern is to enumerate and describe in some detail the kinds of things that would be found in the QED system, including - logics
- axioms
- definitions
- theorems (including an analysis of the major parts of mathematics)
- proofs
- proof-checkers
- decision procedures
- theorem-proving programs
- symbolic computation procedures
- modeling software
- simulation software
- tools for experimentation
- numerical analysis software
- graphical tools for viewing mathematics
- interface tools for using the QED system
Crucial to this initial high level organization effort is deciding what parts of mathematics will be represented, how that mathematics will be organized, and how it will be presented. It is conceivable that years of consideration of these points should precede implementation efforts. One can imagine that a re-organization of mathematics on the order of the scope of the Bourbaki project is necessary. One can imagine major projects in the development of formal "higher-level" languages in which mathematics can be formally discussed and major projects devoted simply to writing the most important theorems, definitions, and proof sketches in such languages. Because different proofs of the same theorem can differ substantially in complexity, and because entering formal proofs into a proof checking system is very expensive, it is highly cost effective to consider many proofs of a theorem before setting out to verify one of them. It has been suggested by several people that a useful and relatively easy early step would be to assemble, in ftp-able form, a comprehensive survey of the parts of mathematics have been checked by various automated reasoning systems. A second planning step would be to establish some "milestones" or some priority list of objectives. For example, one could attempt to outline which parts of mathematics should be added to the system in what order. Simultaneously, an analysis of what sorts of cooperation and resources would be necessary to achieve the earlier goals should be performed. A third planning step would be to accumulate the basic mathematical texts that are to be formalized. It is entirely possible that the QED project will greatly overlap with an effort to build an electronic library of mathematical information. It is not part of the idea of a library that the documents should be in any particular language or subjected to any sort of rigor check. But it would of great inherent value, and great value to the QED project, to have the important works of mathematics available in machine readable form and organized for ease of access. A fourth planning step would be to attempt to achieve consensus about the statement of the most important definitions and theorems in mathematics. Until there is agreement on the formalization of the basic concepts and theorems of the important parts of mathematics, it will be hardly appropriate to begin the difficult task of building formal proofs of theorems. The formalization of statements is an extremely difficult and error-prone activity. Although the scientific obstacles to building QED are formidable, the social, psychological, political, and economic obstacles seem much greater. In principle, we can imagine a vast collection of people successfully collaborating on such an effort. But the problems of actually getting such a collaboration to occur are possibly insurmountable. "Why," an individual researcher could well ask, "should I risk my future by working on what will be but a small part of a vast undertaking? What sort of recognition will I receive for contributing to yet one more computing system?" These are good questions, and it is not clear what the answer is. To a major extent, status in mathematics and computing is a function of publications in major journals - status for research funding, status for tenure decisions, status for promotion. It is far from clear how contributing pieces to the QED system could provide a substitute for such signs of status. Perhaps here research agencies or even university faculties and administrators could be of assistance in establishing a new societal framework in which such cooperation was encouraged. Even given the cooperation of all the necessary people and assuming good luck in overcoming scientific hurdles, there are many issues of a very difficult but somewhat mundane character involving: version control, distribution, and support. A system with hundreds of contributors will create management difficulties perhaps not even imaginable to the small groups of researchers who have worked in the past on parts of the QED idea. It has been suggested about the low-level QED data files that they should be humanly readable and permit comments, and that the character set should be email-able. It has been suggested that the QED system should include historical information. Although such information would obviously not be something that would be mechanically checkable, it could provide extremely valuable contextual information to those trying to learn mathematics from the system, just as the commentaries on Euclid make his Elements intelligible to the modern reader. Strenuous disputes over priority in all forms of discovery, including mathematics, are common, and therefore care must be taken that the QED system permit the presentation of all sides of such disputes. It has been suggested that it would be best if QED focused initially on one part of mathematics, namely ring theory.
To join an Internet electronic discussion group devoted to the QED project, send a message with the single line subscribe qed to majordomo@mcs.anl.gov. The line above should be the content of the message, not the subject line. The subject line is ignored. An archive of this discussion group is in the directory /pub/qed/archive/ available by anonymous ftp from info.mcs.anl.gov. Version of May 15, 1994. |