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 | Too much code to be trusted |
---|---|
2 | Too strong a logic |
3 | Too limited a logic |
4 | Too unintelligible a logic |
5 | Too unnatural a syntax |
6 | Parochialism |
7 | Too little extensibility |
8 | Too little heuristic search support |
9 | Too little care for rigour |
10 | Complete absence of inter-operability |
11 | Too little attention paid to ease of use |
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.
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.
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. 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.
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.
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.
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.
7. Too little extensibility. In 20 years there have been perhaps a dozen major proof-checking projects, each representing an enormous amount of activity, but which have `plataued 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. 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.
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.
9. Too little care for rigour. 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.
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. 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.
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.