Zen and the art of formalisation.

Mathematics is a precise discipline, but mathematical rigor is not the same as logical formality. When one tries to translate a mathematical argument to a format suited for automated processing, one realizes that there is a tangible mismatch between a text-book presentation and what is actually required by the machine. Ordinary mathematics is simply too informal for the logical and algebraic procedures that contemporary au- tomated reasoning has to offer. At a linguistic level, ordinary mathematical discourse systematically overloads symbols and abuses notations in ways that make mechanical interpretation difficult. Subtle contextual cues are needed to resolve the ambiguities that are intrinsic to mathematical vernacular, requiring not just knowledge of the notation and conventions at play but, moreover, an understanding of the relevant mathematical discipline.