The question is about the complexity of the simplest possible Hamel basis of l^infty, and this is a perfectly sensible thing to ask about even in a context where one wants to retain the Axiom of Choice. That is, we know by AC that there is a basis---how complex must it be? 

Such a question finds a natural home in descriptive set theory, a subject concerned with numerous similar complexity issues. In particular,
descriptive set theory provides tools to make the question
precise. 

My answer is that one can never prove a negative answer to the question, because it is consistent with the ZFC axioms of set theory that
Yes, one can concretely exhibit a Hamel basis of l^infty.

To explain, one natural way to measure the complexity of sets of reals
(or subsets of R^infty) is with the projective hierarchy.
This is the hierarchy that begins with the closed sets (in
R, say, or in R^omega), and then iteratively closes under
complements and projections (or equivalently, continuous
images). The Borel sets appear near the bottom of this
hierarchy, at the level called Delta<sup>1</sup><sub>1</sub>, and then the
analytic sets Sigma<sup>1</sup><sub>1</sub> and co-analytic sets Pi<sup>1</sup><sub>1</sub>, and so
on up the hierarchy. Sets in the projective hierarchy are
exactly those sets that can be given by explicit definition
in the structure of the reals, with quantification only
over reals and over natural numbers. If we were to find a
projective Hamel basis, then it will have been
<em>exhibited</em> in a way that is concrete, free of
arbitrary choices. Thus, a very natural way of making the
question precise is to ask:

<b>Question.</b> Does l^infty have a Hamel basis that is
projective?

If the axioms of set theory are consistent, then they are
consistent with a positive answer to this question. This is
not quite the same as proving a positive answer, to be
sure, but it does mean that no-one will ever prove a
negative answer to the question.

<b>Theorem.</b> If the axioms of ZFC are consistent, then
they are consistent with the existence of a projective
Hamel basis for l^infty. Indeed, there can be such a basis
with complexity Pi<sup>1</sup><sub>3</sub>.

Proof. I will prove that under the set-theoretic assumption
known as the Axiom of Constructibility V=L, there is a
projective Hamel basis. In my answer to question about <a
href="http://mathoverflow.net/questions/6593">Well-orderings of the reals</a>, I explained that
in Goedel's constructible universe L, there is a definable
well-ordering of the reals. This well-ordering has
complexity Delta<sup>1</sup><sub>2</sub> in the projective hierarchy. From this
well-ordering, one can easily construct a well-ordering of
l^infty, since infinite sequences of reals are coded
naturally by reals. Now, given the well-ordering of
l^infty, one defines the Hamel basis as usual by taking all
elements not in the span of elements preceding it in the
well-order. The point for this question is that if the
well-order has complexity Delta<sup>1</sup><sub>2</sub>, then this definition
of the basis has complexity Pi<sup>1</sup><sub>3</sub>, as desired. QED

OK, so we can write down a definition, and in some
set-theoretic universes, this definition concretely
exhibits a Hamel basis of l^infty. There is no guarantee,
however, that this definition will work in other models of
set theory. I suspect that one will be able to find other
models of ZFC, in which there is no projective Hamel basis
of l^infty. It is already known that there might be no
projective well ordering of the reals (a situation that
follows from large cardinals and other set theoretic
hypotheses), and perhaps this also implies that there is no
projective Hamel basis. In this case, it would mean that
the possibility of exhibiting a concrete Hamel basis is
itself <em>independent of ZFC</em>. This would be an
interesting and subtle situation. To be clear, I am not
referring here merely to the existence of a basis requiring
AC, but rather, fully assuming the Axiom of Choice, I am
proposing that the possibility of finding a
<em>projective</em> basis is independent of ZFC.

<b>Conjecture.</b> The assertion that there is a projective
Hamel basis of l^infty is independent of ZFC.

I only intend to consider the question in models of ZFC, so
that l^infty has a Hamel basis of some kind, and the only
question is whether there is a projective one or not. In this situation, the fact that AD seems to imply that there is no Hamel basis is not relevent, since that axiom contradicts AC.

Apart from this, I also conjecture that there can never be
a Hamel basis of l^infty that is Borel. This would be a lower bound on the complexity of how concretely one could exhibit the basis.