Your paper: Computer theorem proving in math

[Piotr Rudnicki <piotr@sedalia.cs.ualberta.ca>]

Dear Prof. Simpson:

I have read your paper on computer theorem proving with interest.
On p. 6 you write:

  The first major project involving a large number of people was Mizar;
  it is still ongoing, and led to the Journal of Formalized Mathematics
  which has been publishing articles verified in the MIZAR system since
  at least 1989. The mathematical orientation of most of the articles is
  a little bit far from the mainstream of what we call standard
  mathematics.

I think that AUTOMATH deserves the priority - in the 70's there was
about a dozen people involved in the project.

I wonder on which basis have you formed your opinion that "most of the
[Mizar] articles is a little bit far from the mainstream of what we
call standard mathematics".  

Most of Mizar articles concern the development of basic mathematical
toolkit - stuff that everybody knows but which cannot be even called
folklore as it is too basic.  However, there is quite a number of
developments that you should be aware of: translation of the theory of
continuous lattices, Jordan curve theorem, Groebner basis and many
more.  Longer reports about some of these have been published in
Journal of Symbolic Computation and Journal of Authomated Reasoning
(see http://www.cs.ualberta.ca/~piotr/Mizar for working copies of the
papers).  But to some degree you are right: the Mizar Library includes
quite a number of articles that should not have seen the day of light
ever, all these for some strange public relations reasons.

It has been a long standing (20 some years) opinion within the Mizar
group that without involving working mathematicians such projects are
doomed.  (We have had some short lived interest in Mizar by some big
names in recent mathematics and some quite hostile reactions too.)

I welcome your paper as it may attract working mathematicians towards
computerized proof assistants: Mizar, Coq, Isabelle or whatever, I do
not care.  However, Mizar library seems to be largest of such and I
think that building such a library is the main challenege, for it is
far from clear who will do it and who will pay for it at the large
scale as at the laboratory scale I do not see substantial obstacles
anymore.

Sincerely,

Piotr Rudnicki

CompSci, University of Alberta, Edmonton, Canada
http://web.cs.ualberta.ca/~piotr