This is fascinating. If i had more time to get an articulate question i would, but I'm going to need to sit with this paper for a bit. Amazingly, I've been fooling around on the edges of thereom proving for a bit now and had yet to hear of the Mizar corpus. Really, really fascinating stuff.