In a recent paper Marc Lange gives an account of what constitutes an explanatory proof in mathematics.
Non-explanatory proofs are typically brute-force computations that do not illuminate why the theorem holds, but rather “makes it seem like an accident of algebra, as it were” (16), “supplies ‘little understanding’ and fails to show ‘what’s going on’” (20). Everyone agrees thus far.
Explanatory proofs tend to be more conceptual, as Lange's examples show. In my view, the right way to characterise how these proofs differ from the non-explanatory ones are in terms of cognisability, as I have argued elsewhere.
But Lange has a different proposal. He argues that if a result has a notable symmetry to it then an explanatory proof must itself involve this symmetry in an essential way: “A proof that exploits the symmetry of the setup is privileged as explanatory” (18) and “only a proof exploiting such a symmetry in the problem is recognized as explaining why the solution holds” (19). Lange later generalises from this to allow any “salient feature” of the theorem to take the role of symmetry in this argument (28).
In my view this proposal is off the mark. I say that if a proof is cognisable it would typically count as explanatory, regardless of whether it exploits symmetry properties of the result or not.
An example illustrating this is the proof of the equality of the coordinate and cosine forms of the scalar product.
In my calculus book I prove this in a cognisable way. I start with the geometrical idea of a projection, and I show through intuitive-visual reasoning how this leads to the coordinate form. This is an explanatory proof, in my opinion.
The standard proof in other textbooks is to start with the coordinate form and derive the cosine form using the law of cosines. This is obviously extremely unsatisfactory, since the law of cosines is a “black-box,” algebraic hocus-pocus result. This is a prototypically non-explanatory proof, in the sense of the quotations from Lange above.
Yet according to Lange’s proposal it is the latter proof that is the explanatory one. For the result is certainly symmetric, and the standard proof likewise respects this symmetry throughout.
My proof, on the other hand, is most definitely asymmetrical: it involves the projection of one vector onto another, an asymmetrical relation. Thus my proof actually introduces an asymmetry that was not in the result itself. And it was precisely this move that made the proof congnisable, and thereby explanatory, in my view. Which is the exact opposite of what Lange’s proposal says should happen.