1. Most of A. Trybulec's effort in Mizar has been on the systematic
reconstruction of the language of mathematics as used among the
mathematicians. This process is still in progress with no end in sight.
If we are ever to involve the mathematicians in the QED effort we
should have in mind that the the interface language to QED must
be close to the language of the working mathematician.
Mizar is still some distance away from this language, thoufh it can
be closer than other proof-checking systems.
I have a difficulty realising how the discussion on PRA or other
root logic relates to this issue.
2. During the workshop we tried to answer the question: Who are consumers
of QED? I do not remember much of this, and I do not have any notes.
Does anybody have?
My vision of QED consumers is kind of fuzzy mainly due to the following.
I do not see that I can
interest a working first-class mathematician in QED before QED
includes most of, say, high-school mathematics. And now I have to
come up with a scheme by which I get the high-school mathematics into
QED data base. Does anybody has an idea of how to do it?
-- Piotr (Peter) Rudnicki