A Critique of the QED Manifesto

Roger Jones

This is my personal reaction to the May 1995 version of the QED manifesto.

I am interested in the mechanisation of mathematics by proof, so my basic attitude towards "the QED project" is positive. I mention this because you might otherwise think that this critique is an aggressive attack trying to bury the whole idea. The critique is not just incomplete, but hardly started. I quickly realised that it was going to be too long a litany of negatives to contribute constructively to the project. I then decided that to make a positive contribution I needed to put together some kind of position statement which would enable me to offer constructive alternatives to the features of the manifesto which I disliked. So the critique was suspended until I had some written up some of my own positive ideas on the topic and still awaits (after three years!) my further attention.

I mention the two features of the QED manifesto which seem to me positive and important. Firstly, the implicit recognition that formal proof is central to the mechanisation of mathematics. Secondly the recognition that a great deal can be done in the mechanisation of mathematics through proof without having to solve the problem of machine intelligence.

This critique was produced along with a new HTML version of the manifesto and contains references to sections of the manifesto where this is helpful to the point I am making. I have followed the structure of the manifesto so that the critique can easily be related to the manifesto.

Throughout these comments, hyperlinks to relevant parts of the Qed manifesto are indicated thus: UP

  1. What Is the QED Project and Why Is It Important?
  2. Some Objections to the Idea of the QED Project and Some Responses
  3. Some Background, Being a Critique of Current Related Efforts
  4. The Relationship of QED to Artificial Intelligence (AI) and to Automated Reasoning (AR)
  5. The Root Logic---Some Technical Details
  6. What Is To Be Done?
  7. Copyright

UP HOME RBJ created 1995/12/31 modified 1998/8/13