It is a well known pathological counterexample in group theory that (assuming the axiom of choice), we have an isomorphism$$\mathbb{R} \cong \mathbb{R}^2,$$ where these are additive groups. This somewhat unsettling result generally is shown by appealing to fact that both of these groups, when viewed as $\mathbb{Q}$-vector spaces, have the same dimension. Naturally, showing this relies on the axiom of choice.
As with most results coming from the axiom of choice, it is strongly insinuated that one cannot explicitly construct an isomorphism $\phi : \mathbb{R} \rightarrow \mathbb{R}^2$.
This is very believable, but I'm wondering if it has actually been shown that this fact is equivalent to choice (i.e. without choice, the two are not isomorphic). If so, what would a proof of that look like? All comments are appreciated.
It's definitely not equivalent to full choice, because "choice can start to fail arbitrarily high up the von Neumann hierarchy". One way to see it's independent of $\mathsf{ZF}$ (ie "requires some choice") is to note that composing an isomorphism $\Bbb R \to \Bbb R^2$ with a projection map $\Bbb R^2 \to \Bbb R$ will give a non-injective nontrivial homomorphism $\Bbb R \to \Bbb R$. In other words, this gives a discontinuous solution to the Cauchy functional equation. And it's known to be consistent with $\mathsf{ZF}$ that there's no such function.