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?
|First||enumerate and describe the kinds of things that would be found in the QED system|
|Second||establish some `milestones' or some priority list of objectives|
|Third||to accumulate the basic mathematical texts that are to be formalized|
|Fourth||to achieve consensus about the statement of the most important definitions and theorems in mathematics|
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 systemCrucial 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.