As a former professional mathematician: the benefits mentioned in the article (click-through definitions and statements, analyzing meta trends, version control, ...) do not seem particularly valuable.

The reason to formalize mathematics is to automate mathematical proofs and the production of mathematical theory.