Re: [mizar] Mizar-like proofs

[John Harrison <John.Harrison@cl.cam.ac.uk>]

Hi Josef,

| At http://citeseer.ist.psu.edu/huang94reconstructing.html is an article, 
| where the Mizar "by" proof granularity seems to be largely reinvented. 
| Was Mizar that much unknown in 1994?

Yes! It now seems incredible/lamentable, but the system was then almost
entirely unknown among what one might call the "mainstream" automated
theorem proving community, even though it had a large and thriving
international user community.

The fact that it became better-known is due in no small part to the
efforts of Bob Boyer as part of the QED project. I'm pretty sure that
the first time I heard the name Mizar was in this message from him:

  http://icml.stanford.edu/~uribe/mail/qed.messages/105.html

It was only following the second QED workshop in 1995 that I visited
Bialystock and used the system for the first time. I was immediately
impressed and soon investigated copying the proof style in HOL:

  http://www.cl.cam.ac.uk/users/jrh/papers/mizar.html

Several others have followed in assimilating features of Mizar's proof
language into other systems. Most notably, the Mizar-inspired "Isar" mode
for Isabelle is now that system's main proof language. But there are 
probably other things we still ought to learn from Mizar!

John.