left right UP

Some Objections to the Idea of the QED Project and Some Responses

1Paradoxes, Incompatible Logics, etc.
2Intellectual property problems.
3Too much mathematics.
4Mechanically checked formality is impossible.
5If QED were feasible, it would have already been underway several decades ago.
6QED is too expensive.
7Good mathematicians will never agree to work with formal systems.
8The QED system will be large, and hence, unreliable.
9The cooperation of mathematicians is essential but mathematicians will have no incentive to help.
10QED would divert resource more profitably employed in support of the verification of hardware and software.
11 The notion that interesting mathematics can ever, in practice, be formally checked is a fantasy
UP 1.
This objection is worth answering, but I find the answer given unconvincing.

The claims in the objection, with the sole exception of the very last one (no widely agreeable logic), are false and should be refuted. If the QED project is not able to agree on a single logical foundation on which to base its work then it is unlikely to do much worthwhile mathematics.

The answer appears to be that QED will be based on a new generic proof checker which will simultaneously be used to implement a variety of different kinds of mathematics on a variety of logical foundations.

Jack of all trades, master of none. How many of the proof tools most often used on real world problems are generic tools?

If one of the problems QED is intended to solve is the dissipation of effort resulting from work on too many diverse approaches to "the problem", then this answer suggests that QED will in fact provide a framework which supports rather than discourages diversity. I am not aware of any convicing evidence to support the claim that implementation of diverse logics within a common framework provides significant reuse of results between the distinct institutions.

UP 2.
Automation of mathematical problem solving through proof is potentially of very great economic significance. The current position in relation to IPR amounts to opting for funding, and hence control, by institutional rather than market mechanisms, and limits participation by individuals who prefer independence to institutionalisation.

Fortunately, putting everything in the public domain does not preclude commercial exploitation.

UP 3.
UP 4.
UP 5.
UP 6.
UP 7.
UP 8.
UP 9.
UP 10.
UP 11.


left right UP HOME RBJ created 5/1/96 modified 16/1/96 c