What is the motivation behind formalizing a piece of mathematics in a system like Mizar? I ask as someone interested in the process. I mean it's not like anyone is going to read those formal proofs. It's not like they are going to be useful for anything other than building more useless unreadable proofs, or are they? I would love to be wrong, but how does formalizing mathematics contribute to human understanding of mathematics?