You don’t even need an infinite number of monkeys! For any $\epsilon > 0$ and $k \geq l(\text{Hamlet})$, there is some number $N$ such that $N$ monkeys at typewriters, each typing for $k$ keystrokes, will produce a copy of Hamlet with probability greater than $1-\epsilon$. (This holds under some quite weak conditions on our model of monkey typing.)
This is an example of the general “soft analysis to hard analysis” principle, championed by Terry Tao among others: most any proof in analysis may be transformed into a proof of a quantitative statement such as the one above.
This can be made precise in some generality using various rather beautiful proof-theoretic methods, such as variants of Gödel’s Dialectica translation; lovely results along these lines have been obtained by e.g. Avigad, Gerhardy and Towsner. In this particular case, the bounds we get will of course depend on the model of monkey typing used.
For instance, if we assume that the keystrokes are independently uniformly distributed, if our Hamlet-recognition criterion is case-, punctuation- and whitespace-insensitive, then for the case $k = l(\text{Hamlet})$,
$$N = \left\lceil \frac{\log \epsilon}{\log \left(1 - \frac{1}{26^{l(\text{Hamlet})}}\right)}\right\rceil$$
will work. (The proof is an exercise for the reader.)
Project Gutenberg’s copy of Hamlet (first folio) weighs in at 117,496 alphanumeric characters. So if we want to produce Hamlet (first folio) with probability 1/2, in the minimal number of keystrokes, then by some quick slapdash estimating (rounding up a little to be on the safe side), something like $10^{170,000}$ monkeys should certainly suffice!
I guess empirical testing is out — ethical controls are so tricky. Anyone want to run some simulations?
