Hi John,
| 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
Thanks for the pointer. The question is how much has changed during the 13 years since the message was written.
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!
And now that at least two good systems have both the 'writer-friendly' and the 'reader-friendly' proof styles, someone might implement serious transformation between them ;-). The paper I cited actually explores that.
Best, Josef