  We study methods for automated parsing of informal mathematical expressions
into formal ones, a main prerequisite for deep computer understanding of
informal mathematical texts. We propose a context-based parsing approach that
combines efficient statistical learning of deep parse trees with their semantic
pruning by type checking and large-theory automated theorem proving. We show
that the methods very significantly improve on previous results in parsing
theorems from the Flyspeck corpus.
