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.

created 31/12/95 modified 11/1/96