Could someone give me an explicit basis of $\mathbf{R}$ as a vector space over $\mathbf{Q}$?
I know some linearly independent subset, namely $1,e,e^2,\dots$ but this seems to be a deep result already (this is just the transcendence of $e$, right?), but no maximal linearly independent subset.
Let me clarify: I know how to prove that every vector space (over a division ring) has a basis, it is by Zorn's lemma and equivalent to AC. I don't think that this directly implies that one cannot describe some basis explicitly; can one prove that the existence of a basis of $\mathbf{R}$ over $\mathbf{Q}$ is equivalent to AC? This would convince me.
The axiom of choice is necessary for producing a Hamel basis for $\Bbb R$ over $\Bbb Q$, meaning we can prove that without the axiom of choice we cannot prove the existence of a Hamel basis; and of course it is not equivalent to the existence of such basis.
Let me start with the easy part. The second part. There is no statement which is limited to a particular set that is equivalent to the axiom of choice in general. The reason is that the axiom of choice may fail so far above the real numbers, that the usual proof goes on without a hitch, but the axiom of choice still fails in horrible ways. So no, this is not equivalent to the axiom of choice.
The reason we cannot produce an explicit definition that $\sf ZF$ proves that is a Hamel basis for $\Bbb R$ over $\Bbb Q$, is that there are models of $\sf ZF+\lnot AC$ where there is no such basis. For example, if there is a Hamel basis then there is a discontinuous function $f\colon\Bbb R\to\Bbb R$ such that $f(x+y)=f(x)+f(y)$. This is really just a linear endomorphism over $\Bbb R$ as a vector space over $\Bbb Q$.
Why is there a discontinuous one? Because a Hamel basis would have $2^{2^{\aleph_0}}$ permutations, each inducing a linear automorphism (not just any endomorphism), but as a separable space there are only $2^{\aleph_0}$ continuous functions from $\Bbb R$ to itself.
And in some models of $\sf ZF+\lnot AC$ we can prove that every linear endomorphism of $\Bbb R$ is continuous. So in such model there are no Hamel bases to $\Bbb R$ over $\Bbb Q$.
Of course this does not mean that you can't write a formula which describe a Hamel basis in some models of $\sf ZF$. But these models will have to satisfy certain assumptions which cannot be proved without the axiom of choice, and usually even more than just that. So the "explicit" part here is not that explicit after all.