Consider the following situation:
There is an infinite set $G$ of giraffes.
A lion comes and announces a set $C$ of all possible colours and an infinite cardinal $\kappa$.
The hungry lion tells the giraffes that when she comes back, the following happens:
The giraffes may no longer speak to each other.
The lion gives each giraffe a scarf of some colour in the set $C$.
Every giraffe sees all the scarves (including their own) but may be mistaken of the colour of strictly less than $\kappa$ scarves.
The giraffes do not know which scarves they see correctly, only that there is a strict upper bound on the number of false colours.
Then each giraffe must guess the colour of their own scarf.
The lion eats all the giraffes that guess wrong.
Can the giraffes agree on a survival strategy before the lion returns so that strictly less than $\kappa$ giraffes are eaten?
In the typical formulation of this problem $|G|=\kappa=\aleph_0$ and the giraffes have prior knowledge of which scarves they see.
Let us ignore the practical issues related to this generalized savanna for a moment.
This is what the existence of a survival strategy means in more mathematical terms:
Take any infinite set $G$, any nonempty set $C$ and any infinite cardinal $\kappa$.
A survival strategy is a function $S:G\times C^G\to C$ (strategy) with the following property.
Take any any function (colouring) $f\in C^G$ and any $o\in (C^G)^G$ (the giraffe $g\in G$ observes the colour pattern $o(g)$) so that $\left\lvert\{h\in G;o(g)(h)\neq f(h)\}\right\rvert<\kappa$ for all $g\in G$.
Let $a\in C^G$ (the answers given by the giraffes) be defined by $a(g)=S(g,o(g))$.
This $a$ always satisfies $\left\lvert\{g\in G;a(g)\neq f(g)\}\right\rvert<\kappa$.
Note that to make sense of this existence we need not be able to compare all cardinals; it suffices that $|A|<\kappa$ is well defined.
(I am not a set theorist myself. If this formulation seems inappropriate or does not seem to correspond to the story, let me know. If you know how to add clarifying details to this question, feel free to edit.)
Claim:
The giraffes have a survival strategy in ZFC.
Proof:
In the set $C^G$ of all possible scarf colourings define an equivalence relation $\sim$ by
$$
a\sim b
\iff
\left\lvert\{g\in G;a(g)\neq b(g)\}\right\rvert<\kappa.
$$
Let $q:C^G\to C^G/{\sim}$ be the quotient map and $r$ a right inverse for it.
The giraffes can agree on the map $r$ based on the information given by the lion.
Suppose the scarf colour pattern chosen by the lion is $f\in C^G$.
All giraffes can see the equivalence class $q(f)$ but cannot be sure about $f$ itself.
The giraffe $g\in G$ the guesses $r(q(f))(g)\in C$, so that the answers form the colour pattern $r(q(f))$.
Since $r(q(f))\sim f$, the number of mistaken giraffes is strictly less than $\kappa$.
In terms of the more mathematical formulation, the strategy is $S(g,v)=r(q(v))(g)$.
$\square$
The problem:
The proof relies heavily on the axiom of choice (the existence of $r$).
But is it equivalent to it?
That is, if we assume that the giraffes have a survival strategy for any $G$, $C$ and $\kappa$, can we deduce the axiom of choice?
My vague intuition suggests an affirmative answer, but I do not have any real arguments to support it.
I have not seen such claims in lists of equivalent forms of the axiom of choice.
One issue is that the strategy is somewhat indeterministic in the sense that it does not give any control over the identities of the surviving giraffes.
There are of course variations of the problem:
Do we really need the strategy for all $G$, $C$ and $\kappa$, or is it enough let let one or two of them vary (perhaps $|G|=\kappa$ and $C=\{0,1\}$)?
What if the giraffes have prior knowledge of which scarves they don't see correctly (e.g. their own)?
Note:
One purpose of the animal story is to give simple and reasonably intuitive names for the objects.
But my main purpose is that if the result indeed is equivalent with the axiom of choice, this could be used to demonstrate what the axiom of choice is about to non-mathematical (or choice-ignorant mathematical) audience.
It is of course interesting as such that the existence of a survival strategy follows from AC, but it would be much more interesting if the existence had abstract consequences, AC itself or something else.
Best Answer
It is certainly true that some choice is required.
An isomorphic game (mapping (giraffes, scarves, lion) to (prisoners, hats, warden)) was considered by Hardin and Taylor in their stimulating (and elementary) paper
The claim you make in your question is called by them the Gabay-O'Connor theorem (though Gabay and O'Connor do not seem to have published it).
Hardin and Taylor show that, in the case $|G| = \kappa = \aleph_0$ and $|C|=2$, it is consistent with ZF+DC (where DC is the Axiom of Dependent Choice) that the giraffes cannot win - that for every survival strategy, the lion (knowing the strategy) can assign the scarves in such a way that $\aleph_0$ many giraffes are eaten. Specifically, the existence of a winning survival strategy would imply the existence of a subset of $\mathbb{R}$ which does not have the property of Baire (BP) - and it is a celebrated theorem of Shelah that it is consistent with ZF+DC that every subset of $\mathbb{R}$ has the BP.
It can also be shown that a survival strategy would imply the existence of a subset of $\mathbb{R}$ which is not Lebesgue measurable. (One way to show this is via the Lebesgue density theorem. I also worked out a kind of cute probabilistic argument a couple years ago, which I may put in here if anyone is interested or if I get bored.) Solovay has shown (thanks Asaf for the correction) that if "ZFC + there is an inaccessible cardinal" is consistent (which I understand is widely believed to be the case), then so is "ZF + DC + every subset of $\mathbb{R}$ is Lebesgue measurable." So again we see that more than DC is needed.
On the other hand, one should be able to produce a survival strategy (in the case $|C| = 2$) from a free ultrafilter, so the ultrafilter lemma is sufficient, and I believe the ultrafilter lemma is known to be strictly weaker than AC. So the existence of a survival strategy when $|C|=2$ cannot imply AC. (Maybe a similar argument applies for other finite $C$?) In principle, it could imply some weaker yet still interesting choice principle, but I do not know whether anyone has looked at that.I don't know what I was thinking when I wrote that, but in fact I do not know of any way to get a survival strategy for this particular game from a free ultrafilter. (There are variants where a free ultrafilter suffices, e.g. if the victory condition is changed to "either all giraffes guess correctly or all guess incorrectly".)(Disclaimer: I am not a set theorist and most of this is stuff I have picked up from folklore because it sounded interesting, so I may well have something completely wrong. The real set theorists here are more than welcome to correct me.)