I am a training Algebraic Geometer, and am currently trying to prepare a course on category theory. I would be really thankful if people could tell me about "realmath" applications of theorems about monads which they came across during their career.

3$\begingroup$ By "application", do you mean "example"? It seems to me often useful to notice something is a monad or an adjunction, even if I then don't quote any theorems about general monads in attacking the problem at hand $\endgroup$– Yemon ChoiCommented Dec 26, 2011 at 13:13

1$\begingroup$ I would be interested if there is a realworld theorem where knowing that something is a monad facilitates finding the morally correct proof. $\endgroup$– LukasCommented Dec 26, 2011 at 13:28
4 Answers
The abstract algebra of monads is similar to the algebra of monoids, so that constructions on monoids often suggest similar constructions on monads. This applies in particular to bar constructions.
A pretty striking application in its time was the use of bar constructions on monads to construct deloopings. Around 1963, Stasheff identified the extra structures on Hspaces $X$ that need to hold in order to construct a single delooping $X \simeq \Omega Y$ compatible with the Hspace structures. This was at a time before there were such things as operads and their associated monads. But by the time May's The Geometry of Iterated Loop Spaces had appeared, there was appreciation of the algebra of operads and monads to economically package the panoply of algebraic operations that obtain on iterated loop spaces. In particular, the twosided bar constructions for monads and their algebras, similar to the Milgram bar construction for monoids, were used to give conceptually simple constructions for iterated deloopings, extending the constructions of Stasheff to much more general contexts.

1$\begingroup$ Indeed, monads and monoids are both types of categorical monoids. Because, as we know "A monad is monoid in the category of endofunctors. What's the problem?" $\endgroup$ Commented Dec 4, 2015 at 1:41
Forgetting or ignoring category theory (I hardly knew any in 1971), as Todd says I used monads concretely and constructively to manufacture spaces Y such that $\Omega ^n Y$ is equivalent to $X$, where $X$ is a space with an action by a suitable operad. Operads encode lots of operations, and their associated monads coalesce all those operations into a single operation, the product of the monad. (The portmanteau word operad combines operation and monad, inspired by this connection and by Lewis Carroll). This concrete coalescence of information is the essence of many, but by no means all, applications of monads. In iterated loop space theory, the combinatorial monads associated to operads mesh with the more abstract monads $\Omega^n\Sigma^n$ associated to the adjoint pair of functors $(\Sigma^n,\Omega^n)$.
Monads are very useful in computer science, specifically logic programming. Haskell is a programming language which is extremely mathematical, to the point where programs and proofs are the same thing. It's a pure functional programming language, which means everything is a function and these functions are not allowed to have sideeffects (you can't cheat to make Haskell do something for you). So it should not come as a surprise that ideas from category theory lead to new ways to do things in Haskell. Monads are used in just this way, to get Haskell to do more things than you can get without monads. For example, recursive things. Monads are so useful that someone has website containing a big list of things known to be monads. I saw this website in a talk given by Emilio Gallego, a student of Jim Lipton. I believe there is a link to it from here.
The discussion of monads on wikipedia is very good. You can see all the terms from categorical monads popping up in that article, and facts about monads from category theory often lead to new programs in Haskell and other programming languages. Another nice overview is this pdf. An article written for computer scientists is here.
If someone with more expertise comes along and wants to add to this answer, please do.

1$\begingroup$ «it should not come as a surprise that ideas from category theory lead to new ways to do things in Haskell.» Why shouldn't it? When these ideas started to show up, everyone was pretty surprised! $\endgroup$ Commented Dec 26, 2011 at 17:16

1$\begingroup$ @Mariano: I agree that my wording there is not optimal. I suppose the amount of surprise depends on how the material is presented. I was not all that surprised because the lecturer was building towards this punchline. I'm sure that people who studied Haskell before this connection had been established were much more surprised, otherwise it would have been established much earlier! $\endgroup$ Commented Dec 26, 2011 at 18:22
I would say first that monads are useful in that they offer a level of abstraction that can be used to describe lots of different algebraic phenomena. That is, categories of groups, abelian groups, rings, commutative rings,... can each be described equivalently as categories of algebras over some monad acting on sets (see Lawvere Theory for more examples). There are monads that don't arise in this way, but typically most examples are pretty close to this. So in one sense the theorems that are true in all of these situations are most naturally proven in the language of monads and their categories of algebras.
One of the other ways they show up in 'real math' is via the following: there is always a forgetful functor from the category of $T$algebras in $\scr{C}$ to $\scr{C}$ with a left adjoint, the free $T$algebra functor. This forgetful functor must also preserve and reflect certain coequalizer diagrams. In a precise sense (see Monadicity theorem) we can identify whether or not a functor is a forgetful functor from a category of algebras over some monad by these properties. This gives a useful criterion for seeing whether or not something is in the image of such a functor and what are the maps between such objects. This (or its dual formulation) gives descent type theorems, which is probably what algebraic geometers care most about. These theorems will generally tell you something like when is the category of sheaves of some type equivalent to a category of descent data of a very particular form.
I would recommend looking at Borceux's 'Handbook of Categorical Algebra' Vol. 2 Ch. 4 for more details. I'm sorry that I don't have a more geometric reference at hand.

3$\begingroup$ Just to amplify on Justin's answer slightly: the natural "geometric function theories" in algebraic geometry, i.e. categories of quasicoherent or coherent sheaves, categories of Dmodules, categories of $\ell$adic sheaves, etc. come with direct and inverse image functors of various kinds that have adjoints on one side or another. So one naturally has (co)monadic structure from thatI personally view this as a fundamental organizing principle. There are then many ways to play descenttype games in this setting; a very powerful recent tool is Lurie's BarrBeck theorem for $\infty$cats. $\endgroup$ Commented Dec 28, 2011 at 14:46