Have you solved problems in your sleep? I have hit upon major (for me—relative to my trivial accomplishments)
insights in my research
in various sleep-deprived altered states of consciousness,
e.g., long solo car-drives extending through the night into the morning.
But I have never actually solved a problem in my sleep.
I have awakened thinking That's it!, but never was it actually it.
Q. Can anyone report an actual significant advance in their research
that occurred during and emerged from their sleep?
Of course this is entirely subjective, but you would know it if it happened to you.
Poincaré's famous step onto the bus in 1908
("At the moment when I put my foot on the step the idea came to me...")
indicates significant unconscious processing,
and his insomnia account (quoted below) adds further credence to
such "background" processing.
But I am not aware of first-hand reports of
significant and accurate reasoning
occurring during sleep.


One evening, contrary to my custom, I drank black coffee and could not sleep. Ideas rose in crowds; I felt them collide until pairs interlocked, so to speak, making a stable combination. ... (Link)


 A: This BBC article mentions the Ramanujan story, with other examples from the arts and science, and is followed by readers giving their own examples. One conclusion to draw from this, is that quite often the "discovery in a dream" is just made up. Kekulé's well-known story how he discovered the ring structure of Benzene in a dream may be just an anecdote.
A: In a dream I saw such a vivid image of a sort of vortex at a crossroads that I woke up convinced that it was an important geometric message to myself. In a half-waking state I free-associated and became certain that I knew roughly what question this was the answer to and roughly what direction it was pointing me in. For about two days I was fully expecting this to lead to a little breakthrough, muttering to myself about PL cotangent microbundles; but it all came to nothing.
A: Stanislaw Ulam, as quoted in Turing’s Cathe⁣dral:

Once in my life I had a mathematical dream which proved correct. I was twenty years old. I thought, my God, this is wonderful, I won’t have to work, it will all come in dreams! But it never happened again.

J Thomas:

Once after I had spent several days trying to prove a topology theorem, I dreamed about it and woke up with a counterexample. In the dream it just constructed itself, and I could see it. I didn’t have a fever then, though. Later one of my teachers, an old Polish woman, explained her experience. She kept a notebook by her bed so she could write down any insights she got in her sleep. She woke up in the night with a wonderful proof, and wrote it down, and in the morning when she looked at it it was all garbage. “You cannot do math in your sleep. You will have to work.”

Richard Guy:

Guy: If I do any mathematics at all I think I do it in my sleep.
MP: Do you think a lot of mathematicians work that way?
Guy: I do. Yes. The human brain is a remarkable thing, and we are a long way from understanding how it works. For most mathematical problems, immediate thought and pencil and paper—the usual things one associates with solving mathematical problems—are just totally inadequate. You need to understand the problem, make a few symbols on paper and look at them. Most of us, as opposed to Erdős who would probably give an answer to a problem almost immediately, would then probably have to go off to bed, and, if we’re lucky, when we wake up in the morning, we would already have some insight into the problem. On those rare occasions when I have such insight, I quite often don’t know that I have it, but when I come to work on the problem again, to put pencil to paper, somehow the ideas just seem to click together, and the thing goes through. It is clear to me that my brain must have gone on, in an almost combinatorial way, checking the cases or doing an enormous number of fairly trivial arithmetical computations. It seems to know the way to go. I first noticed this with chess endgames, which are indeed finite combinatorial problems. The first indication that I was interested in combinatorics—I didn’t know I had the interest, and I didn’t even know there was such a subject as combinatorics—was that I used to compose chess endgames. I would sit up late into the night trying to analyze a position. Eventually I would sink into slumber and wake up in the morning to realize that if I had only moved the pawns over one file the whole thing would have gone through clearly. My brain must have been checking over this finite but moderately large number of possibilities during the night. I think a lot of mathematicians must work that way.
MP: Have you talked to any other mathematicians about that?
Guy: No. But in Jacques Hadamard’s book on invention in the mathematical field, he quotes some examples there where it is fairly clear that people do that kind of thing. There was someone earlier this week who was talking about Jean-Paul Serre. He said that if you ask Serre a question he either gives you the answer immediately, or, if he hesitates, and you push him in any way, he will say, “How can I think about the question when I don’t know the answer?” I thought that was a lovely remark. At a much lower level, one should think, “What shape should the answer be?” Then your mind can start checking whether you’re right and how to find some logical sequence to get you where you want to go.

Jaques Hadamard, from An Essay on the Psychology of Invention in the Mathematical Field:

Let us come to mathematicians. One of them, Maillet, started a first inquiry as to their methods of work. One famous question, in particular, was already raised by him that of the “mathematical dream”, it having been suggested often that the solution of problems that have defied investigation may appear in dreams. Though not asserting the absolute non-existence of “mathematical dreams”, Maillet’s inquiry shows that they cannot be considered as having a serious significance. Only one remarkable observation is reported by the prominent American mathematician, Leonard Eugene Dickson, who can positively assert its accuracy…Except for that very curious case, most of the 69 correspondents who answered Maillet on that question never experienced any mathematical dream (I never did) or, in that line, dreamed of wholly absurd things, or were unable to state precisely the question they happened to dream of. 5 dreamed of quite naive arguments. There is one more positive answer; but it is difficult to take account of it, as its author remains anonymous.

Quotes mostly sourced from this essay.
A: I knew someone years ago who reported a dream of dying and going to Hell and meeting Fermat. (Fermat explained to him that that's where all mathematicians go.) My friend asked Fermat how his proof went -- the one that was too long for the margin. He got the beginning of an answer: First we rewrite the equation 
$$y^n=z^n-x^n.
$$
But then he woke up.
A: Hadamard investigates these kinds of issues at length in his book The psychology of invention in the mathematical field. He gives several examples of famous mathematicians dreaming about solutions, including Poincare. His conclusion is that the unconscious definitely plays a decisive role in mathematics, and that sleep often has to do with it, but that it differs from person to person how to tap in to it.
It is (necessarily) a bit pseudoscientific, but has some great tidbits. For example, did you know Mobius' grandson, who was a psychologist into the then-popular phrenology, actually went around measuring mathematicians' heads, trying to locate the "bump" in the skull where mathematical ability should lie?
A: I wanted to extend a algorithm from the (sporadic finite simple) Monster group to the Bimonster (an extension of the direct product of the Monster by itself). I considered this as a difficult task.  Then I had a dream:
I wanted to tune two organ pipes so that they produce the same note. But there were always beats, indicating that the two notes are not exactly the same.
After waking up I found an error, in a paper on the subject that I have read, as well as in my algorithm:
For all generators of the Bimonster that I have used, both factors of the direct product were the same. Hence the generators did not generate the direct product, but just a diagonal of it. So in the dream I had do get the two notes together, and in my system of generators I had to take the two factors of the direct product apart.
A: A. Hitchkock had frequently bright ideas for films in his sleep. Unfortunately, he could not remember them at morning. One evening, he took a paper bond and a pen next to his bed. When an idea came up, he awoke and wrote it, then felt asleep again. At morning, he read the idea : "Boy meets girl".
I recall this well-known account to express my doubt about the efficiency of good reasoning during the sleep. I had many times the impression to achieve wonderful tasks in my sleep, and it was always an illusion.
On the other hand, my uncle told in many interviews how the idea of his thesis (about the higher homotopy groups) came up, in a sleeping car. Then he told is wife, lying on the bed just below : "I got it".
A: 
Have you solved problems in your sleep?

T. K. Rajagopolan, a former accountant general of Madras, would tell of Ramanujan's insistence that after seeing in dreams the drops of blood that, according to tradition, heralded the presence of the god Narasimha, the male consort of the goddess Namagiri, “scrolls containing the most complicated mathematics used to unfold before his eyes.”
K. Gopalachary, a friend of Ramanujan from Madras days, said that Ramanujan even attributed his early interest in mathematics to a dream-a dream about, of all things, a street peddler hawking pills.
$\qquad\qquad\quad$ — Robert Kanigel, The Man Who Knew Infinity: A Life of the Genius Ramanujan.
A: I had a "near miss" while I was a PhD student. In a dream, I proved something about definability in some fragment of first-order logic with generalized quantifiers. I woke up straight away and wrote the proof down before going back to sleep. In the morning, it still looked like a proof so I went and discussed it with my advisor. After a little while, he found a flaw but the proof was still correct in a special case.
I'm not sure if this meets your criterion of "significance". It wasn't trivial (the proof was about a third of a page) but it was hardly ground-breaking. It was something we'd been thinking about for a couple of weeks and, as far as I'm aware, the problem is still open.

As I recall, the problem was something like this.  Let $\mathrm{FO}(\mathrm{GI})$ be the extension of first-order logic with a quantifier for graph isomorphism. The syntax is generated by the normal rules for $\mathrm{FO}$ plus the rule that, if $\varphi(\bar{x},\bar{y})$ and $\psi(\bar{x},\bar{y})$ are formulas in which the variables $\bar{x}=x_1\dots x_k$ and $\bar{y}=y_1\dots y_k$ are free, then $\mathrm{GI}_{\bar{x},\bar{y}}(\varphi,\psi)$ is a formula in which $\bar{x}$ and $\bar{y}$ are bound. The semantics is as follows. In any relational structure with domain $V$, we can consider each of $\varphi$ and $\psi$ as defining a directed graph with vertex set $V^k$ and an edge between any pair of vertices that satisfy the formula. Now, $\mathrm{GI}_{\bar{x},\bar{y}}(\varphi,\psi)$ is true if, and only if, the two graphs are isomorphic.
Question: In the vocabulary with only equality (and no constant symbols), is $\mathrm{FO}=\mathrm{FO}(\mathrm{GI})$ on finite structures?
The case $k=1$ is trivial, as there are only four graphs you can define. I think my proof worked for $k=2$ but not for anything larger.
A: Yes, exactly this happened to me. I had spent the day on a laborious proof of a simple result in $n$-dimensional euclidean geometry. The proof was ugly, and I was unhappy with it; I felt that there should be an elegant way. I went to bed later than usual, exhausted and somewhat frustrated. The moment I woke the next morning, I had the key idea: embed the problem in a higher-dimensional space. This method is not original, but at the time it was new to me. There was a hint of it in the previous work---an $(n+1)$-square matrix popped up as a way of describing something in the proof---but it didn't occur to me to interpret this geometrically while I was awake.
A: An interesting piece to read which tells the story of a dream leading, not to a single result, but a fundamental shift in a mathematician's work (leading to the proof, with collaborators, of Local Langlands for $p$-adic fields and of the Sato-Tate conjecture) by Michael Harris:
https://webusers.imj-prg.fr/~michael.harris/androids.pdf
A: On several occasions it has happened that I have made a key insight while sleeping or drifting in and out of sleep.
For example, one of the critical ideas in my paper

*

*Joel David Hamkins, Gap forcing, Israel J. Math. 125 (2001), 237--252,

came to me this way, and waking up with the mathematical idea, I tore myself out of bed to work it out more fully on paper. It was totally right and formed the basis of later work. I remember sitting in my night attire in the bare moonlight at the table in my apartment, looking out at the empty sidewalk at Wall Street and Williams, where I lived at the time, pondering the approximation property applied to ultrafilters.
Because this has now happened several times, I now quite regularly try to prime myself, by intentionally focusing on a particular mathematical issue just as I am going to sleep. My mind floods with mathematical ideas just as I drift off. On welcome rare occasions, the problem is solved in the hypnagogic state, and having awoken I lay in bed pondering it, trying to check it, and wondering if it really is right (sometimes, of course, what seems right is later found to be mistaken). More often, though, when there is welcome news it consists not of a full solution but rather of a new perspective, which later forms the framework of a solution. That is, the result of the unconscious thought is a new way of thinking about the problem, rather than a complete logical proof.
At times, naturally, it is an interesting (or obsessive) MathOverflow question that I set myself to thinking about as I lay myself down. But let me say categorically that it has never been the case (ahem, cough, cough) that an hour or two after going to bed, I would wake with an answer and crawl out to my computer to type up an MO answer in the dark, while the rest of the household is sleeping, only to realize at that point, right before clicking "Post Your Answer" that the solution was totally flawed or wrong. What a downer that would be, to be sitting in the dark in the middle of the night, tired, with nothing to show for it but a wrong mathematical idea. That has NEVER happened...  :-)
A: The article "Do androids prove theorems in their sleep?" available here describes an instance in which a dream inspired a mathematical result. It describes the details of the Thomason-Trobaugh theorem mentioned above in the comments.
A: It is absolutely not about math but it conveys my experience with that kind of things better than anything else I know
Michel Gondry - rolling egg dream
A: Soon after getting married I dreamt of a number. I knew that that number was somehow very important, and I absolutely shouldn't forget it. Despite being asleep I managed to remember that number and recalled it in the morning. It was very important to me indeed: it was my new wife's social security number that I entered numerous times into various forms the day before.
