The extension of the 2adic valuation to the reals used in the usual proof uses clearly AC. But is this really necessary ? After all, given a equidissection in $n$ triangles, it is finite, so it should be possible to construct a valuation for only the algebraic numbers, and the coordinates of the summits (with a finite number of "choices"), and then follow the proof to show that $n$ must be even. Or am I badly mistaken ?
No choice is needed. If, in a choiceless universe, there were a counterexample, then that counterexample amounts to finitely many real numbers (the coordinates of the relevant points). It would still be a counterexample in the subuniverse of sets constructible (in Gödel's sense) from those finitely many reals. But that subuniverse satisfies the axiom of choice, so your favorite ZFC proof of the theorem applies there.

$\begingroup$ Am I right that this only shows $\def\zf{\text{ZF}}$$\zf \vdash φ$ where $φ$ is a sentence stating Monsky's theorem? If so, then am I correct that it is weaker than the other proof, because it's possible that ZF is $Σ_1$unsound in which case you can prove that ZF proves $φ$ although there is in fact no proof in ZF of $φ$? The other proof however gives us an explicit way to write down a proof of Monsky's theorem over ZF, which avoids the need to assume that ZF is $Σ_1$sound. $\endgroup$ – user21820 Jul 28 '16 at 11:32

$\begingroup$ @user21820 No, this argument, combined with the proofs in ZF of the relativizations to $L[x]$ of the ZFC axioms, provides a way of (constructively) converting any ZFC proof of $\varphi$ into a ZF proof of $\varphi$. Since a ZFC proof is known, we could (tediously) produce an explicit ZF proof. $\endgroup$ – Andreas Blass Jul 28 '16 at 17:48
I was recently looking over Monsky's Theorem as supplementary material for my course notes on local fields, and I noticed that his original article (available here) ends by addressing your question:
The above proof is not so wildly nonconstructive as it first appears. For the entire argument is carried out in the field generated by the coordinates of the vertices. So it is only necessary to extend our ultranorm from $\mathbb{Q}$ to this finitely generated field, not to the entire field of real numbers.
It is easy to see that extending a rank $1$ valuation from a field $K$ to any monogenic extension $K(t)$ does not use the axiom of choice: if $t$ is algebraic over $K$ the set of extensions is finite, nonempty and explicitly in bijection with $\operatorname{Spec} \hat{K} \otimes_K K(t)$ (and even without AC a finitedimensional $K$algebra must have a maximal ideal!); if $t$ is transcendental over $K$, we may endow $K(t)$ with the Gauss norm, determined on $K[t]$ by $a_n t^n + \ldots + a_0 = \max_i a_i$ and extended to $K(t)$ by multiplicativity.
Otherwise put: whereas Andreas Blass's nice answer explains why any proof of this result yields an ACless proof, my answer mentions that Monsky's proof does not really use AC, as pointed out by Monsky.
This paper (Projective Colorings, by Hales and Straus) seems to imply that the Axiom of Choice is necessary for closely related results.

1$\begingroup$ The use of the axiom of choice in the HalesStrauss paper is needed to get nonArchimedean valuations on the whole real field. But in the proof of Monsky's theorem, they use the valuation only for the coordinates of the points involved in an alleged counterexample to Monsky's theorem. So, any particular alleged counterexample can be refuted by a nonArchimedean valuation on a much smaller field, in fact a countable subfield of the reals. And the existence of such valuations doesn't need choice. $\endgroup$ – Andreas Blass Sep 13 '12 at 0:18

$\begingroup$ Thanks! This is pretty much as the OP had conjectured, but I guess my point was that we were skating pretty close to the AC... $\endgroup$ – Igor Rivin Sep 13 '12 at 1:29
In the proof given in the book "Proofs from the book" by Martin Aigner and Gunter Ziegler , 2adic norm is not specifically used.
It proves it using an arbitrary nonarchimedean norm such that v(1/2) > 1. And proves that such a validation exists for R .
Thought it also mentions that 2 adic norm can be extended to reals but it is not "a standard algebra fare" although I don't know what that means.
Here is the link for the proof https://books.google.co.in/books?id=2iI9BAAAQBAJ&pg=PA156&lpg=PA156&dq=monsky+theorem+real+numbers&source=bl&ots=ZnUF1Jv8yF&sig=jLjRaeJYmxtQaYCayy3IkqjRUg0&hl=en&sa=X&ved=0CEoQ6AEwB2oVChMI9SMv9XnxwIVEnGOCh245gwy#v=onepage&q=monsky%20theorem%20real%20numbers&f=false

2$\begingroup$ How does this answer the question about the axiom of choice in the proof? $\endgroup$ – Asaf Karagila Sep 8 '15 at 18:14

$\begingroup$ I tried to imply that since it proves the existence of non archimedian validation for R without axiom of choice it should be able to extend 2adic to R without it too. Am I mistaken in this line of thinking? $\endgroup$ – Tushant Mittal Sep 19 '15 at 21:22