Boris, if you haven't done so already, you might want to try Freek Wiedijk's tutorial: http://www.cs.ru.nl/~freek/mizar/mizman.pdf This is slightly out of date. The differences between it and the current Mizar version just add to the fun, however. Best, James