The QED Manifesto @mime: mit Kommentaren von Michael Meyling, 2004-01-12@ The development of mathematics toward greater precision has led, as is well known, to the formalization of large tracts of it, so that one can prove any theorem using nothing but a few mechanical rules. -- K. Goedel If civilization continues to advance, in the next two thousand years the overwhelming novelty in human thought will be the dominance of mathematical understanding. -- A. N. Whitehead @mime: daran glaube ich nicht@ 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. @mime: ok@ 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. @mime: ok@ 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. @mime: ok@ 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. @mime: das glaube ich nicht: sicherlich ist es nicht notwendig die internen mathematischen Strukturen zu kennen, die nur für den Beweis eines Satzes benötigt wurden. In der Regel sind jedoch die Vorbedingungen des Satzes schon von diesen Strukturen geprägt. Auch zum Verständnis des Vier-Fabensatzes muss man elementare mathematische Strukturen und bestimmte Begriffe kennen. Ob die Begriffe richtig verwendet und die Vorbedingungen erfüllt werden - das muss bei der Anwendung des Satzes innerhalb des QEDEQ-Systems so detailiert angegeben werden, dass das QED-System eine Überprüfung vornehmen kann.@ 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. @mime: hoffe ich ja auch, aber ich glaube das ich hier auch zu optimistisch bin...@ 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. @mime: nein, das kann ich mir gar nicht vorstellen@ 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. @mime: daran mag ich auch nicht glauben, das klingt für mich wie ein KI-Glaubensbekenntnis..@ The third motivation for the QED project is education. @mime: ok@ Nothing is more important than mathematics education to the creation of infrastructure for technology-based economic growth. @mime: Vielleicht reicht da auch eine elementare mathematische Grundausbildung aus? Vielleicht gibt es auch noch andere wichtige Voraussetzungen? Ich fände es zwar gut wenn Mathematikausbildung der Hauptfaktor für das technologisch bedingte Wachstum ist, aber das ist - glaube ich - reines Wunschdenken.@ The development of mathematical ability is notoriously dependent upon ‘doing' rather than upon ‘being told' or ‘remembering'. @mime: vollkommen richtig!@ 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. @mime: glaub ich nicht, so ein System kann den Dialog mit einem guten Mathematiker nicht ersetzen. Das sind einfach unterschiedliche Aspekte. Das QED-System ist nur ein zusätzliches Werkzeug, das weitere Hilfsmittel bereitstellt.@ 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. @mime: im Prinzip richtig, aber Mathematik besteht nicht aus formalen Beweisen! Eine Beweisidee ist nichts formales und eine erste Beweisskizze auch nicht. Bis zu einem formal korrekten Beweis können noch megatonnen an Papier notwendig sein. Aber wie bereits geschrieben, als Hilfsmittel auch zum Lernen und Kontrollieren sollte das System unterstützend sein können.@ Today few students get a grasp of mathematics at a detailed level, but via experimentation with a computerized laboratory, that number will increase. @mime: und was soll das nützen?@ In fact, students can be used (eagerly, we think) to contribute to the development of the body of definitions and proved theorems in QED. @mime: klar@ 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 lok 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. @mime: was hat das mit dem QED-System zu tun. (Fällt mir gerade dazu ein: Haben die Sprachlabors im Englishunterricht den riesigen Durchbruch gebracht?)@ 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. @mime: ok, wobei das "beautiful" in den formalen Beweisen manchmal etwas fehlen kann...@ 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. @mime: klingt gut@ Fifth, the QED system may help preserve mathematics from corruption. @mime: ok@ We must remember that mathematics essentially disappeared from Western civilization once, during the dark ages. Could it happen again? @mime: das ist ein bisschen zu übertrieben..@ 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. @mime: z.B. eine zunehmende Anzahl von Sätzen, deren Beweise nur von ganz wenigen Mathematikern nachvollzogen werden konnten. In der Summe führt das sicherlich dazu, dass (wiedereinmal) Sätze als wahr angenommen werden, obgleich es nur fehlerhafte Beweise für sie gibt (da die Fehler nicht gefunden wurden). Das ist gerade bei der zunehmenden Anzahl und Komplexität der Mathematik unvermeidlich, wenn keine Automatisierung (z.B. durch das QED-System) greift.@ 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. @mime: ist das in der Physik wirklich so, wenn ja: hat das Auswirkungen auf die Mathematik? Zumindest das letztere glaube ich nicht.@ The QED system could offer an antidote to any such tendency. @mime: aber nur für die Mathematik (wo es meiner Meinung nach gar keine solche Tendenz gibt @ 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. @mime: klingt gut@ 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. @mime: Verdoppelungen und Überschneidungen wird es weiterhin geben (z.B. brauchen ja nur unterschiedliche Notationen oder leicht verschiedene Definitionen getroffen werden, das ist automatisch gar nicht zu finden). Allerdings ist es viel leichter möglich zu ermitteln, wer auf welchen Erkenntnissen aufgebaut hat. Die davon abhängenden Ergebnisse können dann viel leichter herausgefunden werden und daraus könnten sich in der Tat interessante Effekte ergeben.@ 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. @mime: klingt gut@ 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. @mime: ok@ 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. @mime: jup @ 2. Some Objections to the Idea of the QED Project and Some Responses ==================================================================== The peculiarity of the evidence of mathematical truths is that all the argument is on one side. There are no objections, and no answer to objections. -- J. S. Mill 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. First 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 thre 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. @mime: Mathematik wird (im Wesentlichen) ausschliesslich in der klassischen Logik betrieben. Das ist das was überall gelehrt und verwendet wird. Dann gibt es natürlich noch ein paar Enklaven... Für die kann natürlich auch ein System definiert werden. (Im Hilbert II Prototyp können beliebige Axiome vorgegeben werden, nur die Regeln sind nicht (vom Endbenutzer) änderbar.) Daher möchte ich mich zumindest zunächst (keine Ahnung was ich in 20 Jahren mache..) mit der klassischen Logik beschäftigen. Wenn es die klassische Logik nicht behindert, kann man das sicher so strukturieren das auch andere Systeme darauf aufbauen können. Unter "klasischer Logik" verstehe ich eine Prädikatenlogik erster Stufe mit Funktoren (wie in "Mengenlehre I"). @ For example, Goedel 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. @mime: es läßt sich eigentlich alles in der PL 1. Stufe ausdrücken. Und für die Betrachtung der höheren Ordnungen baut man das System eben von unten neu auf (mit den Mitteln der PL 1. Stufe werden Zeichensätze manipuliert, die höhere Stufen behandeln...). Dieser Zweig der Mathematik kommt meiner Einschätzung nach erst ganz am Ende, denn er gehört nicht zu den elementaren Grundlagen (Mengenlehre, Zahlentheorie, Algebra).@ Second Reply to Objection 1. These are controversies in the Philosophy of Mathematics. Who cares? The overwhelming majority of contemporary mathematicians believe that there are no doubts about what it means for a proof to be correct, and they agree on a vast common mathematical basis, much stronger than ZFC. If we do not get the mathematicians involved, the QED project will fail as well. But to get mathematicians involved, we have to find out how to talk to them. @mime; ganz genau!@ 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. @mime: richtig@ 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 mathemaics 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. @mime: exactly!@ 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. @mime: yep@ 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. @mime: falls etwas nicht einfach zu formalisieren ist, wird die Sprache (z.B. QEDEQ) erweitert. Genauso wird das ja in der Mathematik auch gemacht. Neue Definitionen, Abkürzungen, Regeln etc.. Entscheidend ist, dass jederzeit eine *automatische* Rückführung in die orginale Syntax möglich ist (konserative Erweiterung). Dazu kann man auch den folgenden "Trick" anwenden: Wir schaffen ein System das "Symbole" bzw. "Symbolketten" als Subjektkonstanten besitzt und als Verknüfungskonstante die "Hintereinanderschreibung" besitzt. Dann definiert man wie üblich auf diesem Zeichenkettenuniversum ein Kalkül (das ist der Formel- und Beweisanteil aus der QEDEQ-Syntax und Semantik) und beweist diverse Sätze und insbesondere Regeln dafür. Durch dieses Kalkül im Kalkül können dann problemlos Metaregeln des inneren Kalküls verwendet werden, da diese Metaregeln ja im (primitiven) äußeren Kalkül bewiesen worden sind... Das ist jetzt etwas verkürzt dargestellt, vielleicht an anderer Stelle mehr...@ 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 QEDrelated projects at their inception, and rapid communication between most mathematics and computer science departments through email, telnet, and ftp has become almost universal. @mime: soweit ok@ 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. @mime: tja, das letzte ist wohl noch nicht ganz so gelöst. Ich denke das Babel-Symptom ist das größte Hindernis@ 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. @mime: ja, die Jugend soll es wieder (kostengünstig) richten...@ 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. @mime: klingt gut@ Objection 7. Good mathematicians will never agree to work with formal systems because they are syntactically so constricting as to be inconsistent with creativity. @mime: das scheint mir der wichtigste Einwand bisher zu sein!@ 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, .... @mime: stimmt!@ 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. @mime: genau so ist es!@ The developers of proof checking and theorem-proving systems have done little towards making their syntax tolerable to mathematicians. @mime: sind eben Informatiker ;-)...@ 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 computerhuman interface for mathematics is something easily within the grasp of current computer theory and technology. The work of Knuth on Tex and the widespread adoption of Tex by mathematicians and mathematics journals demonstrates that it is no problem for computers to deal with any known mathematical notation. @mime: hatte ich ja auch schon mal so angedeutet...@ 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. @mime: (?? ->) QEDEQ -> LaTeX@ 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. @mime: zumindest *lokal* "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. @mime: stimmt, wichtigstes Ergebnis von QED wird dann ja auch eine einheitlichere Notation sein@ 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. @mime: genau, am Ende der mathematischen Entwicklung steht die Übertragungsaufgabe; es geht um die formale Notation und die Verfügbarkeit in dieser Form und nicht um die Neuentdeckungen@ 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. @mime: genau!@ 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. @mime: sollte für Hilbert II auch gelten@ 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. @mime: so it is@ 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 foreeable 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. @mime: ein frommer Wunsch, aber warum gerade 10 Prozent? Sollen 10% für die gesamte Mathematik ausreichen? Das ganze ist ja ein dynamischer Prozess, bei dem man mit ganz wenigen Leuten starten kann und sich dann steigert. Vielleicht gibt es ja auch Berufsbilder wie z.B. "Beweisformalisierer" ;-)@ 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. @mime: ich glaube nicht, dass ein "ausgewachsener" Mathematiker das noch nötig hat. Die Formalisierung der Beweise ist eine zusätzliche Arbeit, die sich für den Mathematiker, der gerade an einem Teilgebiet arbeitet, zunächst nicht rentiert. Er kann dann nur später sagen: und ausserdem sind meine Ergebnise auch formal korrekt mit dem QED-System abgeleitet worden. Damit haben es dann andere Mathematiker leichter - und werden eventuell etwas stärker an den Ergebnissen interessiert sein. Aber zunächst und vor allem ist es eine ungeheure zusätzliche Arbeit!@ One often achieves an appreciation for subtle points in proofs that one might otherwise skim over or skip. @mime: über fremde formale Beweise skipt man besonders schnell. Bei eigenen Beweisen dient das QED-System sicherlich dazu, weniger Fehler zu machen. Und dann bemerkt man sicherlich manchmal einige "subtle points" die man bisher übersehen hat.@ 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. @mime: .. aber sicherlich nicht für die Mehrheit aller Mathematiker@ 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. @mime: glaube ich auch. Ausgehend von einer Keimzelle von ein paar Leuten sollten dann sukzessive neue Leute begeistert werden.@ 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. @mime: seh ich überhaupt nicht als sinnvoll an, das als Ziel für das QED-System festzuschreiben. Meiner Meinung nach sollte es ausschliesslich um Mathematik gehen. Ob dann ein paar Brocken auch für die Korrektheitsprüfungen von Soft- und Hardware abfallen ist mir egal. Insbesondere möchte ich keine Rückkopplung in Form von bestimmten Anforderungen, die aus dieser Ecke kommen könnten, haben. Wenn man wirtschafliche Unterstützung aus der Ecke haben will, dann kommt man da sicher nicht drum rum, aber für mich ist das auch nur ein konstuierter Grund: Ich denke dass die dort notwendigen Korrektheitsprüfungen ein ganz eigenständiges Thema sind, mit dem sich das QED-System nicht belasten sollte.@ 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. @mime: die Folgerung ist Quatsch. Das hängt einfach von der Erweiterungsfähigkeit der formalen Sprache ab. Wenn es die gibt und die Erweiterungen nah an dem "normalen" Umgang liegen, dann ist die Formalisierung ohne grosse Probleme auch leistbar.@ The notion that computing systems can be verified is another fantasy, based upon the misconception that mathematical proof can guarantee properties of physical devices. @mime: dem letzteren Einwand kann ich fast komplett zustimmen, wenn ich auch die Begründung ein wenig anders wählen würden: Korrektheitsprüfungen von Programmen war eine "Modekonzept" (um 1990???), dass - meiner Vermutung nach - inzwischen als gescheitert angesehen werden kann. "Normale" Computersysteme haben eine viel zu hohe Anzahl von Zuständen und ein so komplexes Abhängigkeitsverhalten (auch z.B. das Zeitverhalten), das sich eine simple Korrektheitsprüfung nicht durchführen lässt. Es kann noch nicht einmal eine komplette Systembeschreibung geben, so dass allein deshalb eine Verifkation nicht möglich ist.@ 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. @mime: gleich der erste Satz eine Breitseite...@ 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, Goedel's incompleteness theorem, and the Church-Rosser theorem. @mime: ok@ 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 ben 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. @mime: wie bereits oben beschrieben@ Objection 12. The QED Manifesto is too long. Its length will interfere with the establishment of the project by driving away potential supporters and contributors. Reply to objection 12. Objection 12 is largely correct. For an initial reading, it is suggested that sections 4 and 5 below be skipped. On the other hand, we believe that there is real value in recording the many views on this subject, even views that are clearly refutable. @mime: Länge ist nicht unbedingt schlimm. Kommt auf die Schreibe an. Wenn das wichtigste auch schon oben steht ist gegen Länge nichts einzuwenden.@ 3. Some Background, Being a Critique of Current Related Efforts =============================================================== Although the root of logic is the same for all, the ‘hoi polloi' live as though they have a private understanding. -- Heraclitus 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. @mime: das ist bei solchen Mamutprojekten die Regel. Wenn in kleinen Vorprojekten begonnen und die Projektgröße langsam gesteigert wird, dann lassen sich solche Effekte abmildern. Falls jedoch das Ziel ist, auch später alle demokratisch zu befrieden, dann ist jedes Projekt dieser Größenordnung zum Scheitern verurteilt.@ 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. @mime: if ..@ 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. @mime: ok, mal sehen was weiter unten kommt@ 1. Too much code to be trusted. There have been a number of automated reasoning systems that have checked many theorems of interest, but the amount of code in some of these impressive systems that must be correct if we are to have confidence in the proofs produced by these systems is vastly greater than the few pages of text that we wish to have as the foundation of QED. @mime: könnte ein Argument sein@ 2. Too strong a logic. There have been many good automated reasoning systems that ‘wired in' such powerful rules of inference or such powerful axioms that their work is suspect to many of those who might be tempted to contribute to QED -- those of an intuitionistic or constructivist bent. @mime: das betrifft nur eine absolute Minderheit der Gesamtmathematiker@ 3. Too limited a logic. Some projects have been developed upon intuitionistic or constructive lines, but seem unlikely, so far anyway, to support also the effective checking of theorems in classical mathematics. @mime: das kann gut sein, wenn unter "logic" auch fehlende Metaregeln verstanden wird.@ We regard this ‘boot-strapping problem' -- how to get, rigorously, from checking theorems in a weak logic to theorems in a powerful classical logic, in an effective way -- to be a key unsolved technical obstacle to QED. We discuss it further below. @mime: dazu hatte ich oben schon etwas skizziert (System im System.@ 4. Too unintelligible a logic. Some people have attempted to start projects on a basis that is extremely obscure, at least when observed by most of the community. We believe that if the initial, base, root logic is not widely known, understood, and accepted, there will never be much enthusiasm for QED, and hence it will never get off the ground. It will take the cooperation of many, many people to build the QED system. @mime: genau! Deshalb sollten die Metaregeln ja eng am "normalen Vorgehen" orientiert sein.@ 5. Too unnatural a syntax. Just as QED must support a variety of logics, so too must it support a variety of syntaxes, enough to make most groups of mathematicians happy when they read theorems they are looking for. It is unreasonable to expect mathematicians to have to use some computer oriented or otherwise extremely simplified syntax when concentrating on deep mathematical thoughts. Of course, a rigorous development of the syntaxes will be essential, and it will be a burden on human readers using the QED proof tree to ‘know' not only the logical theory in which any theorem or procedure they are reading is written but also to know the syntax being used. @mime: auch das stimmt! Eventuell muss es vorverarbeitende System geben (e.g. LaTeX -> QEDEQ).@ 6. Parochialism. There are many projects that have started over from scratch rather than building upon the work of others, for reasons of remoteness, ignorance of previous work, personalities, unavailability of code due to intellectual property problems, and issues of grants and publications. We are extremely sensitive to the fact that the issue of credit for scientific work in a large scale project such as this can be a main reason for the failure of the QED project. But we can be hopeful that if a sufficient number of scientists unite in supporting the QED project, then partial contributions to QED's advancement will be seen in a very positive light in comparison to efforts to start all over from scratch. @mime: es gibt in der Tat sehr viele Gründe ein Projekt von grund auf neu zu starten. Das ist aber ein sehr weites Feld...@ 7. Too little extensibility. In 20 years there have been perhaps a dozen major proofchecking projects, each reprsenting an enormous amount of activity, but which have ‘plateaued out' or even evaporated. It seems that when the original authors of these systems cease actively working on their systems, the systems tend to die. Perhaps this problem stems from the fact that insufficient analysis was given to the basic problems of the root logic. @mime: Meiner Ansicht nach sind die bisherigen Systeme zu "unmathematisch" gewesen und haben sich zusehr an der Informatik orientiert. Auch der Lambda-Kalkül muss einem "normalen" Mathematiker nicht bekannt sein. Damit haben sich immer nur spezielle Lösungen ergeben, in die einzuarbeiten andere keine Lust hatten.@ Without a sufficient amount of extensibility, everyone so far seems to have reached a point in which checking new proofs is too much work to do by machine, even though one knows that it is relatively easy for mathematicians to keep making progress by hand. The reason, we suspect, is that mathematicians are using some reflection principles or layers of logics in ways not yet fully understood, or at least not implemented. Mathematicians great contribution has been the continual re-evaluating, re-conceptualizing, connecting, extending and, in cases, discarding of theorems and areas. So each generation stands on the shoulders of the giants before, as if they had always been there. We are far from being able to represent mechanically such evolutionary mathematical processes. Existing mathematical logics are typically as ‘static' as possible, often not even permitting the addition of new definitions! Important work in logic needs to be done to design logics more adaptable to extension and evolution. @mime: genauso ist es! Die Syntax, insbesondere die Metaregeln müssen ständig weiterentwickelt werden, damit ein vernüftiges und "normales mathematisches" Arbeiten mit dem System möglich bleibt.@ 8. Too little heuristic search support. While it is in principle possible to generate entries in the QED system entirely by hand, it seems extremely likely that some sort of automated tools will be necessary, including tools that do lots of search and use lots of heuristics or strategies to control search. Some systems which have completely eschewed such search and heuristic techniques might have gotten much further in checking interesting theorems through such techniques. @mime: das ist mir noch nicht ganz klar: diese Heuristiken und Suchstrategien sollen wozu dienen?@ 9. Too little care for rigor. It is notoriously easy to find ‘bugs' in algorithms for symbolic computation. To make matters worse, these errors are often regarded as of no significance by their authors, who plead that the result returned is true ‘except on a set of measure zero', without explicitly naming the set involved. The careful determination, nay, even proof, of precisely which conditions under which a result is true is essential for building the structure of mathematics so that one can depend on it. The QED system will support the development of symbolic algebra programs in which formal proofs of correctness of derivations are provided, along with the precise statement of conditions under which the results are true. @mime: das habe ich auch schon mehrfach gehört. Aber es geht eigentlich doch nicht um Software wie "Derive" oder "Mathematica", die irgendwelche Terme umformen und darstellen können. Sondern um Theoremprüfer (und vielleicht auch Theoremfinder). Die Software, die dazu zum Einsatz kommt, muss in der Tat höchsten Korrektheitsansprüchen genügen. Das ist in der Tat ein Thema, dem genügend Aufmerksamkeit gewidmet werden muss. Dabei können u.a. auch verschiedenen Implementationen des Systems hilfreich sein.@ 10. Complete absence of inter-operability. One safe generalization about current automated reasoning or symbolic computation systems is that it is always somewhere between impossible and extremely difficult to use any two of them together reliably and mechanically. It seems almost essential to the inception of any major project in this area to choose a logic and a syntax that is original, i.e., incompatible with other tools. @mime: daher möchte ich mich möglichst stark an dem "üblichen Mathematikervorgehen" orientieren.@ One major exception to this generalization is the base syntax and logic for resolution systems. Here, standard problem sets have been circulated for years. But even for such resolution systems there is no standard syntax for entering problems involving such fundamental mathematical constructs as induction schemas or set-builder notation. @mime: selbst bei starker Orientierung am mathematischen Standard wird es schwierig sein, mit der unglaublichen Anzahl von Definitionen (und Metaregeln) zurechtzukommen. Z.B. bei der Verwendung des Symbols für die 1, welches in Verschiedenen Zusammenhängen (natürliche Zahlen, ganze Zahlen, rationale Zahlen, reelle Zahlen oder gar irgendein Ring) verschiedenes bedeutet. Daher ist es äußerst wichtig, dass solche Definitionen leicht gefunden werden können. Im Prinzip entspricht das ja auch dem normalen Vorgehen, dass eine Referenz angegeben wird, allerdings gilt das bei formalen Systemen auch für sehr viele dem "normalen Mathematiker" "selbstverständlichen" Sachen. Da ist meines Erachtens im Zusammenhang mit der Vorverarbeitung (also dem Bringen in das formale System) einiges möglich. 11. Too little attention paid to ease of use. The ease of use of automated reasoning systems is perhaps lower than for any other type of computing system available! In general, while anyone can use a word processor, almost no one but an expert can use a proof checker to check a difficult theorem. Perhaps this can be explained by the fact that the designers of such systems have had to put so much of their energies and attention into rigor, that they simply did not have enough energy left for good interface design. @mime: ich glaube gerne, dass das User-Interface nicht schön und bei allen Systemen verbesserungswürdig ist (s.o.), aber ich denke auch, dass es *prinzipiell* auch nicht möglich ist, ein simples Benutzerinterface anzubieten. Denn Mathematik *benötigt mehr als viele andere Disziplinen* Gehirnschmalz und das drückt sich letztlich auch im Benutzerinterface aus.@ 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. @mime: sollte so sein!@ 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. @mime: stimmt@ 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. @mime: unbedingt!!!@ 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 =========================================== Method consists entirely in the order and disposition of the objects towards which our mental vision must be directed if we would find out any truth. We shall comply with it exactly if we reduce involved and obscure propositions step by step to those that are simple, and then starting with the intuitive apprehension of all those that are absolutely simple, attempt to ascend to the knowledge of all others by precisely similar steps. -- R. Descartes 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. @mime: das ist eine gute Idee. Die "root logic" muss ja mit Zeichenketten als Subjekte umgehen können, um dann Metaregeln beweisen zu können. In Hilbert II will ich erst einmal mit der notwendigen mathematischen Logik anfangen. Diese "root logic"-Geschichte erfordert meines Erachtens einen ziemlich hohen Aufwand. Dafür soll es in Hilbert II ja (wie im Prototypen bereits realisiert) eine Rückführung auf die Grundregeln geben. Das reicht später nicht mehr aus, da allein schon die Rückführung in primitiver Notation (z.B. ohne die aufzählende Mengenschreibweise) Formeln ziemlich unlesbar machen. Später kann dann auch *innerhalb* von Hilbert II eine root logic entwickelt werden@ In the end, it will be the ‘social process' of mathematical agreement that will lead to confidence in the implementations of these proofcheckers 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. @mime: diese "root logic" ist nichts für "normale" Mathematiker, denn da geht es um die (rekursive) Fundierung der formalen Sprache und ihrer Metaregeln. Das Thema kann man viel später angehen. Viel wichtiger ist die Festlegung der Regeln, die im täglichen Gebrauch zum Einsatz kommen. Also von der Klassenschreibweise bis zur Anwendung der vollständigen Induktion.@ 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. @Ja, für die "root logic" mag das gelten, aber bitte nicht für die, mit der wir starten um die Mathematik zu dokumentieren. Es gibt einfach einen Standard, und den legen wir bis in die formal notwendigen Details fest.@ 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 ofinstantiation, 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. @mime ... kann ich alles nachvollziehen für die "root logic". Meiner Ansicht nach sollte die "root logic" im Wesentlichen Aussagen über Zeichen, Zeichenketten und Mengen von Zeichenketten treffen können. Welche Art von Mengenlehre da vonnöten ist, kann empirisch ermittelt werden: alles das, was z.B. benötigt wird, um die in dem Skript "Mengenlehre I" vorkommenden Axiome, Definitionen, Notationen, Regeln und Metaregeln anwenden und beweisen zu können. Das ist, glaube ich, viel weniger als ZFC, NBG oder MK.@ 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 loic 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. @mime: genau diese "reflection" ist das, was in Hilbert II in den Metaregeln passiert. Nur das dieses alles nicht automatisch sondern händisch (programmiert) gemacht wird. (Die Metaregeln sind programiert, die Rückführung auf die primitivere Stufe ist dann natürlich automatisch.)@ 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. @mime: für das Hilbert II Projekt nicht so ein Problem: die "root logic" muss sich nur mit dem QEDEQ-Format beschäftigen. Das führt zu einer Normierung!@ 6. What Is To Be Done? ====================== The idea is to make a language such that everything we write in it is interpretable as correct mathematics ... This may include the writing of a vast mathematical encyclopedia, to which everybody (either a human or a machine) may contribute what he likes. The idea of a kind of formalized encyclopedia was already conceived and partly carried out by Peano around 1900, but that was still far from what we might call automatically readable. -- N. G. de Bruijn 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 agreemen 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 @mime: bis hier hin sind wir schon fast... ;-)@ @mime: begin of skip@ - decision procedures - theorem-proving programs - symbolic computation procedures - modeling software - simulation software - tools for experimentation - numerical analysis software - graphical tools for viewing mathematics @mime: end of skip@ - interface tools for using the QED system @mime: was noch kein Interface-Tool ist, aber dennoch "lebenswichtig" ist meines Erachtens die Erzeugung von HTML oder LaTeX-Dokumentationen.@ 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. @mime: ja, ja - das kommt auch noch alles auf uns zu..@ 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. @mime: genau!@ 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. @mime: ja, stimmt@ 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. @mime: stimmt, aber zunächst einmal geht es ja um die Dokumentation von *bestehendem* mathematischem Wissen. Und das kann ja (theoretisch) jeder Student in eine entsprechend formalisierte Form bringen...@ 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. @mime: ich würde mich freuen, wenn wir je dieses organisatorsche Problem bekommen würden.@ 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 emailble. @mime: gilt für das QEDEQ-Format im Wesentlichen.@ It has been suggested that the QED system should include historical information. @mime: der LaTeX-Anteil in QEDEQ-Dateien dient u.a. auch dazu.@ 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. @mime: meine Meinung: Mengenlehre, Zahlentheorie, Algebra. Danach kann man fast schon wieder von vorn anfangen, denn diese Reihung bezieht sich nur auf die allerelementarsten Grundlagen.@ Non-Copyright: This document is in the public domain and so unlimited alteration, reproduction, and distribution by anyone are permitted. Authorship: This preliminary discussion of project QED (very tentative name) is an amalgam of many ideas that many people have had and for which perhaps no one alive today deserves much credit. We are deliberately avoiding any authorship or institutional affiliation at this early stage in the project (and may decide to do so forever) in the hope that many will want to join in the project as principals, even as originators (to the extent that anyone alive today could be thought to be an originator of this project). Some of those involved in the project would much rather that QED be completed than that they, as individuals, be lucky enough to partake significantly in the project, much less get any public credit for its completion. It may seem paranoid to avoid personalities, but we are inspired by the extraordinary cooperation achieved in the Bourbaki series in an atmosphere of anonymity. Version of May 15, 1994. An 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.