In February of this year (2016), the Alfred P. Sloan Foundation sponsored a workshop at the Fields Institute about the development of a new 'language' to represent mathematics in computerized/formalized form.
The participants were 40 mathematicians, logicians, experts in computational mathematics and formalized mathematics.
Because bringing the approximate 100 million pages of peer-reviewed research mathematics into a modern, computer-understandable form will be a long term global effort (https://arxiv.org/abs/1404.1905), the Alfred P. Sloan Foundation also sponsored the making of a documentary-style video about the workshop; including participant interviews (e.g. with Ingrid Daubechies, Yuri Matiyasevich, Harvey Friedman, Stanislav Smirnov, Jeremy Avigad, Georges Gonthier) to foster a more global discussion on the subjects involved in developing such a new 'language'.
Topics such as: what is mathematics, why we need proofs, how to get more people involved in formal mathematics, what is the mechanized future of mathematics and others are discussed.
I was one of the workshop organizers, and we just finished editing a 90 min video ("Towards a Semantic Language of Mathematics") and it is now on Youtube: