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.) 


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$. 


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$. 


I have found this paper by Peter Loeb:
Here is the theorem from this paper that implies that the usual Hilbert cube is compact without using the AC.
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]$. 

