Is $\alpha < \beta \to 2^\alpha < 2^\beta$ provable in ZF+V=HOD?

No, of course not.

Lemma. Every set of ordinals appears in the $\sf HOD$ of a generic extension which agrees on the power set of whatever fixed $\lambda$.

Sketch of Proof. Let $A\subseteq\alpha$ be a set of ordinals. Pick some large enough $\kappa$, and force $\sf GCH$ to hold between $\kappa$ and $\kappa^{+\alpha}$ by means of forcing and without adding new subsets to $\lambda$. Next, force that $2^{\kappa^{+\beta+1}}=\kappa^{+\beta+3}$ if and only if $\beta\in A$. We can do that without adding subsets to $\lambda$ as well.

Now $A$ is definable from the parameters $\kappa$ and $\alpha$, since it is exactly the failure of $\sf GCH$ in the first $\alpha$th successors of $\kappa$.

Now, start with a model of $\sf GCH$, add $\aleph_2$ Cohen reals, so that $2^{\aleph_0}=2^{\aleph_1}=\aleph_2$. Next, consider the Cohen reals as a subset of $\omega_2\times\omega$, and code this into a set of ordinals $A$ (either via the Gödel pairing function, or simply in the naive way of looking at this as a subset of the ordinal $\omega_2\cdot\omega$).

Then code $A$ into $\sf HOD$ of some generic extension without adding any new subsets to $\omega_2$.