1 | Paradoxes, Incompatible Logics, etc. |

2 | Intellectual property problems. |

3 | Too much mathematics. |

4 | Mechanically checked formality is impossible. |

5 | If QED were feasible, it would have already been underway several decades ago. |

6 | QED is too expensive. |

7 | Good mathematicians will never agree to work with formal systems. |

8 | The QED system will be large, and hence, unreliable. |

9 | The cooperation of mathematicians is essential but mathematicians will have no incentive to help. |

10 | QED 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 |

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.

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.