Ramsey's Theorem for infinite graphs requires some choice but when looking at the proof it is not evident how choice is exactly used.
Sketch of the proof:
Given $c:[\omega]^2\rightarrow 2$ a coloring we construct a homogeneous set as follows. Inductively we set $a_0=0$ and $S_0=\omega$ then one has that $S_0$ is partitioned into $H^0_0\{a\in S_0\setminus\{a_0\}:c(\{a,a_0\})=0\}$ and $H^0_1\{a\in S_0\setminus\{a_0\}:c(\{a,a_0\})=1\}$ we set $S_1$ to be $H^0_0$ if it's infinite and $H^0_1$ if it's not. And we set $a_1$ to be the minimum of $S_1$. We define analogously $a_{n+1}$ and $S_{n+1}$ from $S_n$ and $a_n$. Given then the set $\{a_n:n\in \omega\}$ we have that for a given $n$ then for all $m>n$ $c(\{a_n,a_m\})$ is constant of color $i_n$. This defines a function $\omega \rightarrow 2$ so we take the preimage of $0$ if it's infinite other we take the preimage of $1$.
I know I am wrong but none of the steps seem arbitrary since both $\omega$ and $2$ are well ordered I can always choose a least element. So where exactly is the axiom of choice needed in this proof? Since the graph version is equivalent to the fact that $\aleph_0$ has the tree property I am assuming it has to do with the existence of the "branch" $S_n$.
Best Answer
Ramsey's theorem for countably infinite graphs (or even just Dedekind-infinite graphs) does not require choice. It's only when we try to formulate it for arbitrary infinite graphs that choice comes into play.
Specifically, if we want to prove "For every infinite set $X$ and every $c:[X]^2\rightarrow2$, there is an infinite $H\subseteq X$ such that $c\upharpoonright [H]^2$ is constant," we need to first find a copy of $\omega$ inside $X$ (in order to run the argument in the OP). But the statement "Every infinite set has a countably infinite subset" requires choice in a pretty clear way.
Incidentally, it's worth keeping in mind - just as a basic reality-checking mechanism - that choice (and the continuum hypothesis, and etc.) cannot possibly be relevant to any sufficiently concrete theorem. Specifically, $\mathsf{ZFC+GCH}$ (+ even more!) proves exactly the same $\Pi^1_2$ sentences as $\mathsf{ZF}$; this is (a special case of) Shoenfield absoluteness. And Ramsey's theorem for $\omega$ is prima facie $\Pi^1_2$, so right off the bat we know that choice can't be needed for it.
Is Shoenfield overkill here? Oh my goodness yes. But set theory has so many counterintuitive aspects that I really do think it is a useful thing to keep in mind, even when not necessary, simply to assure yourself that there are really no secret applications of choice lurking in an apparently-simple argument. In particular, I think it's totally appropriate to treat Shoenfield as a blackbox for now; it will still serve a purpose.