Whereas the interpretation of formal mathematical proof is a relatively straightforward process of rule-applicability verification that has been successfully automated by AI researchers, the interpretation of informal mathematical proof is a more complex process of guided observation, likened by Hardy (1928) to observing and focusing on the features of a distant mountain range, except that the observed entities are instantiations of mathematical schemas constructed and combined in the mind's eye.
These mathematical schemas have their grounding in components deriving from common human experience (Lakoff, 1987). The texts of mathematical definitions make reference to ordinary image-schemas (Johnson, 1987) but cause them to be modifed by either truncation, the removal of certain perceptual properties resulting in partial structure, or extension, the addition of certain procedural properties in an inductive way (see Kitcher, 1984). The geometric concept of POINT furnishes an example of truncation: all physical objects possess location, whereas a point is defined to possess location yet no physical extension.
In order to be convinced by a proof, the reader must perform an extended series of mental operations at each step. In addition to imagining and focusing on schematic structures, these operations typically require blending schemas held in mind with ones retrieved from either the immediate context of the proof or from the background system of schema definitions, possibly constructing counterfactual configurations, and looking for dissonance or its absence. My analysis demonstrates how the complexities of this process are similar to some of those that have been shown to exist in the interpretation of language and discourse.
This framework may be applied to understand certain trends in the development of mathematics, particularly, those which have been driven by disagreement over the convincingness of proofs. Such disagreements can be traced to difficulties in the guided construction and observation process, and resolutions typically take the form of modifications to the specifications of schemas or the methods used to combine them that simplify it.