  In section 4 it was pointed out that two major forms of the search for explanations in mathematical practice occur at the level of comparison between different proofs of the same result and in the conceptual recasting of major areas. These two types of explanatory activity lead to two different conceptions of explanation. These conceptions could be characterized as local and global. The point is that in the former case explanatoriness is primarily a (local) property of proofs whereas in the latter it is a (global) property of the whole theory or framework and the proofs are judged explanatory on account of their being part of the framework. While these two types of explanatory activity do not exhaust the varieties of mathematical explanations that occur in practice, the contraposition between local and global captures well the major difference between the two major classical accounts of mathematical explanation, those of Steiner and Kitcher (more recent accounts will be discussed in section 7). While we shall emphasize the local/global dichotomy, it is important to add that there are other ways to conceptualize the major alternatives in the theory of mathematical explanation. For instance, Kim 1994 uses the contraposition between ‘explanatory internalism’ and ‘explanatory externalism’ to give a taxonomy of the different accounts of scientific explanation. Whereas for ‘explanatory internalism’ explanations are activities internal to an epistemic corpus (a theory or set of beliefs), an ‘explanatory externalist’ will look for some ontic relations that ground the explanatory relations reflected in linguistic ascriptions of explanatoriness. This taxonomy is orthogonal to the local/global taxonomy and we only mention here that the spirit of Kitcher’s theory of explanation is ‘internalist’ whereas that of Steiner is ‘externalist’.