| Proposition: The purpose of the QED project is to mechanize the algebra
| of proofs in working mathematics. For this purpose, the language
| of ordinary mathematics suffices and there is no need to adopt
| any meta-mathematical framework.
I might agree if by "purpose" you mean "ultimate goal". In much the same
way the purpose of AI is to produce machines that can hold an everyday
conversation with a human being, but experience shows that it's wise for
AI to lower its sights. In the same way, computerizing even a more
stylized subset of natural language, viz. the "mathematical vernacular",
may be well-nigh impossible in the foreseeable future.
This is not to say that a metamathematical framework is necessarily
called for. However at the workshop there seemed to be a clear majority
(everyone except me, in fact!) in favour of such a scheme. Certainly it
offers many interesting challenges, although I can understand that it
might try the patience of those mathematicians uninterested in logic.
John.