Which interesting theorems in TCS rely on the Axiom of Choice? (Or alternatively, the Axiom of Determinacy?)
Any arithmetical statement provable in ZFC is provable in ZF, and hence does not "need" the axiom of choice.  By an "arithmetical" statement I mean a statement in the first-order language of arithmetic, meaning that it can be stated using only quantifiers over natural numbers ("for all natural numbers x" or "there exists a natural number x"), without quantifying over sets of natural numbers.  At first glance it might seem very restrictive to forbid quantification over sets of integers; however, finite sets of integers can be "encoded" using a single integer, so it's O.K. to quantify over finite sets of integers.

Virtually any statement of interest in TCS can, with perhaps a bit of finagling, be phrased as an arithmetical statement, and so doesn't need the axiom of choice.  For example, $P\ne NP$ looks at first glance like an assertion about infinite sets of integers, but can be rephrased as, "for every polynomial-time Turing machine, there exists a SAT instance that it gets wrong," which is an arithmetical statement.  Thus my answer to Ryan's question is, "There aren't any that I know of."

But wait, you may say, what about arithmetical statements whose proof requires something like Koenig's lemma or Kruskal's tree theorem?  Don't these require a weak form of the axiom of choice?  The answer is that it depends on exactly how you state the result in question.  For example, if you state the graph minor theorem in the form, "given any infinite set of unlabeled graphs, there must exist two of them such that one is a minor of the other," then some amount of choice is needed to march through your infinite set of data, picking out vertices, subgraphs, etc. [EDIT: I made a mistake here. As Emil Jeřábek explains, the  graph minor theorem&mdash;or at least the most natural statement of it in the absence of AC&mdash;is provable in ZF.  But modulo this mistake, what I say below is still essentially correct.] However, if instead you write down a particular encoding by natural numbers of the minor relation on labeled finite graphs, and phrase the graph minor theorem as a statement about this particular partial order, then the statement becomes arithmetical and doesn't require AC in the proof.

Most people feel that the "combinatorial essence" of the graph minor theorem is already captured by the version that fixes a particular encoding, and that the need to invoke AC to label everything, in the event that you're presented with the general set-theoretic version of the problem, is sort of an irrelevant artifact of a decision to use set theory rather than arithmetic as one's logical foundation.  If you feel the same way, then the graph minor theorem doesn't require AC.  (See also this post by Ali Enayat to the Foundations of Mathematics mailing list, written in response to a similar question that I once had.)

The example of the chromatic number of the plane is similarly a matter of interpretation.  There are various questions you can ask that turn out to be equivalent if you assume AC, but which are distinct questions if you don't assume AC.  From a TCS point of view, the combinatorial heart of the question is the colorability of finite subgraphs of the plane, and the fact that you can then (if you want) use a compactness argument (this is where AC comes in) to conclude something about the chromatic number of the whole plane is amusing, but of somewhat tangential interest.  So I don't think this is a really good example.

I think ultimately you may have more luck asking whether there are any TCS questions that require large cardinal axioms for their resolution (rather than AC).  Work of Harvey Friedman has shown that certain finitary statements in graph theory can require large cardinal axioms (or at least the 1-consistency of such axioms).  Friedman's examples so far are slightly artificial, but I wouldn't be surprised to see similar examples cropping up "naturally" in TCS within our lifetimes.