Find all the functions $f:\mathbb R\rightarrow \mathbb R$, such that $f\left(x+2^y\right)=f(x)+2^{f(y)}$

Lemma 1. $f(0) = 0$ and $f(1) = 1$.

Proof. Notice that

$$f(2) = f(0 + 2^1) = f(0) + 2^{f(1)}.$$

On the other hand, applying $f(x+1) = f(x + 2^0) = f(x) + 2^{f(0)}$ twice shows that

$$f(2) = f(0) + 2\cdot 2^{f(0)} = f(0) + 2^{1+f(0)}.$$

Comparing both identities yield $f(1) = f(0) + 1$. Then comparing this with $f(1) = f(0) + 2^{f(0)}$, we find that $f(0) = 0$ and $f(1) = 1$ as desired.

Lemma 2. $f(2^x) = 2^{f(x)}$ for all $x \in \Bbb{R}$. In particular, $f(x) > 0$ if $x > 0$.

Proof. $f(2^x) = f(0 + 2^x) = f(0) + 2^{f(x)} = 2^{f(x)}$ by Lemma 1.

Lemma 3. $f(-x) = -f(x)$ for all $x \in \Bbb{R}$.

Proof. In view of Lemma 1, it suffices to assume that $x > 0$. Then $x = 2^y$ for some $y \in \Bbb{R}$. Then

$$ 0 = f(0) = f(-x + 2^y) = f(-x) + 2^{f(y)} = f(-x) + f(2^y) = f(-x) + f(x). $$

Lemma 4. $f(x+y) = f(x)+f(y)$ for all $x,y \in \Bbb{R}$.

Proof. By Lemma 1, it suffices to show this for $y \neq 0$. If $y > 0$, we have

$$ f(x+y) = f(x) + 2^{f(\log_2 y)} = f(x) + f(y). $$

If $y < 0$, then the previous step and Lemma 3 shows that

$$ f(x+y) = -f(-x+(-y)) = -f(-x) - f(-y) = f(x) + f(y). $$

Proposition. $f(x) = x$ for all $x \in \Bbb{R}$.

(We can appeal to the general theory of Cauchy functional equation, but let me give a self-contained proof for this specific problem.)

Proof. By the mathematical induction together with Lemma 4, $f(nx) = nf(x)$ for all $n \in \Bbb{Z}_{>0}$ and $x \in \Bbb{R}$. By Lemma 3, this extends to all of $n \in \Bbb{Z}$. Then for any rational number $r = p/q$ with $p, q$ integers and $q > 0$,

$$ qf(r) = f(qr) = f(p) = pf(1) = p $$

and thus $f(r) = r$. Now using Lemma 2, we know that $f$ is increasing. Fix $x \in \Bbb{R}$ and choose two sequences of rational numbers $(l_n)$ and $(u_n)$ such that $l_n \uparrow x$ and $u_n \downarrow x$. Then taking limit to the inequality

$$l_n = f(l_n) \leq f(x) \leq f(u_n) = u_n $$

shows that $f(x) = x$.

Suggestion: I don't know how either, but look at what $x = y = 0$ tells you: $f(1) = f(0) + 2^{f(0)}$. If we let $A = 2^{f(0)}$ for the moment, then by plugging in some other values for $x$ (holding $y$ at 0) we get $$ f(2) = f(1+1) = f(1) + A\\ f(3) = f(2+1) = f(2) + A = f(1) + 2A \\ f(n + 1) = f(n) + A = \ldots = f(1) + (n-1) A $$

So on the integers at least, you have something affine.

Post-comment additions:

Following @JLoreaux's comment, this actually holds for all integers. And Rupert's comment gives us that $f$ is increasing. So if we can just prove continuity, we'll be done: pick $f(0)$, and the rest follows.

For continuity: Look at $f(x+h) - f(x)$ as $h \to 0+$. Write $y = \log_2 h$, so that $h = 2^y$, and as $h \to 0$, $y \to -\infty$. Then we get $$ f(x+h) - f(x) = 2^{f(\log_2 h)} = 2^{f(y)}. $$ with $y \to -\infty$. Now for $y$ a dyadic rational, the function is affine, and since the affine slope is positive, on the dyadic rationals, $f(y) -> -\infty$. But since $f$ is increasing, we actually can extend this to say that $f(y) \to -\infty$ on the reals as well.

Hence $$ \lim_{h \to 0+} f(x+h) - f(x) = 0. $$

So the function is right-continuous at every point.

So this leaves only left-continuity. For that, at present, I have no insight. But maybe "affine on the dyadic rationals and right continuous" actually implies continuity on the reals. It sure seems likely, but my analysis skills are way out of date.