Towards a Semantic Language of Mathematics

This film discusses the techniques, and outlines the vision of the future computerization of pure mathematics through interviews and talk segments from renowned mathematicians, meta-mathematicians, computational mathematicians, and theorem provers.