More generally, say we want to prove a theorem that looks something like “If A, then B has property C.” You start at A and, appealing to the definition of C, show that B has it. There’s probably some cleverness involved in doing so, but you start at the obvious place (A), end in the obvious place (B satisfies the definition of C), and don’t rely on any crazy, seemingly-unrelated insights. Let’s call this sort of proof mundane.
There is a virtue in mundane proofs: a smart reader can usually generate them after they read the theorem but before they read its proof. Doing is beneficial, since proof-generating makes the theorem more memorable. It also gives the reader practice building intuition by playing around with the mathematical objects and helps them improve their proofwriting by comparing their output to a maximally refined proof.
On the end of the spectrum opposing mundane is witchcraft. Proofs that use witchcraft typically have a step where you demonstrate you’re as ingenious as Pascal by having a seemingly-unrelated insight that makes everything easier. Notice that, even if you are as ingenious as Pascal, you won’t necessarily be able to generate these insights quickly enough to get through the text at any reasonable pace.
I’m skeptical that this is a huge problem in practice,and my hunch is that this is mostly a matter of the original proof being badly conveyed. In the case of Pascal ingenuious proof of the gambler’s ruin, what the exposition in MCS isn’t conveying clearly enough is that we’re essentially defining a “game” (or more subtly, a valuation) as f([gambler’s capital]) that is fair in the expectation sense, and, more importantly, results in “ruin” or “win” exactly when the original game does. If you start with a proof of this statement, you’re back in the familiar pattern of “If A, then B has property C”. We’ve just inserted a simple step of “Actually, we’ll just need to show that B’ has property C, and then B does too”, which is mundane, because it just follows from what C is like!
The point though is that not all expositions make this obvious enough; some just focus on proofs that are “mundane” in your original sense, but this too is a kind of “dumbing down” and lack of mathematical maturity.
I’m skeptical that this is a huge problem in practice,and my hunch is that this is mostly a matter of the original proof being badly conveyed. In the case of Pascal ingenuious proof of the gambler’s ruin, what the exposition in MCS isn’t conveying clearly enough is that we’re essentially defining a “game” (or more subtly, a valuation) as f([gambler’s capital]) that is fair in the expectation sense, and, more importantly, results in “ruin” or “win” exactly when the original game does. If you start with a proof of this statement, you’re back in the familiar pattern of “If A, then B has property C”. We’ve just inserted a simple step of “Actually, we’ll just need to show that B’ has property C, and then B does too”, which is mundane, because it just follows from what C is like!
The point though is that not all expositions make this obvious enough; some just focus on proofs that are “mundane” in your original sense, but this too is a kind of “dumbing down” and lack of mathematical maturity.