Some info about the Mizar project is in my paper "An Overview of the Mizar
Project" available via anonymous ftp from
menaik.cs.ualberta.ca
129.128.4.241
in
/pub/Mizar/Mizar_Over.tar.Z
After uncompress and tar you get a directory Mizar_92BRA in which
you find TeX source of the paper. There is no .dvi or .ps file.
For more info you may write to:
Roman Matuszewski
Mizar Group
Institute of Mathematics
Warsaw University - Bialystok Branch
15-276 Bialystok
Poland
Roman will provide you with instructions how to get a copy of the system.
If there is sufficient interest I will make all texts from the Mizar
library available for anonymous ftp.
The Mizar Group runs Mizar Digest as a moderated mailing list in BITNET.
Everybody is welcome to join. Some fragments of the first issue of the Digest
are attached below.
I will be delighted to answer any questions.
-- Piotr (Peter) Rudnicki
=============================================================================== M M I ZZZZZ A RR DD I GGG EEEEE SSS TTTTT MM MM I Z AA R R D D I G E S T M M M M I Z A A R R D D I G GG EEE SS T M M M M I Z AAAA RRR D D I G G E S T M M M I ZZZZZ A A R R DDD I GGG EEEEE SSS T =============================================================================== 27 Jul 1993 Nr 1 moderator : L.Borys<mizar@plbial11.bitnet> =============================================================================== Current Mizar ver. 4.05 Current MML ver. 4.05
We start to publish "Mizar Digest". It will be distributed to all users subscribed to MIZAR at PLEARN.BITNET. The obvious purpose is to provide an opportunity to discuss various topics related to Mizar. Particularly: - the changes introduced in new Mizar version; - the development of the MML: new articles and revisions; - planned changes in the Mizar language Please feel free to send to Digest any criticism related to Mizar (it will be
published, if contains new arguments, of course), proposed development of the language, criticism of existing articles, the analyzes of the development of
a particular field of mathematics in MML (done on needed) etc. We will provided a sort of user service. You are encouraged to send questions related to formalization in Mizar of definitions, theorems, or proofs. Also please inform u s if you run into troubles. We will try to help, to advice how to cope with the problem or to fix the Mizar bug. Mizar Digest will be distributed every week. To facilitate to keep track we decided to publish the issue even it we have nothing to publish. However such an issue will include steady information: current version of Mizar and current version of MML. Mizar Digest will be published in (scientific pidgin) English. The correspondence should be sent to MIZAR at PLBIAL11.BITNET. Moderator