(This started out as a comment and got way way way too long).
You may enjoy William Thurston's article On Proof and Progress in Mathematics.
Mathematics in some sense has a common language: a language of symbols, technical definitions, computations, and logic. This language efficiently conveys some, but not all, modes of mathematical thinking. Mathematicians learn to translate certain things almost unconsciously from one mental mode to the other, so that some statements quickly become clear. [...]
People familiar with ways of doing things in a subfield recognize various patterns of statements or formulas as idioms or circumlocution for certain concepts or mental images. But to people not already familiar with what’s going on the same patterns are not very illuminating; they are often even misleading. The language is not alive except to those who use it. [...]
We mathematicians need to put far greater effort into communicating mathematical ideas. To accomplish this, we need to pay much more attention to communicating not just our definitions, theorems, and proofs, but also our ways of thinking. We need to appreciate the value of different ways of thinking about the same mathematical structure.
We need to focus far more energy on understanding and explaining the basic mental infrastructure of mathematics—with consequently less energy on the most recent results. This entails developing mathematical language that is effective for the radical purpose of conveying ideas to people who don’t already know them.
Regarding the original question, there are papers that do not present ideas in the Definition-Theorem-Proof (DTP) format. Timothy Chow has a few papers that focus on communicating ideas (though they are not the first (or second) papers on the topic/result).
- You could have invented spectral sequences, Timothy Chow, Notices of the AMS
- Forcing for dummies, Timothy Chow
One possible reason for the prevalence of the DTP format is that we are all just used to it from books and papers. Reviewers (and readers) sometimes find non-standard writing style distracting. A middle ground is papers that gently break the reader into a result. There are papers that present a special case or a simple problem that illustrates the general idea.
- The Topological Structure of Asynchronous Computability, Maurice Herlihy and Nir Shavit. The paper has many illustrations and demonstrates the general idea for a simple protocol before applying the main theorem to solve some open problems.
- Logic and $p$ recognizable sets of integers, Véronique Bruyàre, Georges Hansel, Christian Michaux, and Roger Villemaire. A survey-style exposition of a beautiful result: the sets of natural numbers that are encodable by finite automata, independent of the base chosen are precisely those definable in Presburger arithmetic. The paper has numerous examples, covers special cases before the general case and provides historical background about erroneous proof attempts.
No discussion of a non-standard presentation of remarkable ideas would be complete without mentioning the work of Jean-Yves Girard. Unique is probably the best word to describe it (without being diplomatic or sarcastic). From, the paper Linear Logic.
The philosophical exegesis of Heyting’s rules leaves in fact very little room for a further discussion of the intuitionistic calculus; but has anybody ever seriously tried? In fact, linear logic, which is a clear and clean extension of usual logic, can be reached through a more perspicuous analysis of the semantics of proofs (not very far from the computer-science approach and thus relegated to the next section), or by certain more or less immediate considerations about sequent calculus. These considerations are of immediate geometrical meaning, but in order to understand them, one has to forget the intentions, remembering, with a Chinese leader, that it’s not the colour of the cat that matters, but the fact that it catches mice.
There are still people saying that , in order to make computer science, one essentially needs a soldering iron; this opinion is shared by logicians who despise computer science and by engineers who despise theoreticians. However, in recent years, the need for a logical study of programmation has become clearer and clearer and the linkage logic-computer-science seems irreversible.
In some sense , logic plays the same role as the one played by geometry w.r.t. physics: the geometrical frame imposes certain conservation results, for instance, the Stokes formula. The symmetries of logic presumably express deep conservation of information, in form which have not yet been rightly conceptualised.