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 finite-dimensional $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 AC-less proof, my answer mentions that Monsky's proof does not really use AC, as pointed out by Monsky.