Explaining the main ideas of proof before giving details I'll be the first to admit that this is a risky question to try to get away with on math overflow, but I'm going to give it a shot anyway.
Roughly speaking, the question is this: Is it good to try to explain the main ideas of a complicated proof before giving the details?
One the one hand, the naive answer might be "Yes of course, why wouldn't you want it explained in clear language before you have to go through  the fiddly computation or tricky argument". But this seems not to actually hold up to much scrutiny... because well...It's actually relatively rare to do so. Papers are full of tricky, fiddly, deep and complicated proofs in which the authors don't try to outline the argument in more natural language. Should they? Why don't they?


*

*Is it just bad writing? 

*Or is it an example of over-adherence to formal style that harms the richness and intelligibility of the literature? (this retired MO classic comes to mind: What are some examples of colorful language in serious mathematics  papers? )

*Is it because to do it, we'd have to make the mathematics less precise and we just hate doing this?

*Or is it because: (and this might be the real reason I think this question is interesting):
when done only quite well but not brilliantly, it can actually make
it harder to understand the proof: Somehow you might expect to gain
clarity by reading the more top-level description of the proof, but
actually it is mired in the way the math seems or feels on a more intuitive level to the author, which just might not click with you  (cf. Thinking and Explaining ). 

*Another blander aspect is: It takes up space. I sometimes get into a period of a few weeks where I do it to a few of the proofs in a paper and then later I cut them all out again because the paper has gotten long.


Similar to, but not the same as: When to postpone a proof?
 A: Yes.  And No.
There are times when the goal is to establish a result for later use (rather than just to understand the object and its properties claimed by a result).  Here a reasonable goal is to say why it is used, but if the proof seems unrelated to the later use, it can impede understanding.  So instead of explaining why or how the result is true, explain instead why or how the result is useful.
Sometimes the proof is complicated and you want to do a test run: explain why A implies B and B implies C and C implies D. This was done quite effectively in the FGKT paper (or is it now FGKMT?) on large gaps between consecutive primes, where they started (effectively) with C implies D, to show why C was a reasonable goal, and then B and then A as progressive milestones, which to me helped motivate the probabilistic methods used in the proof.  You dole out the tricky parts between the implications after you have made the goals understandable.
My acid test for mathematical writing is my ability to explain the result to someone else after I have read it once or twice.  This requires having the top level clear and easily digested, but also requires a clear connection between the top level intuition and the formal statement of the lemma, proposition, or theorem, AND it also requires some understanding of how to go about proving each such formal statement.
My acid test for solid software writing is to be able to simulate in my head a run and explain to myself why and how the data is transformed at  each instruction. For solid proof vetting, not only do I have to check each statement, I need a model of the situation that I can manipulate according to the statements made in the proof.
I think for clarity of communication that a good model of what is going on should be suggested, so reviewing the main steps of a proof is recommended.  However the goal may not be communication but robustness, in which case the big picture may work against verification.
Gerhard "Are You Teaching Or Building?" Paseman, 2018.05.24.
A: New proofs in combinatorics are usually interesting not only for the result, but for the technique. 
For example, a proof using a sign-reversing involution, a proof using a bijection, a proof using RSK and a proof using crystal graphs 
all mean something for proving Schur positivity. However, a crystal proof usually implies the existence of an RSK proof and a bijective proof. 
There are several open problems in my area that are of the form "find a proof using technique Y of statement X". Thus, when giving a proof of something, the main idea and technique used should perhaps even be in the abstract.
A: This is always helpful if the proof is long and complicated.
Some experts may need only this to understand the proof. Some people may read only some steps, once they have the general idea. Those who prefer to read only the full detail, can always skip this informal description. So I do not see any arguments against this, except the increased length of the paper. But this is rarely a problem. I usually do this in long papers.
A: This is a very interesting philosophical question about something perceived missing from common mathematical writing. Of course, each of us has different experience and baggage and can conjure different examples of this phenomenon, perhaps, extreme ones rather than statistically generic. Add to that different tastes in what constitutes "good" exposition and no wonder that this risks becoming a "subjective and argumentative" sort of quandary.
I would like to approach it in an epistemological way, by specifying a piece of "contrarian" positive evidence for evaluation and to invite analysis, in this instance, of whether presenting ideas before formal proofs (subjectively) adds to clarity of exposition or detracts from it, and other aspects of the value of two opposite styles of presenting proofs, "intuitive" vs "formal". I have in mind the following well-known textbook written from the "ideas first" perspective:


Robert Strichartz, The Way of Analysis. 


As the author comments in the introduction, he deliberately and manifestly followed the intuitive path, by presenting special cases of theories first, even if with little extra effort one can get much more general statements (sometimes reworked in a later chapter), by giving intuitive arguments examining whether and why a theorem might be true prior to a formal proof, and occasionally belaboring certain points of the proofs at the risk of overdoing it. To be clear, complete proofs are provided (or deferred to exercises) after the underlying ideas have been clearly identified and examined, which sometimes necessitates performing additional technical work and also results in a certain amount of repetition.     
By a way of contrast, here is an example of a mainstream formal approach: 


Walter Rudin, Principles of Mathematical Analysis.


As an interesting sociological observation, I have noted vastly different reactions regarding the relative merits of these two textbooks, both from professors and students in Honors Real Analysis courses at Cornell where one or the other is often used as a required text.
A: I honestly just don't know. Of course, including anything that can be skipped but can, in principle, help at least someone into the paper cannot be "bad", so the question is rather whether it is practically possible and whether it is worth the effort. The proofs are (normally) designed to unfold as logic towers in which you cannot often even formulate the next step before you digested (some of) the previous ones. You are lucky if all you need from the previous part is a concisely formulated lemma or formula (some people insist that you should always try to make it the case but I'm often failing quite miserably on that account). In this case you can just write the sequence of statements and delegate the proofs to the subsequent sections. However often (especially if the paper is 40+ pages long) you need to immerse the reader into some general atmosphere, associations, and way of thinking before you can really say something with the hope that it will be comprehended at the level beyond formal verification. Alas, as I said once, there is no language for communicating those three directly and you often have to indirectly derive them from chains of two-line formulae with 6-10 different objects in each. 
You should keep in mind that I'm writing to convey techniques. The results do not matter: they are marble statues to admire or ready stones to fill some holes in the walls with. In both cases they may be aesthetically pleasing and even useful, but hardly interesting by themselves. What interests me and what I'm trying to learn from and pass to others are fancy twists, unexpected moves, etc, and more often than not the best way to demonstrate such a thing is just to perform it from the beginning to the end. The only way to simplify then is to perform the trick on some model case where at least some of the difficulties of the real problem are still present. Choosing a good simplified model is an art and often requires at least as much time and effort as doing the whole thing (unless you arrived at the proof by figuring out some model first; then, again, your life is easy: just write the exposition for the model before going into the hard stuff).
As to styles, etc., the resulting style is always a compromise between the writer's style, the styles of his co-authors, the patches done to satisfy the reviewers, not to mention the contributions of overzealous editors (Journal d'Analyse is quite something in this respect: they have some guy who feels like his sacred duty is to edit everything from commas to the formulations of the theorems, and I'm not entirely sure he is really qualified to do either; to his credit I should say that he doesn't make any fuss when you request reverting to the original version, but it is always a funny experience to look at your own text after he has worked on it). So I doubt stylistic considerations play much role here. Still, one of my friends always criticizes me for trying to explain how I thought of this or that when writing. He insists that people think of and view things differently and such explanations can only perplex them. I respectfully disagree (I'm always  happy to learn the thinking ways of others if they are any good for problem solving, and that others can figure out something I cannot is a sure certification that they are) but he may have his point, especially when teaching students is concerned (he is a much better teacher than what I can hope to be in my wildest dreams) and that activity is not too far from writing papers.
A: It would not be unprecedented to have a complete and correct proof accompanied by an incorrect intuition, the incorrectness of which becomes evident only after the passage of some time.  I strongly suspect that authors are sometimes averse to revealing too much about their intuitions for fear of looking foolish in the future.
