I am just curious: is there a published proof of the compactness of the Hilbert cube that does not use the Axiom of Choice, or is it well known?
If by the Hilbert cube you mean only $[0,1]^\mathbb N$ then the answer is yes. There is such proof, you can find it in Herrlich's The Axiom of Choice as Theorem 3.13.
If you mean the general case of $[0,1]^I$ then the answer is no, to prove that all Hilbert cubes are compact is equivalent to BPIT/The ultrafilter lemma/Tychonoff for Hausdorff spaces. The proof of that you can find in the same book as Theorem 4.70.
The compactness of the Hilbert cube follows (without AC) from the compactness of $2^\omega$, since $[0,1]$ as well as $[0,1]^\omega$ are continuous images of $2^\omega$.
(Conversely, $2^\omega$ is a closed subset of the Hilbert cube.)
The compactness of $2^\omega$ is just König's lemma for trees of binary sequences, which is easy to prove (hence certainly wellknown) without AC. (I think this is called "weak König's lemma", an important principle in reverse mathematics.)

2$\begingroup$ But Koenig's lemma does require a minute amount of choice. It is not needed in the case of $2^\omega$ because that is a linearly ordered set, and every level is finite, so we get a choice function. $\endgroup$ – Asaf Karagila Jan 19 '13 at 21:59

3$\begingroup$ Compactness of $2^\omega$ can also easily be seen by identifying it with the Cantor set, a closed subset of $[0,1]$. $\endgroup$ – Eric Wofsey Jan 19 '13 at 22:03

$\begingroup$ Andrej, it depends on your formulation of the lemma. If you formulate it over a countable tree  sure. But if you only state that the tree has $\omega$ levels and each is finite then you do need the axiom of choice. See Jech's "The Axiom of Choice" for details, Chapter 7 somewhere around the end. $\endgroup$ – Asaf Karagila Jan 19 '13 at 22:07

1$\begingroup$ Clearly, you should understand my comment in the form that is relevant to pointing out that the general case of Koenig's lemma does require choice. I have seen more than enough people thinking that the existence of free ultrafilters is equivalent to the axiom of choice, just because you are using Zorn's lemma. $\endgroup$ – Asaf Karagila Jan 19 '13 at 22:15

6$\begingroup$ I don't understand what you are arguing about. Asaf, Andrej and I agree that the version of König's lemma that is needed here does not need AC. $\endgroup$ – Goldstern Jan 19 '13 at 22:34
Some of the comments in Goldstern's answer look like they express doubt as to whether choice is required. Here is a proof without choice, in gory detail, just to make sure. The trick is to notice that the construction of an infinite branch $\alpha$ in an infinite binary tree $T$ requires no appeal to the axion of choice because we can specify a concrete choice: go left if you can, otherwise go right.
The Hilbert cube is a continuous image of the Cantor space $2^\omega$ of infinite binary sequences with the product topology. Thus it suffices to show that $2^\omega$ is compact. Given a finite binary sequence $a = [a_1, \ldots, a_n]$, denote by $a = n$ its length, and let $B_a = \lbrace \alpha \in 2^\omega \mid a = [\alpha_1, \ldots, \alpha_{a}] \rbrace$ be the basic open subset of those sequences that start with $a$.
Consider any cover $(B_{a_i})_{i \in I}$ of $2^\omega$. We build a binary tree $T$ which consists of those finite binary sequences $a$ for which $B_a$ is not contained in any $B_{a_i}$, $$T = \lbrace a \in 2^{*} \mid \forall i \in I . B_a \not\subseteq B_{a_i} \rbrace.$$ In other words, we put in $T$ any finite sequence $a$ such that all of its prefixes are not in $(a_i)_{i \in I}$. Let us show that $T$ has bounded height, i.e., there is $n$ such that every branch in $T$ has lebgth at most $n$.
Suppose on the contrary that the height of $T$ is unbounded. Then we can build an infinite path $\alpha$ in $T$ by recursion as follows. (This is König's lemma, saying that an unbounded binary tree has an infinite path.) We make sure that at each stage $n$ the subtree of $T$ at $[\alpha_1, \ldots, \alpha_n]$ has unbounded height. Start with the empty sequence $[]$. The tree at $[]$ is all of $T$, which has unbounded height by assumption. If $[\alpha_1, \ldots, \alpha_n]$ has been constructed, let $T'$ be the subtree of $T$ at $[\alpha_1, \ldots, \alpha_n]$. One or both of the trees $$T_0' = \lbrace b \in T' \mid b_{n+1} = 0 \rbrace$$ and $$T_1' = \lbrace b \in T' \mid b_{n+1} = 1 \rbrace$$ have unbounded height. If $T_0'$ does, set $\alpha_{n+1} = 0$, otherwise set $\alpha_{n+1} = 1$. (At this point we did not appeal to the axiom of choice, but we did appeal to excluded middle.) This concludes the construction of $\alpha$. Now we have a problem since $\alpha$ is covered by some $B_{a_i}$, and so $a_i$ is a prefix of $\alpha$, but this contradicts the definition of $T$.
Now we know that the height of $T$ is bounded by some $n$. Consider the subset $J \subseteq I$ of those indices $j \in I$ for which $a_j \leq n + 1$. As there are only finitely many binary sequences of length at most $n+1$, the set $J$ is finite. But since every sequence of length $n+1$ has some $j \in J$ such that $a_j$ is its prefix, $(B_{a_j})_{j \in J}$ is a finite cover of $2^\omega$.

3$\begingroup$ No one in the comments to Goldstern's answer has any doubts that the axiom of choice is unneeded. $\endgroup$ – Asaf Karagila Jan 19 '13 at 23:11

$\begingroup$ Furthermore, let $S=\bigcup_{n\in\omega} P_n$ be a disjoint union of pairs such that no infinite set of pairs has a choice function. Let $T$ be the tree of finite choice functions from an initial segment of $\omega$, that is $g\in T$ is a function from some $n\in\omega$ into $S$ such that $g(i)\in P_i$ for $i<n$. This is an infinite binary tree, but it has no branch. $\endgroup$ – Asaf Karagila Jan 19 '13 at 23:38

$\begingroup$ Why are you coming up with stuff that is irrelevant to this question? $\endgroup$ – Andrej Bauer Jan 20 '13 at 8:47

$\begingroup$ I fixed the first sentence so as to make it as clear that nobody had doubts about choice as you made it clear in the comments that you had no such doubts ;) $\endgroup$ – Andrej Bauer Jan 20 '13 at 8:48

2$\begingroup$ Andrej, first I thank you for removing that line. Second, the reason I am coming up with things so irrelevant is that your phrasing is wrong. I gave you an example of an infinite binary tree without an infinite path. Infinite does not mean countably infinite, or even Dedekindinfinite without the axiom of choice. It is important to make this distinction because while I know it, and I am sure that you and Goldstern are well aware of this distinction not all the readers are. The relevant changes are not big and they are important. Next thing people insist that cardinals are always ordinals.. $\endgroup$ – Asaf Karagila Jan 20 '13 at 13:07
Thanks for all the answers and sorry about a silly question. I have also figured out that it can be proved using the usual complete metric on the usual (countable product) Hilbert cube and finite $\epsilon$nets.
Update. Here is a proof.
Let $X = [\frac{1}{2},\frac{1}{2}]\times[\frac{1}{4},\frac{1}{4}]\times[\frac{1}{8},\frac{1}{8}]\times\dotsb$ be a Hilbert cube endowed with its $\ell_\infty$ metric. For every positive integer $k$, let $N_k$ be the “natural” $\frac{1}{2^k}$net for $X$.
Let $\mathcal U$ be a given family of open sets such that no finite subfamily of $\mathcal U$ covers $X$. Then let $S_k$ be the set of those elements of $N_k$ which are within the distance of $\frac{1}{2^k}$ from the complement of any finite union of elements of $\mathcal U$. Each $S_k$ is nonempty. For all $m$ and $n$, the distance from any point of $S_m$ to the set $S_n$ is at most $\frac{1}{2^m}+\frac{1}{2^n}$.
Assume that the points of $X$ are ordered by the lexicographic order of their coordinates. Take the “first” $x_1\in S_1$ (i.e. the smallest in the order), then the “first” $x_2\in S_2$ that is within the distance of $\frac{3}{4}$ from $x_1$, then the “first” $x_3\in S_3$ that is within the distance of $\frac{3}{8}$ from $x_2$, and so forth. The obtained sequence $\lbrace x_k \rbrace_{k=1}^\infty$ is Cauchy. Its limit is not in any element of $\mathcal U$.

1$\begingroup$ You have to be careful how you formulate this proof. The implication "Every totally bounded complete metric space is compact" uses AC, as far as I can see. $\endgroup$ – Goldstern Jan 20 '13 at 10:05

$\begingroup$ @Goldstern, probably you are right in general (is the Axiom of Choice for families of finite sets equivalent to the usual one?). In the case of Hilbert cube, the $\epsilon$nets can be constructed explicitly, so that there will be no problem. $\endgroup$ – Alexey Muranov Jan 20 '13 at 12:57

2$\begingroup$ Alexey far from it. The axiom of choice for families of finite sets do not imply the axiom of choice for families of countable sets, or even countable choice for that matter. $\endgroup$ – Asaf Karagila Jan 20 '13 at 13:05
I have found this paper by Peter Loeb:
 Peter A. Loeb, A new proof of the Tychonoff Theorem, The American Mathematical Monthly 72 (1965), no. 7, 711717.
Here is the theorem from this paper that implies that the usual Hilbert cube is compact without using the AC.
Theorem 1. Let $\{\,X_\nu\mid\nu\in I\,\}$ be a family of compact spaces which is indexed by a set $I$ on which there is a wellordering $\ge$. If $I$ is an infinite set, let there also be a choice function $F$ on the collection $\{\,C\mid\text{$C$ is closed},\ C\ne\varnothing,\ \text{$C\subset X_\nu$ for some $\nu$}\,\}$. Then the product space $\prod_{\nu\in I}X_\nu$ is compact in the product topology.
For the usual Hilbert cube $[0,1]^{\mathbb N}$, the function $F$ can, for example, select the least element in every compact subset of $[0,1]$.