The Mizar proof system (2017)

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.

This actually look more approachable than other proof systems I've looked at. The included proof seems understandable though I'm not sure how all steps are deterministic, how they're sufficient to fully make the proof.

That said, there's a note at the bottom of the page saying: "(last modification 2002-01-29)" so perhaps "2002" would be a more appropriate date here? The Mizar system itself seems like it's being maintained presently, according to its website. http://www.mizar.org/

The theorem language I have heard most about lately is called Lean. Working number theorists are very active in developing it, driving to make it actually useful to write their theorems in it.