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 det

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/ http://www.mizar.org/