I spent two weeks in Bialystok in the 1990's learning Mizar from Andrzej. He was a fascinating person (unfortunately he passed away two years ago). He was train

I spent two weeks in Bialystok in the 1990's learning Mizar from Andrzej. He was a fascinating person (unfortunately he passed away two years ago). He was trained as a topologist (under K. Borsuk, a well-known Polish mathematician) and got interested in linguistics. He told me that he started working on Mizar as an automated translation system 'from mathematics into English' and someone suggested that he added a proof checker. I think the result is very elegant. I always liked the way Mizar proofs look. Also, working on some relatively simple proofs, I got to appreciate how much is left unsaid in most mathematical papers. Some details I would consider trivial were anything but. I wish only that Mizar was GPL'd but according to Andrzej himself he wanted more control over his creation. I am not sure I would agree but I certainly respect his choice.