I understand that one can give a proof of each of these propositions assuming the truth of the other. But this seems a bit squishy to me, since there is a trivial sense in which any two true theorems are equivalent (to any proof of Theorem A, prepend "Assume Theorem B", and vice versa; the objection "But the proof of Theorem A doesn't really use the assumption that Theorem B holds" seems more psychological than mathematical).
One might try to formalize the notion of equivalence by considering the lengths of proofs, saying "There is a derivation of Theorem A from Theorem B that is significantly shorter than any proof of Theorem A from scratch, and vice versa", but this too is squishy, in two distinct ways: the length of a proof depends on the formalization procedure one chooses, and "significantly shorter" is vague. Moreover, it's hard to imagine how one could work with this notion of equivalence, since the totality of all short proofs is going to be hard to get a handle on, for the usual reasons.
Can one find some sort of mathematical context (a topos, perhaps?) in which there is a rigorously defined (and not vacuously true) meaning of the equivalence between Sperner and Brouwer?
(For a recent article that discusses this equivalence and gives pointers to relevant literature, see "A Borsuk-Ulam Equivalent that Directly Implies Sperner's Lemma" by Nyman and Su in the April 2013 issue of the American Mathematical Monthly, a version of which is available online at http://willamette.edu/~knyman/papers/Fan_Sperner.pdf .)
See also the related thread Sperner's lemma and Tucker's lemma.
Best Answer
Sperner's lemma is not equivalent to Brouwer's Fixed Point Theorem. All that one can prove directly from Sperner's Lemma is the following weaker statement.
Approximate Fixed Point Theorem. Let $K$ be the standard $n$-dimensional simplex and let $f:K \to K$ be a continuous function. For every $\varepsilon \gt 0$ there is an $x \in K$ such that $|f(x) - x| \leq \varepsilon$.
A compactness argument is then needed to derive the existence of an actual fixed point for $f$.
The analysis is done in §IV.7 of Simpson's Subsystems of Second-Order Arithmetic and the conclusion is that the Brouwer Fixed Point Theorem is equivalent to the Weak König Lemma over the base system RCA0. On the other hand, since Sperner's Lemma is a finite combinatorial statement, it is provable in RCA0. The Approximate Fixed Point Theorem is also provable in RCA0 via Sperner's Lemma. The final compactness argument is however beyond the reach of RCA0.